theorem :: FIELD_15:64

for F being Field
for p being non zero Polynomial of F
for E being FieldExtension of F
for a being Element of F holds multiplicity (p,(@ (a,E))) = multiplicity (p,a) by multi3;