theorem :: FIELD_8:29

for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for U being FieldExtension of F
for E being b₃ -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff Roots (E,p) = Roots (U,p) )