Theorem psr1bascl

Description: A univariate power series is a multivariate power series on one index. (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypotheses	psr1rcl.p	|- P = ( PwSer1 ` R )
	psr1rcl.b	|- B = ( Base ` P )
Assertion	psr1bascl	|- ( F e. B -> F e. ( Base ` ( 1o mPwSer R ) ) )

Proof

Step	Hyp	Ref	Expression
1		psr1rcl.p	|- P = ( PwSer1 ` R )
2		psr1rcl.b	|- B = ( Base ` P )
3		id	|- ( F e. B -> F e. B )
4		eqid	|- ( 1o mPwSer R ) = ( 1o mPwSer R )
5	1 2 4	psr1bas2	|- B = ( Base ` ( 1o mPwSer R ) )
6	3 5	eleqtrdi	|- ( F e. B -> F e. ( Base ` ( 1o mPwSer R ) ) )