theorem Th12: :: FIELD_11:35

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