let R be non degenerated Ring; :: thesis: for n being Ordinal
for p being Polynomial of n,R holds Lt (LM p) = Lt p
let n be Ordinal; :: thesis: for p being Polynomial of n,R holds Lt (LM p) = Lt p
let p be Polynomial of n,R; :: thesis: Lt (LM p) = Lt p
H: Lt p is Element of Bags n by PRE_POLY:def 12;
field (BagOrder n) = Bags n by ORDERS_1:12;
then I: BagOrder n linearly_orders Support (LM p) by ORDERS_1:37, ORDERS_1:38;

per cases ( p = 0_ (n,R) or p <> 0_ (n,R) ) ;

suppose AS: p = 0_ (n,R) ; :: thesis: Lt (LM p) = Lt p

then B: Support p = {} by YY;
Support (LM p) c= Support p by YZ;
then Support (LM p) = {} by B;
hence Lt (LM p) = Lt p by AS, YY; :: thesis: verum

end;

suppose p <> 0_ (n,R) ; :: thesis: Lt (LM p) = Lt p

then LC p <> 0. R by Y0;
then (LM p) . (Lt p) <> 0. R by lemY;
then A: Lt p in Support (LM p) by H, POLYNOM1:def 4;
then B: Support (LM p) = {(Lt p)} by Z2;
then E: card (Support (LM p)) = 1 by CARD_1:30;
then C: len (SgmX ((BagOrder n),(Support (LM p)))) = 1 by I, PRE_POLY:11;
rng (SgmX ((BagOrder n),(Support (LM p)))) = {(Lt p)} by I, B, PRE_POLY:def 2;
then D: SgmX ((BagOrder n),(Support (LM p))) = <*(Lt p)*> by E, I, PRE_POLY:11, FINSEQ_1:39;
E: LM p <> 0_ (n,R) by A, YY;
thus Lt (LM p) = <*(Lt p)*> . 1 by C, D, E, defLT
.= Lt p ; :: thesis: verum

end;

end;