set n = card (nonConstantPolys F);
defpred S₁[ Element of Bags (card (nonConstantPolys F)), Element of the carrier of F] means ( ( support $1 = {} & $2 = p . 0 ) or ( support $1 = {m} & $2 = p . ($1 . m) ) or ( support $1 <> {} & support $1 <> {m} & $2 = 0. F ) );
A: for x being Element of Bags (card (nonConstantPolys F)) ex y being Element of the carrier of F st S₁[x,y]

proof

let x be Element of Bags (card (nonConstantPolys F)); :: thesis: ex y being Element of the carrier of F st S₁[x,y]

per cases ( support x = {} or support x = {m} or ( support x <> {} & support x <> {m} ) ) ;

suppose support x = {} ; :: thesis: ex y being Element of the carrier of F st S₁[x,y]

hence ex y being Element of the carrier of F st S₁[x,y] ; :: thesis: verum

end;

suppose support x = {m} ; :: thesis: ex y being Element of the carrier of F st S₁[x,y]

hence ex y being Element of the carrier of F st S₁[x,y] ; :: thesis: verum

end;

suppose ( support x <> {} & support x <> {m} ) ; :: thesis: ex y being Element of the carrier of F st S₁[x,y]

hence ex y being Element of the carrier of F st S₁[x,y] ; :: thesis: verum

end;

end;

end;

consider f being Function of (Bags (card (nonConstantPolys F))), the carrier of F such that
B: for x being Element of Bags (card (nonConstantPolys F)) holds S₁[x,f . x] from FUNCT_2:sch 3(A);
set M = { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } ;
C: { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } is finite

proof

per cases ( { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } = {} or { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } <> {} ) ;

suppose { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } = {} ; :: thesis: { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } is finite

hence { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } is finite ; :: thesis: verum

end;

suppose { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } <> {} ; :: thesis: { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } is finite

then reconsider M1 = { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } as non empty set ;
defpred S₂[ Element of M1, Element of NAT ] means ex b being bag of card (nonConstantPolys F) st
( $1 = b & support b = {m} & $2 = b . m );
C0: for x being Element of M1 ex y being Element of NAT st S₂[x,y]

proof

let x be Element of M1; :: thesis: ex y being Element of NAT st S₂[x,y]
x in { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } ;
then consider b being bag of card (nonConstantPolys F) such that
C1: ( x = b & support b = {m} & b . m is Element of NAT & b . m in Support p ) ;
take b . m ; :: thesis: S₂[x,b . m]
thus S₂[x,b . m] by C1; :: thesis: verum

end;

consider f being Function of M1,NAT such that
C1: for x being Element of M1 holds S₂[x,f . x] from FUNCT_2:sch 3(C0);
f is one-to-one

proof

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume C2: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
C3: dom f = M1 by FUNCT_2:def 1;
reconsider x1b = x1, x2b = x2 as Element of M1 by C2;
consider b1 being bag of card (nonConstantPolys F) such that
C4: ( x1 = b1 & support b1 = {m} & b1 . m is Element of NAT & b1 . m in Support p ) by C2, C3;
consider b2 being bag of card (nonConstantPolys F) such that
C5: ( x2 = b2 & support b2 = {m} & b2 . m is Element of NAT & b2 . m in Support p ) by C2, C3;
C6: ( S₂[x1b,f . x1b] & S₂[x2b,f . x2b] ) by C1;
C8: dom b1 = card (nonConstantPolys F) by PARTFUN1:def 2
.= dom b2 by PARTFUN1:def 2 ;

now :: thesis: for x being object st x in dom b1 holds
b1 . x = b2 . x

let x be object ; :: thesis: ( x in dom b1 implies b1 . b₁ = b2 . b₁ )
assume x in dom b1 ; :: thesis: b1 . b₁ = b2 . b₁

per cases ( x in support b1 or not x in support b1 ) ;

suppose x in support b1 ; :: thesis: b1 . b₁ = b2 . b₁

then x = m by C4, TARSKI:def 1;
hence b1 . x = b2 . x by C4, C2, C5, C6; :: thesis: verum

end;

suppose C9: not x in support b1 ; :: thesis: b2 . b₁ = b1 . b₁

hence b2 . x = 0 by C5, C4, PRE_POLY:def 7
.= b1 . x by C9, PRE_POLY:def 7 ;
:: thesis: verum

end;

end;

end;

then b1 = b2 by C8;
hence x1 = x2 by C4, C5; :: thesis: verum

end;

hence f is one-to-one ; :: thesis: verum

end;

then C2: card (dom f) = card (rng f) by CARD_1:70;
C3: Support p is finite by POLYNOM1:def 5;
rng f c= Support p

proof

now :: thesis: for o being object st o in rng f holds
o in Support p

let o be object ; :: thesis: ( o in rng f implies o in Support p )
assume o in rng f ; :: thesis: o in Support p
then consider u being object such that
C4: ( u in dom f & f . u = o ) by FUNCT_1:def 3;
u in M1 by C4;
then consider b being bag of card (nonConstantPolys F) such that
C5: ( u = b & support b = {m} & b . m is Element of NAT & b . m in Support p ) ;
reconsider u = u as Element of M1 by C4;
S₂[u,f . u] by C1;
hence o in Support p by C4, C5; :: thesis: verum

end;

hence rng f c= Support p ; :: thesis: verum

end;

then dom f is finite by C3, C2;
hence { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } is finite by FUNCT_2:def 1; :: thesis: verum

end;

end;

end;

Support f c= { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } \/ {((card (nonConstantPolys F)) --> 0)}

proof

now :: thesis: for x being object st x in Support f holds
x in { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } \/ {((card (nonConstantPolys F)) --> 0)}

let x be object ; :: thesis: ( x in Support f implies b₁ in { b₂ where b is bag of card (nonConstantPolys F) : ( support b₂ = {m} & b₂ . m is Element of NAT & b₂ . m in Support p ) } \/ {((card (nonConstantPolys F)) --> 0)} )
assume C0: x in Support f ; :: thesis: b₁ in { b₂ where b is bag of card (nonConstantPolys F) : ( support b₂ = {m} & b₂ . m is Element of NAT & b₂ . m in Support p ) } \/ {((card (nonConstantPolys F)) --> 0)}
then C1: ( x in dom f & f . x <> 0. F ) by POLYNOM1:def 3;
reconsider b = x as Element of Bags (card (nonConstantPolys F)) by C0;
C2: dom b = card (nonConstantPolys F) by PARTFUN1:def 2;

per cases ( support b = {} or support b = {m} or ( support b <> {} & support b <> {m} ) ) ;

suppose support b = {} ; :: thesis: b₁ in { b₂ where b is bag of card (nonConstantPolys F) : ( support b₂ = {m} & b₂ . m is Element of NAT & b₂ . m in Support p ) } \/ {((card (nonConstantPolys F)) --> 0)}

then for z being object st z in dom b holds
b . z = 0 by PRE_POLY:def 7;
then b = (card (nonConstantPolys F)) --> 0 by C2, FUNCOP_1:11;
then x in {((card (nonConstantPolys F)) --> 0)} by TARSKI:def 1;
hence x in { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } \/ {((card (nonConstantPolys F)) --> 0)} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose H: support b = {m} ; :: thesis: b₁ in { b₂ where b is bag of card (nonConstantPolys F) : ( support b₂ = {m} & b₂ . m is Element of NAT & b₂ . m in Support p ) } \/ {((card (nonConstantPolys F)) --> 0)}

reconsider i = b . m as Element of NAT ;
K: dom p = NAT by FUNCT_2:def 1;
f . b = p . (b . m) by B, H;
then b . m in Support p by K, C1, POLYNOM1:def 3;
then b in { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } by H;
hence x in { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } \/ {((card (nonConstantPolys F)) --> 0)} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ( support b <> {} & support b <> {m} ) ; :: thesis: b₁ in { b₂ where b is bag of card (nonConstantPolys F) : ( support b₂ = {m} & b₂ . m is Element of NAT & b₂ . m in Support p ) } \/ {((card (nonConstantPolys F)) --> 0)}

hence x in { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } \/ {((card (nonConstantPolys F)) --> 0)} by B, C1; :: thesis: verum

end;

end;

end;

hence Support f c= { b where b is bag of card (nonConstantPolys F) : ( support b = {m} & b . m is Element of NAT & b . m in Support p ) } \/ {((card (nonConstantPolys F)) --> 0)} ; :: thesis: verum

end;

then reconsider f = f as Polynomial of (card (nonConstantPolys F)),F by C, POLYNOM1:def 5;
take f ; :: thesis: ( f . (EmptyBag (card (nonConstantPolys F))) = p . 0 & ( for b being bag of card (nonConstantPolys F) st support b = {m} holds
f . b = p . (b . m) ) & ( for b being bag of card (nonConstantPolys F) st support b <> {} & support b <> {m} holds
f . b = 0. F ) )
support (EmptyBag (card (nonConstantPolys F))) = {} ;
hence f . (EmptyBag (card (nonConstantPolys F))) = p . 0 by B; :: thesis: ( ( for b being bag of card (nonConstantPolys F) st support b = {m} holds
f . b = p . (b . m) ) & ( for b being bag of card (nonConstantPolys F) st support b <> {} & support b <> {m} holds
f . b = 0. F ) )
thus for b being bag of card (nonConstantPolys F) st support b = {m} holds
f . b = p . (b . m) :: thesis: for b being bag of card (nonConstantPolys F) st support b <> {} & support b <> {m} holds
f . b = 0. F

proof

let b be bag of card (nonConstantPolys F); :: thesis: ( support b = {m} implies f . b = p . (b . m) )
assume H: support b = {m} ; :: thesis: f . b = p . (b . m)
reconsider b1 = b as Element of Bags (card (nonConstantPolys F)) by PRE_POLY:def 12;
S₁[b1,f . b1] by B;
hence f . b = p . (b . m) by H; :: thesis: verum

end;

thus for b being bag of card (nonConstantPolys F) st support b <> {} & support b <> {m} holds
f . b = 0. F :: thesis: verum

proof

let b be bag of card (nonConstantPolys F); :: thesis: ( support b <> {} & support b <> {m} implies f . b = 0. F )
assume H: ( support b <> {} & support b <> {m} ) ; :: thesis: f . b = 0. F
reconsider b1 = b as Element of Bags (card (nonConstantPolys F)) by PRE_POLY:def 12;
S₁[b1,f . b1] by B;
hence f . b = 0. F by H; :: thesis: verum

end;