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= the carrier of U )
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= the carrier of U )
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= the carrier of U )
let E be U -extending FieldExtension of F; :: thesis: ( p splits_in E implies ( p splits_in U iff Roots (E,p) c= the carrier of U ) )
assume AS: p splits_in E ; :: thesis: ( p splits_in U iff Roots (E,p) c= the carrier of U )

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

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

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

let o be object ; :: thesis: ( o in Roots (E,p) implies o in the carrier of U )
assume o in Roots (E,p) ; :: thesis: o in the carrier of U
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;
hence o in the carrier of U by A2; :: thesis: verum

end;

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

end;

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

assume B1: Roots (E,p) c= the carrier of U ; :: thesis: p splits_in U

now :: thesis: for a being Element of E st a is_a_root_of p,E holds
a in U

let a be Element of E; :: thesis: ( a is_a_root_of p,E implies a in U )
assume a is_a_root_of p,E ; :: thesis: a in U
then a in { a where a is Element of E : a is_a_root_of p,E } ;
then a in Roots (E,p) by FIELD_4:def 4;
hence a in U by B1; :: thesis: verum

end;

hence p splits_in U by AS, lemma2; :: thesis: verum

end;

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