let F be Field; :: thesis: for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F holds
( Poly (m,p) = 0_ ((card (nonConstantPolys F)),F) iff p = 0_. F )
let m be Ordinal; :: thesis: ( m in card (nonConstantPolys F) implies for p being Polynomial of F holds
( Poly (m,p) = 0_ ((card (nonConstantPolys F)),F) iff p = 0_. F ) )
assume K: m in card (nonConstantPolys F) ; :: thesis: for p being Polynomial of F holds
( Poly (m,p) = 0_ ((card (nonConstantPolys F)),F) iff p = 0_. F )
let p be Polynomial of F; :: thesis: ( Poly (m,p) = 0_ ((card (nonConstantPolys F)),F) iff p = 0_. F )
set n = card (nonConstantPolys F);
H: Support (Poly (m,p)) c= {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m} } by Th14c;

A: now :: thesis: ( p = 0_. F implies Poly (m,p) = 0_ ((card (nonConstantPolys F)),F) )

assume AS: p = 0_. F ; :: thesis: Poly (m,p) = 0_ ((card (nonConstantPolys F)),F)

now :: thesis: for o being object holds not o in Support (Poly (m,p))

let o be object ; :: thesis: not o in Support (Poly (m,p))
assume B: o in Support (Poly (m,p)) ; :: thesis: contradiction

per cases ( o in {(EmptyBag (card (nonConstantPolys F)))} or o in { b where b is bag of card (nonConstantPolys F) : support b = {m} } ) by H, B, XBOOLE_0:def 3;

suppose o in {(EmptyBag (card (nonConstantPolys F)))} ; :: thesis: contradiction

then o = EmptyBag (card (nonConstantPolys F)) by TARSKI:def 1;
then (Poly (m,p)) . o = p . 0 by defPg;
hence contradiction by B, AS, POLYNOM1:def 4; :: thesis: verum

end;

suppose o in { b where b is bag of card (nonConstantPolys F) : support b = {m} } ; :: thesis: contradiction

then consider b being bag of card (nonConstantPolys F) such that
D: ( o = b & support b = {m} ) ;
(Poly (m,p)) . b = p . (b . m) by D, defPg;
hence contradiction by D, B, AS, POLYNOM1:def 4; :: thesis: verum

end;

end;

end;

then Support (Poly (m,p)) = {} by XBOOLE_0:def 1;
hence Poly (m,p) = 0_ ((card (nonConstantPolys F)),F) by YY; :: thesis: verum

end;

now :: thesis: ( Poly (m,p) = 0_ ((card (nonConstantPolys F)),F) implies p = 0_. F )

assume AS: Poly (m,p) = 0_ ((card (nonConstantPolys F)),F) ; :: thesis: p = 0_. F

now :: thesis: for i being Element of NAT holds p . i = 0. F

let i be Element of NAT ; :: thesis: p . b₁ = 0. F

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: p . b₁ = 0. F

hence p . i = (Poly (m,p)) . (EmptyBag (card (nonConstantPolys F))) by defPg
.= 0. F by AS, POLYNOM1:22 ;
:: thesis: verum

end;

suppose A: i <> 0 ; :: thesis: p . b₁ = 0. F

for o being object st o in {m} holds
o in card (nonConstantPolys F) by K, TARSKI:def 1;
then reconsider S = {m} as finite Subset of (card (nonConstantPolys F)) by TARSKI:def 3;
set b = (S,i) -bag ;
B: support ((S,i) -bag) = S by A, UPROOTS:8;
m in {m} by TARSKI:def 1;
hence p . i = p . (((S,i) -bag) . m) by UPROOTS:7
.= (Poly (m,p)) . ((S,i) -bag) by B, defPg
.= 0. F by AS, POLYNOM1:22 ;
:: thesis: verum

end;

end;

end;

hence p = 0_. F ; :: thesis: verum

end;

hence ( Poly (m,p) = 0_ ((card (nonConstantPolys F)),F) iff p = 0_. F ) by A; :: thesis: verum