Theorem psr1basf

Description: Univariate power series base set elements are functions. (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypotheses	psr1rcl.p	|- P = ( PwSer1 ` R )
	psr1rcl.b	|- B = ( Base ` P )
	psr1basf.k	|- K = ( Base ` R )
Assertion	psr1basf	|- ( F e. B -> F : ( NN0 ^m 1o ) --> K )

Proof

Step	Hyp	Ref	Expression
1		psr1rcl.p	|- P = ( PwSer1 ` R )
2		psr1rcl.b	|- B = ( Base ` P )
3		psr1basf.k	|- K = ( Base ` R )
4		elmapi	|- ( F e. ( K ^m ( NN0 ^m 1o ) ) -> F : ( NN0 ^m 1o ) --> K )
5	1 2 3	psr1bas	|- B = ( K ^m ( NN0 ^m 1o ) )
6	4 5	eleq2s	|- ( F e. B -> F : ( NN0 ^m 1o ) --> K )