let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field; :: thesis: for a being non square Element of F holds FAdj (F,{(sqrt a)}) is SplittingField of X^2- a
let a be non square Element of F; :: thesis: FAdj (F,{(sqrt a)}) is SplittingField of X^2- a
set E = FAdj (F,{(sqrt a)});
reconsider p = X^2- a as Element of the carrier of (Polynom-Ring F) ;
reconsider b = sqrt a as Element of (FAdj (F,{(sqrt a)})) by FIELD_7:def 5;
reconsider q = (rpoly (1,b)) *' (rpoly (1,(- b))) as Element of the carrier of (Polynom-Ring (FAdj (F,{(sqrt a)}))) by POLYNOM3:def 10;
FAdj (F,{(sqrt a)}) is Subring of embField (canHomP (X^2- a)) by FIELD_4:def 1;
then H: - b = - (sqrt a) by FIELD_6:17;
I: X- b = X- (sqrt a) by FIELD_4:21;
K: X+ b = X+ (sqrt a) by H, FIELD_4:21;
(rpoly (1,b)) *' (rpoly (1,(- b))) = (X- (sqrt a)) *' (X+ (sqrt a)) by I, K, FIELD_4:17
.= X^2- a by Fi1a ;
then D: X^2- a = (1. (FAdj (F,{(sqrt a)}))) * q ;
( rpoly (1,b) is Ppoly of FAdj (F,{(sqrt a)}) & rpoly (1,(- b)) is Ppoly of FAdj (F,{(sqrt a)}) ) by RING_5:51;
then q is Ppoly of FAdj (F,{(sqrt a)}) by RING_5:52;
then A: X^2- a splits_in FAdj (F,{(sqrt a)}) by D, FIELD_4:def 5;

now :: thesis: for U being FieldExtension of F st X^2- a splits_in U & U is Subfield of FAdj (F,{(sqrt a)}) holds
FAdj (F,{(sqrt a)}) == U

let U be FieldExtension of F; :: thesis: ( X^2- a splits_in U & U is Subfield of FAdj (F,{(sqrt a)}) implies FAdj (F,{(sqrt a)}) == U )
assume D0: ( X^2- a splits_in U & U is Subfield of FAdj (F,{(sqrt a)}) ) ; :: thesis: FAdj (F,{(sqrt a)}) == U
then D3: FAdj (F,{(sqrt a)}) is U -extending by FIELD_4:7;
D4: Roots ((FAdj (F,{(sqrt a)})),(X^2- a)) c= the carrier of U by D3, D0, A, FIELD_8:27;
Roots ((FAdj (F,{(sqrt a)})),p) = {(sqrt a),(- (sqrt a))} by Fi2a;
then sqrt a in Roots ((FAdj (F,{(sqrt a)})),p) by TARSKI:def 2;
then sqrt a in the carrier of U by D4;
then D1: {(sqrt a)} c= the carrier of U by TARSKI:def 1;
D2: U is Subfield of embField (canHomP (X^2- a)) by D0, EC_PF_1:5;
F is Subfield of U by FIELD_4:7;
then FAdj (F,{(sqrt a)}) is Subfield of U by D1, D2, FIELD_6:37;
hence FAdj (F,{(sqrt a)}) == U by D0, FIELD_7:def 2; :: thesis: verum

end;

hence FAdj (F,{(sqrt a)}) is SplittingField of X^2- a by A, FIELD_8:def 1; :: thesis: verum