theorem spl1: :: FIELD_8:33

for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F st p splits_in E holds
FAdj (F,(Roots (E,p))) is SplittingField of p