theorem sepsep: :: FIELD_15:58

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