let n be Ordinal; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for b being bag of n st b in Support p holds

degree p >= degree b

let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L

for b being bag of n st b in Support p holds

degree p >= degree b

let p be Polynomial of n,L; :: thesis: for b being bag of n st b in Support p holds

degree p >= degree b

let b be bag of n; :: thesis: ( b in Support p implies degree p >= degree b )

assume A1: b in Support p ; :: thesis: degree p >= degree b

then Support p <> {} by XBOOLE_0:def 1;

then p <> 0_ (n,L) by POLYNOM7:1;

hence degree p >= degree b by A1, Def3; :: thesis: verum

for p being Polynomial of n,L

for b being bag of n st b in Support p holds

degree p >= degree b

let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L

for b being bag of n st b in Support p holds

degree p >= degree b

let p be Polynomial of n,L; :: thesis: for b being bag of n st b in Support p holds

degree p >= degree b

let b be bag of n; :: thesis: ( b in Support p implies degree p >= degree b )

assume A1: b in Support p ; :: thesis: degree p >= degree b

then Support p <> {} by XBOOLE_0:def 1;

then p <> 0_ (n,L) by POLYNOM7:1;

hence degree p >= degree b by A1, Def3; :: thesis: verum