for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for U being FieldExtension of E st p splits_in E holds
p splits_in U