theorem sepsep1: :: FIELD_15:59

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 a being Element of E holds multiplicity (q,a) = multiplicity (p,a)