theorem :: FIELD_5:31
for F being Field
for f being non constant Element of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st f splits_in E