let n be Ordinal; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds
( degree p = 0 iff Support p c= {(EmptyBag n)} )
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L holds
( degree p = 0 iff Support p c= {(EmptyBag n)} )
let p be Polynomial of n,L; :: thesis: ( degree p = 0 iff Support p c= {(EmptyBag n)} )
thus ( degree p = 0 implies Support p c= {(EmptyBag n)} ) :: thesis: ( Support p c= {(EmptyBag n)} implies degree p = 0 )

proof

assume A1: degree p = 0 ; :: thesis: Support p c= {(EmptyBag n)}

per cases ( p = 0_ (n,L) or p <> 0_ (n,L) ) ;

suppose A2: p = 0_ (n,L) ; :: thesis: Support p c= {(EmptyBag n)}

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Support p or y in {(EmptyBag n)} )
assume A3: y in Support p ; :: thesis: y in {(EmptyBag n)}
then p . y <> 0. L by POLYNOM1:def 3;
hence y in {(EmptyBag n)} by A3, A2, POLYNOM1:22; :: thesis: verum

end;

suppose A4: p <> 0_ (n,L) ; :: thesis: Support p c= {(EmptyBag n)}

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Support p or y in {(EmptyBag n)} )
assume A5: y in Support p ; :: thesis: y in {(EmptyBag n)}
then reconsider S = y as bag of n ;
degree S = 0 by A1, A4, Def3, A5;
then S = EmptyBag n by UPROOTS:12;
hence y in {(EmptyBag n)} by TARSKI:def 1; :: thesis: verum

end;

end;

end;

assume A6: Support p c= {(EmptyBag n)} ; :: thesis: degree p = 0
assume A7: degree p <> 0 ; :: thesis: contradiction
then p <> 0_ (n,L) by Def3;
then consider s being bag of n such that
A8: ( s in Support p & degree p = degree s ) by Def3;
s = EmptyBag n by A6, A8, TARSKI:def 1;
hence contradiction by A7, A8, UPROOTS:11; :: thesis: verum