let F be non 2 -characteristic Field; :: thesis: for p being quadratic Polynomial of F holds
( card (Roots p) = 1 iff DC p = 0. F )
let p be quadratic Polynomial of F; :: thesis: ( card (Roots p) = 1 iff DC p = 0. F )
consider a being non zero Element of F, b, c being Element of F such that
A: p = <%c,b,a%> by qua5;
set r = the Element of Roots p;

B: now :: thesis: ( DC p = 0. F implies card (Roots p) = 1 )

assume DC p = 0. F ; :: thesis: card (Roots p) = 1
then B0: (b ^2) - ((4 '*' a) * c) = 0. F by A, defDC;
then consider w being Element of F such that
B1: (b ^2) - ((4 '*' a) * c) = w ^2 by O_RING_1:def 2;
B2: Roots p = {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))} by B1, A, TC0;
0. F = w * w by B0, B1, O_RING_1:def 1;
then w = 0. F by VECTSP_2:def 1;
then Roots p = {(((- b) + w) * ((2 '*' a) "))} by B2, ENUMSET1:29;
hence card (Roots p) = 1 by CARD_1:30; :: thesis: verum

end;

L: 2 '*' a <> 0. F by ch2;

now :: thesis: ( card (Roots p) = 1 implies DC p = 0. F )

assume B0: card (Roots p) = 1 ; :: thesis: DC p = 0. F
then Roots p <> {} ;
then DC p is square by TC1;
then (b ^2) - ((4 '*' a) * c) is square by A, defDC;
then consider w being Element of F such that
B1: (b ^2) - ((4 '*' a) * c) = w ^2 by O_RING_1:def 2;
B2: Roots p = {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))} by B1, A, TC0;
((- b) + w) * ((2 '*' a) ") = ((- b) - w) * ((2 '*' a) ") by B0, B2, CARD_2:57;
then (((- b) + w) * ((2 '*' a) ")) * (2 '*' a) = ((- b) - w) * (((2 '*' a) ") * (2 '*' a)) by GROUP_1:def 3
.= ((- b) - w) * (1. F) by L, VECTSP_1:def 10 ;
then (- b) - w = ((- b) + w) * (((2 '*' a) ") * (2 '*' a)) by GROUP_1:def 3
.= ((- b) + w) * (1. F) by L, VECTSP_1:def 10 ;
then b + ((- b) - w) = (b + (- b)) + w by RLVECT_1:def 3
.= (0. F) + w by RLVECT_1:5 ;
then w = (b + (- b)) + (- w) by RLVECT_1:def 3
.= (0. F) + (- w) by RLVECT_1:5 ;
then w + w = 0. F by RLVECT_1:5;
then 2 '*' w = 0. F by RING_5:2;
then w = 0. F by ch2;
hence DC p = 0. F by B1, A, defDC; :: thesis: verum

end;

hence ( card (Roots p) = 1 iff DC p = 0. F ) by B; :: thesis: verum