let R be non degenerated Ring; :: thesis: for p being non zero Polynomial of R holds LM p = anpoly ((p . (deg p)),(deg p))
let p be non zero Polynomial of R; :: thesis: LM p = anpoly ((p . (deg p)),(deg p))
set q = anpoly ((p . (deg p)),(deg p));
set r = LM p;
set n = deg p;
reconsider degp = deg p as Element of NAT ;
A1: deg p = (len p) -' 1 by XREAL_0:def 2;

now :: thesis: for i being Element of NAT holds (LM p) . i = (anpoly ((p . (deg p)),(deg p))) . i

let i be Element of NAT ; :: thesis: (LM p) . b₁ = (anpoly ((p . (deg p)),(deg p))) . b₁

per cases ( i <> deg p or i = deg p ) ;

suppose A3: i <> deg p ; :: thesis: (LM p) . b₁ = (anpoly ((p . (deg p)),(deg p))) . b₁

then (LM p) . i = 0. R by A1, POLYNOM4:def 1
.= (anpoly ((p . (deg p)),(deg p))) . i by A3, POLYDIFF:25 ;
hence (LM p) . i = (anpoly ((p . (deg p)),(deg p))) . i ; :: thesis: verum

end;

suppose A4: i = deg p ; :: thesis: (LM p) . b₁ = (anpoly ((p . (deg p)),(deg p))) . b₁

then (LM p) . i = p . (deg p) by A1, POLYNOM4:def 1
.= (anpoly ((p . (deg p)),(deg p))) . i by A4, POLYDIFF:24 ;
hence (LM p) . i = (anpoly ((p . (deg p)),(deg p))) . i ; :: thesis: verum

end;

end;

end;

hence LM p = anpoly ((p . (deg p)),(deg p)) ; :: thesis: verum