theorem multi4b: :: FIELD_15:66

for F being Field
for p being non zero Polynomial of F
for q being Polynomial of F
for a being Element of F st p = ((X- a) `^ (multiplicity (p,a))) *' q holds
eval (q,a) <> 0. F