theorem Th14z: :: FIELD_11:27

for F being Field
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)) )