let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field; :: thesis: for p being quadratic non DC-square Element of the carrier of (Polynom-Ring F) holds FAdj (F,{(sqrt (DC p))}) is SplittingField of p
let p be quadratic non DC-square Element of the carrier of (Polynom-Ring F); :: thesis: FAdj (F,{(sqrt (DC p))}) is SplittingField of p
set E = FAdj (F,{(sqrt (DC p))});
set r1 = Root1 p;
set r2 = Root2 p;
reconsider q = (rpoly (1,(Root1 p))) *' (rpoly (1,(Root2 p))) as Element of the carrier of (Polynom-Ring (FAdj (F,{(sqrt (DC p))}))) by POLYNOM3:def 10;
K: F is Subring of FAdj (F,{(sqrt (DC p))}) by FIELD_4:def 1;

Y: now :: thesis: not @ ((LC p),(FAdj (F,{(sqrt (DC p))}))) is zero

assume Y1: @ ((LC p),(FAdj (F,{(sqrt (DC p))}))) is zero ; :: thesis: contradiction
LC p = @ ((LC p),(FAdj (F,{(sqrt (DC p))}))) by FIELD_7:def 4
.= 0. F by Y1, K, C0SP1:def 3 ;
hence contradiction ; :: thesis: verum

end;

(rpoly (1,(Root1 p))) *' (rpoly (1,(Root2 p))) = (X- (Root1 p)) *' (X- (Root2 p)) ;
then D: p = (@ ((LC p),(FAdj (F,{(sqrt (DC p))})))) * ((rpoly (1,(Root1 p))) *' (rpoly (1,(Root2 p)))) by Z5;
( rpoly (1,(Root1 p)) is Ppoly of FAdj (F,{(sqrt (DC p))}) & rpoly (1,(Root2 p)) is Ppoly of FAdj (F,{(sqrt (DC p))}) ) by RING_5:51;
then (rpoly (1,(Root1 p))) *' (rpoly (1,(Root2 p))) is Ppoly of FAdj (F,{(sqrt (DC p))}) by RING_5:52;
then A: p splits_in FAdj (F,{(sqrt (DC p))}) by Y, D, FIELD_4:def 5;

now :: thesis: for U being FieldExtension of F st p splits_in U & U is Subfield of FAdj (F,{(sqrt (DC p))}) holds
U == FAdj (F,{(sqrt (DC p))})

let U be FieldExtension of F; :: thesis: ( p splits_in U & U is Subfield of FAdj (F,{(sqrt (DC p))}) implies U == FAdj (F,{(sqrt (DC p))}) )
assume D0: ( p splits_in U & U is Subfield of FAdj (F,{(sqrt (DC p))}) ) ; :: thesis: U == FAdj (F,{(sqrt (DC p))})
then D3: ( FAdj (F,{(sqrt (DC p))}) is U -extending & U is Subring of FAdj (F,{(sqrt (DC p))}) ) by FIELD_5:12, FIELD_4:7;
D4: Roots ((FAdj (F,{(sqrt (DC p))})),p) c= the carrier of U by D3, D0, A, FIELD_8:27;
Roots ((FAdj (F,{(sqrt (DC p))})),p) = {(Root1 p),(Root2 p)} by Z4;
then Root1 p in Roots ((FAdj (F,{(sqrt (DC p))})),p) by TARSKI:def 2;
then reconsider w = Root1 p as Element of U by D4;
sqrt (DC p) in the carrier of U

proof

consider aF being non zero Element of F, bF, cF being Element of F such that
A1: p = <%cF,bF,aF%> by qua5;
set aE = @ (aF,(FAdj (F,{(sqrt (DC p))})));
set bE = @ (bF,(FAdj (F,{(sqrt (DC p))})));
set cE = @ (cF,(FAdj (F,{(sqrt (DC p))})));

C1: now :: thesis: not @ (aF,(FAdj (F,{(sqrt (DC p))}))) is zero

assume C2: @ (aF,(FAdj (F,{(sqrt (DC p))}))) is zero ; :: thesis: contradiction
aF = 0. (FAdj (F,{(sqrt (DC p))})) by C2, FIELD_7:def 4
.= 0. F by K, C0SP1:def 3 ;
hence contradiction ; :: thesis: verum

end;

not FAdj (F,{(sqrt (DC p))}) is 2 -characteristic by K;
then C3: 2 '*' (@ (aF,(FAdj (F,{(sqrt (DC p))})))) <> 0. (FAdj (F,{(sqrt (DC p))})) by C1, ch2;
I1: ( @ (aF,(FAdj (F,{(sqrt (DC p))}))) = aF & @ (bF,(FAdj (F,{(sqrt (DC p))}))) = bF & @ (cF,(FAdj (F,{(sqrt (DC p))}))) = cF ) by FIELD_7:def 4;
then p = <%(@ (cF,(FAdj (F,{(sqrt (DC p))})))),(@ (bF,(FAdj (F,{(sqrt (DC p))})))),(@ (aF,(FAdj (F,{(sqrt (DC p))}))))%> by A1, eval2;
then Root1 p = ((- (@ (bF,(FAdj (F,{(sqrt (DC p))}))))) + (RootDC p)) * ((2 '*' (@ (aF,(FAdj (F,{(sqrt (DC p))}))))) ") by C1, Z2;
then (Root1 p) * (2 '*' (@ (aF,(FAdj (F,{(sqrt (DC p))}))))) = ((- (@ (bF,(FAdj (F,{(sqrt (DC p))}))))) + (RootDC p)) * (((2 '*' (@ (aF,(FAdj (F,{(sqrt (DC p))}))))) ") * (2 '*' (@ (aF,(FAdj (F,{(sqrt (DC p))})))))) by GROUP_1:def 3
.= ((- (@ (bF,(FAdj (F,{(sqrt (DC p))}))))) + (RootDC p)) * (1. (FAdj (F,{(sqrt (DC p))}))) by C3, VECTSP_1:def 10 ;
then B: (@ (bF,(FAdj (F,{(sqrt (DC p))})))) + ((Root1 p) * (2 '*' (@ (aF,(FAdj (F,{(sqrt (DC p))})))))) = ((@ (bF,(FAdj (F,{(sqrt (DC p))})))) + (- (@ (bF,(FAdj (F,{(sqrt (DC p))})))))) + (RootDC p) by RLVECT_1:def 3
.= (0. (FAdj (F,{(sqrt (DC p))}))) + (RootDC p) by RLVECT_1:5 ;
set aU = @ (aF,U);
set bU = @ (bF,U);
set cU = @ (cF,U);
I2: ( @ (aF,U) = aF & @ (bF,U) = bF & @ (cF,U) = cF ) by FIELD_7:def 4;
2 '*' (@ (aF,U)) = 2 '*' (@ (aF,(FAdj (F,{(sqrt (DC p))})))) by D3, I2, Z3, FIELD_7:def 4;
then w * (2 '*' (@ (aF,U))) = (Root1 p) * (2 '*' (@ (aF,(FAdj (F,{(sqrt (DC p))}))))) by D3, FIELD_6:16;
then (@ (bF,U)) + (w * (2 '*' (@ (aF,U)))) = (@ (bF,(FAdj (F,{(sqrt (DC p))})))) + ((Root1 p) * (2 '*' (@ (aF,(FAdj (F,{(sqrt (DC p))})))))) by D3, I1, I2, FIELD_6:15;
hence sqrt (DC p) in the carrier of U by B; :: thesis: verum

end;

then D1: {(sqrt (DC p))} c= the carrier of U by TARSKI:def 1;
D2: U is Subfield of embField (canHomP (X^2- (DC p))) by D0, EC_PF_1:5;
F is Subfield of U by FIELD_4:7;
then FAdj (F,{(sqrt (DC p))}) is Subfield of U by D1, D2, FIELD_6:37;
hence U == FAdj (F,{(sqrt (DC p))}) by D0, FIELD_7:def 2; :: thesis: verum

end;

hence FAdj (F,{(sqrt (DC p))}) is SplittingField of p by A, FIELD_8:def 1; :: thesis: verum