theorem lemsep3: :: FIELD_15:72

for F being Field
for p being non zero Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F st p splits_in E holds
( ex a being Element of E st multiplicity (p,a) > 1 iff p gcd ((Deriv F) . p) <> 1_. F )