let F be non 2 -characteristic Field; :: thesis: for p being quadratic Polynomial of F holds
( Roots p <> {} iff DC p is square )
let p be quadratic Polynomial of F; :: thesis: ( Roots 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 Roots p <> {} )

assume DC p is square ; :: thesis: Roots p <> {}
then (b ^2) - ((4 '*' a) * c) is being_a_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;
((- b) + w) * ((2 '*' a) ") is_a_root_of p by A, B1, lemeval;
hence Roots p <> {} by POLYNOM5:def 10; :: thesis: verum

end;

now :: thesis: ( Roots p <> {} implies DC p is square )

assume Roots p <> {} ; :: thesis: DC p is square
then (b ^2) - ((4 '*' a) * c) is square by A, lemeval2;
hence DC p is square by A, defDC; :: thesis: verum

end;

hence ( Roots p <> {} iff DC p is square ) by B; :: thesis: verum