theorem ThSep02: :: FIELD_15:77

for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff for E being FieldExtension of F
for a being Element of E holds multiplicity (p,a) <= 1 )