theorem UP55: :: FIELD_15:62

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