let R be non degenerated Ring; :: thesis: for n being Ordinal
for p being Polynomial of n,R holds
( Lt (LM p) = Lt p & LC (LM p) = LC p )
let n be Ordinal; :: thesis: for p being Polynomial of n,R holds
( Lt (LM p) = Lt p & LC (LM p) = LC p )
let p be Polynomial of n,R; :: thesis: ( Lt (LM p) = Lt p & LC (LM p) = LC p )
thus Lt (LM p) = Lt p by lemZ; :: thesis: LC (LM p) = LC p
thus LC (LM p) = (LM p) . (Lt p) by lemZ
.= LC p by lemY ; :: thesis: verum