let R be Ring; :: thesis: for p being Polynomial of R holds deg (LM p) = deg p
let p be Polynomial of R; :: thesis: deg (LM p) = deg p
thus deg (LM p) = (len (LM p)) - 1 by HURWITZ:def 2
.= (len p) - 1 by POLYNOM4:15
.= deg p by HURWITZ:def 2 ; :: thesis: verum