theorem :: FIELD_15:55

for F being Field
for p being non zero Polynomial of F
for a being Element of F holds deg p >= multiplicity (p,a) by ro00;