Theorem coef

Description: The domain and codomain of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypothesis	dgrval.1	|- A = ( coeff ` F )
Assertion	coef	|- ( F e. ( Poly ` S ) -> A : NN0 --> ( S u. { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		dgrval.1	|- A = ( coeff ` F )
2	1	dgrlem	|- ( F e. ( Poly ` S ) -> ( A : NN0 --> ( S u. { 0 } ) /\ E. n e. ZZ A. x e. ( `' A " ( CC \ { 0 } ) ) x <_ n ) )
3	2	simpld	|- ( F e. ( Poly ` S ) -> A : NN0 --> ( S u. { 0 } ) )