Theorem psrelbasfun

Description: An element of the set of power series is a function. (Contributed by AV, 17-Jul-2019)

	Ref	Expression
Hypotheses	psrelbasfun.s	|- S = ( I mPwSer R )
	psrelbasfun.b	|- B = ( Base ` S )
Assertion	psrelbasfun	|- ( X e. B -> Fun X )

Proof

Step	Hyp	Ref	Expression
1		psrelbasfun.s	|- S = ( I mPwSer R )
2		psrelbasfun.b	|- B = ( Base ` S )
3		eqid	|- ( Base ` R ) = ( Base ` R )
4		eqid	|- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
5		id	|- ( X e. B -> X e. B )
6	1 3 4 2 5	psrelbas	|- ( X e. B -> X : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
7	6	ffund	|- ( X e. B -> Fun X )