theorem :: FIELD_15:65

for F being Field
for p being non zero Polynomial of F
for E being FieldExtension of F
for K being b₃ -extending FieldExtension of F
for a being Element of E holds multiplicity (p,(@ (a,K))) = multiplicity (p,a) by multi3K;