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 )

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

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 A6:
Support p c= {(EmptyBag n)}
; :: thesis: degree p = 0
assume A1:
degree p = 0
; :: thesis: Support p c= {(EmptyBag n)}

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

end;

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;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

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;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

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