theorem ThSep03: :: FIELD_15:78

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