let F be Field; :: thesis: for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F holds Poly (m,(LM p)) = Monom ((LC (Poly (m,p))),(Lt (Poly (m,p))))
let m be Ordinal; :: thesis: ( m in card (nonConstantPolys F) implies for p being Polynomial of F holds Poly (m,(LM p)) = Monom ((LC (Poly (m,p))),(Lt (Poly (m,p)))) )
assume AS: m in card (nonConstantPolys F) ; :: thesis: for p being Polynomial of F holds Poly (m,(LM p)) = Monom ((LC (Poly (m,p))),(Lt (Poly (m,p))))
let p be Polynomial of F; :: thesis: Poly (m,(LM p)) = Monom ((LC (Poly (m,p))),(Lt (Poly (m,p))))
set n = card (nonConstantPolys F);
set q = Poly (m,(LM p));
thus Poly (m,(LM p)) = Monom ((coefficient (Poly (m,(LM p)))),(term (Poly (m,(LM p))))) by POLYNOM7:11
.= Monom ((LC (Poly (m,(LM p)))),(term (Poly (m,(LM p))))) by Th14x
.= Monom ((LC (Poly (m,(LM p)))),(Lt (Poly (m,(LM p))))) by Th14x
.= Monom ((LC (Poly (m,p))),(Lt (Poly (m,(LM p))))) by AS, Th14z
.= Monom ((LC (Poly (m,p))),(Lt (Poly (m,p)))) by AS, Th14z ; :: thesis: verum