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,p)) = LC p
let m be Ordinal; :: thesis: ( m in card (nonConstantPolys F) implies for p being Polynomial of F holds LC (Poly (m,p)) = LC p )
assume K: m in card (nonConstantPolys F) ; :: thesis: for p being Polynomial of F holds LC (Poly (m,p)) = LC p
let p be Polynomial of F; :: thesis: LC (Poly (m,p)) = LC p
H: LC p = p . ((len p) -' 1) by RATFUNC1:def 6;

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

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

reconsider p1 = p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
p1 is constant by I0, RATFUNC1:def 2;
then consider a being Element of F such that
I1: p = a | F by RING_4:20;
thus LC (Poly (m,p)) = p . 0 by K, I0, ZZZ
.= a by I1, Th28
.= LC p by I1, RING_5:6 ; :: thesis: verum

end;

suppose I: not p is constant ; :: thesis: LC (Poly (m,p)) = LC p

then A: p <> 0_. F ;
B: support (Lt (Poly (m,p))) = {m} by I, K, XYZa;
E: len p <> 0 by A, POLYNOM4:5;
D: deg p = (len p) - 1 by HURWITZ:def 2
.= (len p) -' 1 by E, XREAL_0:def 2 ;
thus LC (Poly (m,p)) = p . ((Lt (Poly (m,p))) . m) by B, defPg
.= LC p by I, K, D, H, XYZa ; :: thesis: verum

end;

end;