let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st FAdj (F,(Roots (E,p))) is SplittingField of p
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ex E being FieldExtension of F st FAdj (F,(Roots (E,p))) is SplittingField of p
consider E being FieldExtension of F such that
A: p splits_in E by FIELD_5:31;
take E ; :: thesis: FAdj (F,(Roots (E,p))) is SplittingField of p
set K = FAdj (F,(Roots (E,p)));
thus p splits_in FAdj (F,(Roots (E,p))) by A, lemma5; :: according to FIELD_8:def 1 :: thesis: for E being FieldExtension of F st p splits_in E & E is Subfield of FAdj (F,(Roots (E,p))) holds
E == FAdj (F,(Roots (E,p)))

now :: thesis: for U being FieldExtension of F st U is Subfield of FAdj (F,(Roots (E,p))) & p splits_in U holds
FAdj (F,(Roots (E,p))) is Subfield of U

let U be FieldExtension of F; :: thesis: ( U is Subfield of FAdj (F,(Roots (E,p))) & p splits_in U implies FAdj (F,(Roots (E,p))) is Subfield of U )
assume B: ( U is Subfield of FAdj (F,(Roots (E,p))) & p splits_in U ) ; :: thesis: FAdj (F,(Roots (E,p))) is Subfield of U
C: U is Subfield of E by B, EC_PF_1:5;
then C1: E is FieldExtension of U by FIELD_4:7;
D: F is Subfield of U by FIELD_4:7;
E: Roots (U,p) c= Roots (E,p) by C1, lemma7;
Roots (E,p) c= Roots (U,p) by C1, A, B, lemma3;
then Roots (E,p) is Subset of U by E, XBOOLE_0:def 10;
hence FAdj (F,(Roots (E,p))) is Subfield of U by D, C, FIELD_6:37; :: thesis: verum

end;

hence for E being FieldExtension of F st p splits_in E & E is Subfield of FAdj (F,(Roots (E,p))) holds
E == FAdj (F,(Roots (E,p))) ; :: thesis: verum