let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F st p splits_in E holds
FAdj (F,(Roots (E,p))) is SplittingField of p
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: for E being FieldExtension of F st p splits_in E holds
FAdj (F,(Roots (E,p))) is SplittingField of p
let E be FieldExtension of F; :: thesis: ( p splits_in E implies FAdj (F,(Roots (E,p))) is SplittingField of p )
assume AS: p splits_in 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 AS, 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, AS, 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