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= {()} )

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= {()} )

let p be Polynomial of n,L; :: thesis: ( degree p = 0 iff Support p c= {()} )
thus ( degree p = 0 implies Support p c= {()} ) :: thesis: ( Support p c= {()} implies degree p = 0 )
proof
assume A1: degree p = 0 ; :: thesis: Support p c= {()}
per cases ( p = 0_ (n,L) or p <> 0_ (n,L) ) ;
suppose A2: p = 0_ (n,L) ; :: thesis: Support p c= {()}
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Support p or y in {()} )
assume A3: y in Support p ; :: thesis: y in {()}
then p . y <> 0. L by POLYNOM1:def 3;
hence y in {()} by ; :: thesis: verum
end;
suppose A4: p <> 0_ (n,L) ; :: thesis: Support p c= {()}
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Support p or y in {()} )
assume A5: y in Support p ; :: thesis: y in {()}
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 {()} by TARSKI:def 1; :: thesis: verum
end;
end;
end;
assume A6: Support p c= {()} ; :: thesis:
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 ;
hence contradiction by A7, A8, UPROOTS:11; :: thesis: verum