theorem :: FIELD_15:83

for F being Field
for p being monic non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff for E being SplittingField of p holds p is Ppoly of E,(Roots (E,p)) )