let F be Field; :: thesis: for m being Ordinal
for p being Polynomial of F holds Support (Poly (m,p)) c= {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m} }
let m be Ordinal; :: thesis: for p being Polynomial of F holds Support (Poly (m,p)) c= {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m} }
let p be Polynomial of F; :: thesis: Support (Poly (m,p)) c= {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m} }
set n = card (nonConstantPolys F);
set q = Poly (m,p);

now :: thesis: for o being object st o in Support (Poly (m,p)) holds
o in {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m} }

let o be object ; :: thesis: ( o in Support (Poly (m,p)) implies b₁ in {(EmptyBag (card (nonConstantPolys F)))} \/ { b₂ where b is bag of card (nonConstantPolys F) : support b₂ = {m} } )
assume A: o in Support (Poly (m,p)) ; :: thesis: b₁ in {(EmptyBag (card (nonConstantPolys F)))} \/ { b₂ where b is bag of card (nonConstantPolys F) : support b₂ = {m} }
then reconsider b = o as bag of card (nonConstantPolys F) ;
B: (Poly (m,p)) . b <> 0. F by A, POLYNOM1:def 3;

per cases ( support b = {} or ( support b = {m} & b . m is Element of NAT ) or ( support b = {m} & b . m is not Element of NAT ) or ( support b <> {} & support b <> {m} ) ) ;

suppose support b = {} ; :: thesis: b₁ in {(EmptyBag (card (nonConstantPolys F)))} \/ { b₂ where b is bag of card (nonConstantPolys F) : support b₂ = {m} }

then for i being object st i in card (nonConstantPolys F) holds
b . i = {} by PRE_POLY:def 7;
then b = EmptyBag (card (nonConstantPolys F)) by PBOOLE:6;
then b in {(EmptyBag (card (nonConstantPolys F)))} by TARSKI:def 1;
hence o in {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m} } by XBOOLE_0:def 3; :: thesis: verum

end;

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

then b in { b where b is bag of card (nonConstantPolys F) : support b = {m} } ;
hence o in {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m} } by XBOOLE_0:def 3; :: thesis: verum

end;

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

hence o in {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m} } ; :: thesis: verum

end;

suppose ( support b <> {} & support b <> {m} ) ; :: thesis: b₁ in {(EmptyBag (card (nonConstantPolys F)))} \/ { b₂ where b is bag of card (nonConstantPolys F) : support b₂ = {m} }

hence o in {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m} } by defPg, B; :: thesis: verum

end;

end;

end;

hence Support (Poly (m,p)) c= {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m} } ; :: thesis: verum