let R be non degenerated Ring; :: thesis: for n being Ordinal
for p being Polynomial of n,R holds
( LM p = 0_ (n,R) iff p = 0_ (n,R) )
let n be Ordinal; :: thesis: for p being Polynomial of n,R holds
( LM p = 0_ (n,R) iff p = 0_ (n,R) )
let p be Polynomial of n,R; :: thesis: ( LM p = 0_ (n,R) iff p = 0_ (n,R) )
H: Lt p is Element of Bags n by PRE_POLY:def 12;

A: now :: thesis: ( p = 0_ (n,R) implies LM p = 0_ (n,R) )

assume p = 0_ (n,R) ; :: thesis: LM p = 0_ (n,R)
then B: Support p = {} by YY;
Support (LM p) c= Support p by YZ;
then Support (LM p) = {} by B;
hence LM p = 0_ (n,R) by YY; :: thesis: verum

end;

now :: thesis: ( LM p = 0_ (n,R) implies p = 0_ (n,R) )

assume LM p = 0_ (n,R) ; :: thesis: p = 0_ (n,R)
then Support (LM p) = {} by YY;
then 0. R = (LM p) . (Lt p) by H, POLYNOM1:def 4
.= LC p by lemY ;
hence p = 0_ (n,R) by Y0; :: thesis: verum

end;

hence ( LM p = 0_ (n,R) iff p = 0_ (n,R) ) by A; :: thesis: verum