theorem Th14y: :: FIELD_11:28

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