let F be non 2 -characteristic Field; :: thesis: for p being quadratic Polynomial of F holds
( card (Roots p) = 2 iff ( not DC p is zero & DC p is square ) )
let p be quadratic Polynomial of F; :: thesis: ( card (Roots p) = 2 iff ( not DC p is zero & 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;
L: 2 '*' a <> 0. F by ch2;

B: now :: thesis: ( card (Roots p) = 2 implies ( not DC p is zero & DC p is square ) )

assume B0: card (Roots p) = 2 ; :: thesis: ( not DC p is zero & DC p is square )
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;

B3: now :: thesis: not ((- b) + w) * ((2 '*' a) ") = ((- b) - w) * ((2 '*' a) ")

assume ((- b) + w) * ((2 '*' a) ") = ((- b) - w) * ((2 '*' a) ") ; :: thesis: contradiction
then Roots p = {(((- b) + w) * ((2 '*' a) "))} by B2, ENUMSET1:29;
hence contradiction by B0, CARD_2:42; :: thesis: verum

end;

now :: thesis: not (b ^2) - ((4 '*' a) * c) = 0. F

assume (b ^2) - ((4 '*' a) * c) = 0. F ; :: thesis: contradiction
then w * w = 0. F by B1, O_RING_1:def 1;
then w = 0. F by VECTSP_2:def 1;
hence contradiction by B3; :: thesis: verum

end;

hence ( not DC p is zero & DC p is square ) by A, defDC, B1; :: thesis: verum

end;

now :: thesis: ( not DC p is zero & DC p is square implies card (Roots p) = 2 )

assume C0: ( not DC p is zero & DC p is square ) ; :: thesis: card (Roots p) = 2
then (b ^2) - ((4 '*' a) * c) is square by A, defDC;
then consider w being Element of F such that
C1: w ^2 = (b ^2) - ((4 '*' a) * c) by O_RING_1:def 2;
C2: Roots <%c,b,a%> = {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))} by C1, TC0;

now :: thesis: not ((- b) + w) * ((2 '*' a) ") = ((- b) - w) * ((2 '*' a) ")

assume ((- b) + w) * ((2 '*' a) ") = ((- b) - w) * ((2 '*' a) ") ; :: thesis: contradiction
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 contradiction by C0, C1, A, defDC; :: thesis: verum

end;

hence card (Roots p) = 2 by A, C2, CARD_2:57; :: thesis: verum

end;

hence ( card (Roots p) = 2 iff ( not DC p is zero & DC p is square ) ) by B; :: thesis: verum