let F be Field; :: thesis:
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis:
let U be FieldExtension of F; :: thesis:
let E be U -extending FieldExtension of F; :: thesis:
assume AS: p splits_in E ; :: thesis:

A: now :: thesis:

assume A1: p splits_in U ; :: thesis:

now :: thesis:

let o be object ; :: thesis:
assume o in Roots (E,p) ; :: thesis:
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:

end;

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

end;

now :: thesis:

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

now :: thesis:

let a be Element of E; :: thesis:
assume a is_a_root_of p,E ; :: thesis:
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:

end;

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

end;

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