let F be Field; :: thesis: for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F holds
( LC (Poly (m,(LM p))) = LC (Poly (m,p)) & Lt (Poly (m,(LM p))) = Lt (Poly (m,p)) )
let m be Ordinal; :: thesis: ( m in card (nonConstantPolys F) implies for p being Polynomial of F holds
( LC (Poly (m,(LM p))) = LC (Poly (m,p)) & Lt (Poly (m,(LM p))) = Lt (Poly (m,p)) ) )
assume AS: m in card (nonConstantPolys F) ; :: thesis: for p being Polynomial of F holds
( LC (Poly (m,(LM p))) = LC (Poly (m,p)) & Lt (Poly (m,(LM p))) = Lt (Poly (m,p)) )
let p be Polynomial of F; :: thesis: ( LC (Poly (m,(LM p))) = LC (Poly (m,p)) & Lt (Poly (m,(LM p))) = Lt (Poly (m,p)) )
set n = card (nonConstantPolys F);
thus LC (Poly (m,(LM p))) = LC (LM p) by AS, Th14b
.= (LM p) . ((len (LM p)) -' 1) by RATFUNC1:def 6
.= (LM p) . ((len p) -' 1) by POLYNOM4:15
.= p . ((len p) -' 1) by POLYNOM4:def 1
.= LC p by RATFUNC1:def 6
.= LC (Poly (m,p)) by Th14b, AS ; :: thesis: Lt (Poly (m,(LM p))) = Lt (Poly (m,p))

per cases ( p is constant or not p is constant ) ;

suppose I0: p is constant ; :: thesis: Lt (Poly (m,(LM p))) = Lt (Poly (m,p))

hence Lt (Poly (m,p)) = EmptyBag (card (nonConstantPolys F)) by AS, ZZZ
.= Lt (Poly (m,(LM p))) by AS, I0, ZZZ ;
:: thesis: verum

end;

suppose I0: not p is constant ; :: thesis: Lt (Poly (m,(LM p))) = Lt (Poly (m,p))

len (LM p) = len p by POLYNOM4:15;
then H: deg (LM p) = (len p) - 1 by HURWITZ:def 2
.= deg p by HURWITZ:def 2 ;
deg p > 0 by I0, RATFUNC1:def 2;
then I1: not LM p is constant by H, RATFUNC1:def 2;
set b1 = Lt (Poly (m,p));
set b2 = Lt (Poly (m,(LM p)));

now :: thesis: for o being object st o in card (nonConstantPolys F) holds
(Lt (Poly (m,p))) . o = (Lt (Poly (m,(LM p)))) . o

let o be object ; :: thesis: ( o in card (nonConstantPolys F) implies (Lt (Poly (m,p))) . b₁ = (Lt (Poly (m,(LM p)))) . b₁ )
assume o in card (nonConstantPolys F) ; :: thesis: (Lt (Poly (m,p))) . b₁ = (Lt (Poly (m,(LM p)))) . b₁
then reconsider i = o as Ordinal ;

per cases ( i = m or i <> m ) ;

suppose I4: i = m ; :: thesis: (Lt (Poly (m,p))) . b₁ = (Lt (Poly (m,(LM p)))) . b₁

then (Lt (Poly (m,p))) . i = deg p by I0, AS, XYZaa
.= (Lt (Poly (m,(LM p)))) . i by H, I4, I1, AS, XYZaa ;
hence (Lt (Poly (m,p))) . o = (Lt (Poly (m,(LM p)))) . o ; :: thesis: verum

end;

suppose I4: i <> m ; :: thesis: (Lt (Poly (m,p))) . b₁ = (Lt (Poly (m,(LM p)))) . b₁

then (Lt (Poly (m,p))) . i = 0 by I0, AS, XYZaa
.= (Lt (Poly (m,(LM p)))) . i by I4, I1, AS, XYZaa ;
hence (Lt (Poly (m,p))) . o = (Lt (Poly (m,(LM p)))) . o ; :: thesis: verum

end;

end;

end;

hence Lt (Poly (m,(LM p))) = Lt (Poly (m,p)) by PBOOLE:def 10; :: thesis: verum

end;

end;