Theorem ply1basf

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

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

Proof

Step	Hyp	Ref	Expression
1		ply1rcl.p	|- P = ( Poly1 ` R )
2		ply1rcl.b	|- B = ( Base ` P )
3		ply1basf.k	|- K = ( Base ` R )
4		eqid	|- ( 1o mPoly R ) = ( 1o mPoly R )
5		eqid	|- ( Base ` ( 1o mPoly R ) ) = ( Base ` ( 1o mPoly R ) )
6		psr1baslem	|- ( NN0 ^m 1o ) = { a e. ( NN0 ^m 1o ) | ( `' a " NN ) e. Fin }
7		id	|- ( F e. B -> F e. B )
8		eqid	|- ( PwSer1 ` R ) = ( PwSer1 ` R )
9	1 8 2	ply1bas	|- B = ( Base ` ( 1o mPoly R ) )
10	7 9	eleqtrdi	|- ( F e. B -> F e. ( Base ` ( 1o mPoly R ) ) )
11	4 3 5 6 10	mplelf	|- ( F e. B -> F : ( NN0 ^m 1o ) --> K )