let F be non 2 -characteristic Field; :: thesis: for p being quadratic Element of the carrier of (Polynom-Ring F) holds
( F is SplittingField of p iff DC p is square )
let p be quadratic Element of the carrier of (Polynom-Ring F); :: thesis: ( F is SplittingField of p iff DC p is square )
consider a being non zero Element of F, b, c being Element of F such that
A: p = <%c,b,a%> by qua5;

B: now :: thesis: ( DC p is square implies F is SplittingField of p )

assume DC p is square ; :: thesis: F is SplittingField of p
then (b ^2) - ((4 '*' a) * c) is square by A, defDC;
then consider w being Element of F such that
C: w ^2 = (b ^2) - ((4 '*' a) * c) by O_RING_1:def 2;
set r1 = ((- b) + w) * ((2 '*' a) ");
set r2 = ((- b) - w) * ((2 '*' a) ");
D: <%c,b,a%> = a * ((X- (((- b) + w) * ((2 '*' a) "))) *' (X- (((- b) - w) * ((2 '*' a) ")))) by C, lemred;
( rpoly (1,(((- b) + w) * ((2 '*' a) "))) is Ppoly of F & rpoly (1,(((- b) - w) * ((2 '*' a) "))) is Ppoly of F ) by RING_5:51;
then E: (rpoly (1,(((- b) + w) * ((2 '*' a) ")))) *' (rpoly (1,(((- b) - w) * ((2 '*' a) ")))) is Ppoly of F by RING_5:52;
F: F is FieldExtension of F by FIELD_4:6;

now :: thesis: for E being FieldExtension of F st p splits_in E & E is Subfield of F holds
E == F

let E be FieldExtension of F; :: thesis: ( p splits_in E & E is Subfield of F implies E == F )
assume F1: ( p splits_in E & E is Subfield of F ) ; :: thesis: E == F
F is Subfield of E by FIELD_4:7;
hence E == F by F1, FIELD_7:def 2; :: thesis: verum

end;

hence F is SplittingField of p by E, F, A, D, FIELD_4:def 5, FIELD_8:def 1; :: thesis: verum

end;

now :: thesis: ( F is SplittingField of p implies DC p is square )

assume F is SplittingField of p ; :: thesis: DC p is square
then p splits_in F by FIELD_8:def 1;
then consider x being non zero Element of F, q being Ppoly of F such that
G: p = x * q by FIELD_4:def 5;
Roots p <> {} by G;
then (b ^2) - ((4 '*' a) * c) is square by A, lemeval2;
hence DC p is square by A, defDC; :: thesis: verum

end;

hence ( F is SplittingField of p iff DC p is square ) by B; :: thesis: verum