theorem ThSep1: :: FIELD_15:76

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 st a is_a_root_of p,E holds
multiplicity (p,a) = 1 ) ) )