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) . b1 = (anpoly ((p . (deg p)),(deg p))) . b1
per cases ( i <> deg p or i = deg p ) ;
suppose A3: i <> deg p ; :: thesis: (LM p) . b1 = (anpoly ((p . (deg p)),(deg p))) . b1
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) . b1 = (anpoly ((p . (deg p)),(deg p))) . b1
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