let F be Field; :: thesis: 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) c= Roots (U,p) )
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: 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) c= Roots (U,p) )
let U be FieldExtension of F; :: thesis: for E being U -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff Roots (E,p) c= Roots (U,p) )
let E be U -extending FieldExtension of F; :: thesis: ( p splits_in E implies ( p splits_in U iff Roots (E,p) c= Roots (U,p) ) )
assume AS: p splits_in E ; :: thesis: ( p splits_in U iff Roots (E,p) c= Roots (U,p) )
H: U is Subfield of E by FIELD_4:7;

A: now :: thesis: ( p splits_in U implies Roots (E,p) c= Roots (U,p) )

assume A1: p splits_in U ; :: thesis: Roots (E,p) c= Roots (U,p)

now :: thesis: for o being object st o in Roots (E,p) holds
o in Roots (U,p)

let o be object ; :: thesis: ( o in Roots (E,p) implies o in Roots (U,p) )
assume o in Roots (E,p) ; :: thesis: o in Roots (U,p)
then o in { a where a is Element of E : a is_a_root_of p,E } by FIELD_4:def 4;
then consider a being Element of E such that
A2: ( o = a & a is_a_root_of p,E ) ;
a in U by AS, A1, A2, lemma2;
then reconsider b = a as Element of U ;
Ext_eval (p,b) = Ext_eval (p,a) by FIELD_7:14
.= 0. E by A2, FIELD_4:def 2
.= 0. U by H, EC_PF_1:def 1 ;
then b is_a_root_of p,U by FIELD_4:def 2;
then b in { a where a is Element of U : a is_a_root_of p,U } ;
hence o in Roots (U,p) by A2, FIELD_4:def 4; :: thesis: verum

end;

hence Roots (E,p) c= Roots (U,p) ; :: thesis: verum

end;

now :: thesis: ( Roots (E,p) c= Roots (U,p) implies p splits_in U )

assume Roots (E,p) c= Roots (U,p) ; :: thesis: p splits_in U
then Roots (E,p) c= the carrier of U by XBOOLE_1:1;
hence p splits_in U by AS, lemma6; :: thesis: verum

end;

hence ( p splits_in U iff Roots (E,p) c= Roots (U,p) ) by A; :: thesis: verum