theorem ZZ7: :: FIELD_14:23

for F being Field
for p, q being non zero Polynomial of F
for a being Element of F holds multiplicity (p,a) <= multiplicity ((p *' q),a)