let R be Ring; :: thesis: for p being Polynomial of R holds LC (LM p) = LC p
let p be Polynomial of R; :: thesis: LC (LM p) = LC p
thus LC (LM p) = (LM p) . ((len (LM p)) -' 1) by RATFUNC1:def 6
.= (LM p) . ((len p) -' 1) by POLYNOM4:15
.= p . ((len p) -' 1) by POLYNOM4:def 1
.= LC p by RATFUNC1:def 6 ; :: thesis: verum