theorem lemma5: :: FIELD_8:30

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
p splits_in FAdj (F,(Roots (E,p)))