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) = 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) = 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) = 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) = Roots (U,p) ) )
assume AS: p splits_in E ; :: thesis: ( p splits_in U iff Roots (E,p) = Roots (U,p) )

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

assume p splits_in U ; :: thesis: Roots (E,p) = Roots (U,p)
then B: Roots (E,p) c= Roots (U,p) by AS, lemma3;
Roots (U,p) c= Roots (E,p) by lemma7;
hence Roots (E,p) = Roots (U,p) by B, XBOOLE_0:def 10; :: thesis: verum

end;

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