let R be non degenerated Ring; :: thesis: for p being non zero Polynomial of R holds p . (deg p) = LC p
let p be non zero Polynomial of R; :: thesis: p . (deg p) = LC p
deg p = (len p) - 1 by HURWITZ:def 2;
hence p . (deg p) = p . ((len p) -' 1) by XREAL_0:def 2
.= LC p by RATFUNC1:def 6 ;
:: thesis: verum