let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F)
for m being Ordinal st m in card (nonConstantPolys F) holds
Poly (m,(anpoly ((LC p),(deg p)))) = LM (Poly (m,p))
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: for m being Ordinal st m in card (nonConstantPolys F) holds
Poly (m,(anpoly ((LC p),(deg p)))) = LM (Poly (m,p))
let m be Ordinal; :: thesis: ( m in card (nonConstantPolys F) implies Poly (m,(anpoly ((LC p),(deg p)))) = LM (Poly (m,p)) )
set n = card (nonConstantPolys F);
assume AS: m in card (nonConstantPolys F) ; :: thesis: Poly (m,(anpoly ((LC p),(deg p)))) = LM (Poly (m,p))
deg p > 0 by RING_4:def 4;
then (len p) - 1 > 0 by HURWITZ:def 2;
then (len p) - 1 = (len p) -' 1 by XREAL_0:def 2;
then deg p = (len p) -' 1 by HURWITZ:def 2;
then anpoly ((LC p),(deg p)) = anpoly ((p . (deg p)),(deg p)) by RATFUNC1:def 6
.= LM p by FIELD_1:11 ;
hence Poly (m,(anpoly ((LC p),(deg p)))) = LM (Poly (m,p)) by AS, Th14y; :: thesis: verum