let R be non degenerated Ring; :: thesis: for n being Ordinal
for p being Polynomial of n,R
for b being bag of n st b <> Lt p holds
(LM p) . b = 0. R
let n be Ordinal; :: thesis: for p being Polynomial of n,R
for b being bag of n st b <> Lt p holds
(LM p) . b = 0. R
let p be Polynomial of n,R; :: thesis: for b being bag of n st b <> Lt p holds
(LM p) . b = 0. R
let b be bag of n; :: thesis: ( b <> Lt p implies (LM p) . b = 0. R )

now :: thesis: ( (LM p) . b <> 0. R implies b = Lt p )

assume AS: (LM p) . b <> 0. R ; :: thesis: b = Lt p
b is Element of Bags n by PRE_POLY:def 12;
then A: b in Support (LM p) by AS, POLYNOM1:def 4;

now :: thesis: not b <> Lt p

assume b <> Lt p ; :: thesis: contradiction
then not b in {(Lt p)} by TARSKI:def 1;
hence contradiction by Z2, A; :: thesis: verum

end;

hence b = Lt p ; :: thesis: verum

end;

hence ( b <> Lt p implies (LM p) . b = 0. R ) ; :: thesis: verum