theorem spl0: :: FIELD_8:32

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