theorem :: FIELD_11:29

for F being Field
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F holds LM (Poly (m,p)) = Poly (m,(LM p)) by Th14y;