let F be non 2 -characteristic Field; :: thesis: for a being non zero Element of F
for b, c, w being Element of F st w ^2 = (b ^2) - ((4 '*' a) * c) holds
Roots <%c,b,a%> = {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))}
let a be non zero Element of F; :: thesis: for b, c, w being Element of F st w ^2 = (b ^2) - ((4 '*' a) * c) holds
Roots <%c,b,a%> = {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))}
let b, c be Element of F; :: thesis: for w being Element of F st w ^2 = (b ^2) - ((4 '*' a) * c) holds
Roots <%c,b,a%> = {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))}
let w be Element of F; :: thesis: ( w ^2 = (b ^2) - ((4 '*' a) * c) implies Roots <%c,b,a%> = {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))} )
reconsider p = <%c,b,a%> as non zero Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
set r1 = ((- b) + w) * ((2 '*' a) ");
set r2 = ((- b) - w) * ((2 '*' a) ");
assume AS: w ^2 = (b ^2) - ((4 '*' a) * c) ; :: thesis: Roots <%c,b,a%> = {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))}
L: 2 '*' a <> 0. F by ch2;

C: now :: thesis: for o being object st o in Roots p holds
o in {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))}

let o be object ; :: thesis: ( o in Roots p implies b₁ in {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))} )
assume C1: o in Roots p ; :: thesis: b₁ in {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))}
then reconsider r = o as Element of F ;
r is_a_root_of p by C1, POLYNOM5:def 10;
then 0. F = (c + (b * r)) + (a * (r ^2)) by evalq
.= ((a * (r ^2)) + (b * r)) + c by RLVECT_1:def 3
.= ((a * (r ^2)) + (r * b)) + c by GROUP_1:def 12 ;
then 0. F = (4 '*' a) * (((a * (r ^2)) + (r * b)) + c)
.= ((4 '*' a) * ((a * (r ^2)) + (r * b))) + ((4 '*' a) * c) by VECTSP_1:def 2
.= (((4 '*' a) * (a * (r ^2))) + ((4 '*' a) * (r * b))) + ((4 '*' a) * c) by VECTSP_1:def 2
.= (((4 '*' a) * (a * (r ^2))) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c) by GROUP_1:def 3
.= ((((4 '*' a) * a) * (r ^2)) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c) by GROUP_1:def 3
.= (((4 '*' (a * a)) * (r ^2)) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c) by REALALG2:5
.= ((((2 * 2) '*' (a ^2)) * (r ^2)) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c) by O_RING_1:def 1
.= ((((2 ^2) '*' (a ^2)) * (r ^2)) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c) by SQUARE_1:def 1
.= ((((2 '*' a) ^2) * (r ^2)) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c) by ch1
.= ((((2 '*' a) * r) ^2) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c) by ch0 ;
then - ((4 '*' a) * c) = (((((2 '*' a) * r) ^2) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c)) - ((4 '*' a) * c)
.= ((((2 '*' a) * r) ^2) + (((4 '*' a) * r) * b)) + (((4 '*' a) * c) - ((4 '*' a) * c)) by RLVECT_1:def 3
.= ((((2 '*' a) * r) ^2) + (((4 '*' a) * r) * b)) + (0. F) by RLVECT_1:15 ;
then (b ^2) + (- ((4 '*' a) * c)) = ((((2 '*' a) * r) ^2) + (((2 * 2) '*' (a * r)) * b)) + (b ^2) by REALALG2:5
.= ((((2 '*' a) * r) ^2) + ((2 '*' (2 '*' (a * r))) * b)) + (b ^2) by RING_3:65
.= ((((2 '*' a) * r) ^2) + ((2 '*' ((2 '*' a) * r)) * b)) + (b ^2) by REALALG2:5
.= (((2 '*' a) * r) + b) ^2 by REALALG2:7 ;

per cases then ( w = ((2 '*' a) * r) + b or w = - (((2 '*' a) * r) + b) ) by AS, REALALG2:10;

suppose w = ((2 '*' a) * r) + b ; :: thesis: b₁ in {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))}

then (- b) + w = ((2 '*' a) * r) + (b + (- b)) by RLVECT_1:def 3
.= ((2 '*' a) * r) + (0. F) by RLVECT_1:5
.= (2 '*' a) * r ;
then ((2 '*' a) ") * ((- b) + w) = (((2 '*' a) ") * (2 '*' a)) * r by GROUP_1:def 3
.= (1. F) * r by L, VECTSP_1:def 10 ;
then r = ((- b) + w) * ((2 '*' a) ") by GROUP_1:def 12;
hence o in {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))} by TARSKI:def 2; :: thesis: verum

end;

suppose w = - (((2 '*' a) * r) + b) ; :: thesis: b₁ in {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))}

then (- b) + (- w) = ((2 '*' a) * r) + (b + (- b)) by RLVECT_1:def 3
.= ((2 '*' a) * r) + (0. F) by RLVECT_1:5
.= (2 '*' a) * r ;
then ((2 '*' a) ") * ((- b) + (- w)) = (((2 '*' a) ") * (2 '*' a)) * r by GROUP_1:def 3
.= (1. F) * r by L, VECTSP_1:def 10 ;
then r = ((- b) - w) * ((2 '*' a) ") by GROUP_1:def 12;
hence o in {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

now :: thesis: for o being object st o in {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))} holds
o in Roots p

let o be object ; :: thesis: ( o in {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))} implies b₁ in Roots p )
assume o in {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))} ; :: thesis: b₁ in Roots p

per cases then ( o = ((- b) + w) * ((2 '*' a) ") or o = ((- b) - w) * ((2 '*' a) ") ) by TARSKI:def 2;

suppose D: o = ((- b) + w) * ((2 '*' a) ") ; :: thesis: b₁ in Roots p

((- b) + w) * ((2 '*' a) ") is_a_root_of p by AS, lemeval;
hence o in Roots p by D, POLYNOM5:def 10; :: thesis: verum

end;

suppose D: o = ((- b) - w) * ((2 '*' a) ") ; :: thesis: b₁ in Roots p

((- b) - w) * ((2 '*' a) ") is_a_root_of p by AS, lemeval;
hence o in Roots p by D, POLYNOM5:def 10; :: thesis: verum

end;

end;

end;

hence Roots <%c,b,a%> = {(((- b) + w) * ((2 '*' a) ")),(((- b) - w) * ((2 '*' a) "))} by C, TARSKI:2; :: thesis: verum