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 m being Monomial of n,L
for b being bag of n st b <> term m holds
m . b = 0. L
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L
for m being Monomial of n,L
for b being bag of n st b <> term m holds
m . b = 0. L
let p be Polynomial of n,L; :: thesis: for m being Monomial of n,L
for b being bag of n st b <> term m holds
m . b = 0. L
let m be Monomial of n,L; :: thesis: for b being bag of n st b <> term m holds
m . b = 0. L
let b be bag of n; :: thesis: ( b <> term m implies m . b = 0. L )
assume A1: b <> term m ; :: thesis: m . b = 0. L

per cases ( Support m = {} or Support m = {(term m)} ) by POLYNOM7:7;

suppose Support m = {} ; :: thesis: m . b = 0. L

then m = 0_ (n,L) by POLYNOM7:1;
hence m . b = 0. L by POLYNOM1:22; :: thesis: verum

end;

suppose A2: Support m = {(term m)} ; :: thesis: m . b = 0. L

A3: b is Element of Bags n by PRE_POLY:def 12;
not b in Support m by A1, A2, TARSKI:def 1;
hence m . b = 0. L by A3, POLYNOM1:def 4; :: thesis: verum

end;

end;