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
for r1, r2 being Element of F st r1 = ((- b) + w) * ((2 '*' a) ") & r2 = ((- b) - w) * ((2 '*' a) ") holds
<%c,b,a%> = a * ((X- r1) *' (X- r2))
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
for r1, r2 being Element of F st r1 = ((- b) + w) * ((2 '*' a) ") & r2 = ((- b) - w) * ((2 '*' a) ") holds
<%c,b,a%> = a * ((X- r1) *' (X- r2))
let b, c be Element of F; :: thesis: for w being Element of F st w ^2 = (b ^2) - ((4 '*' a) * c) holds
for r1, r2 being Element of F st r1 = ((- b) + w) * ((2 '*' a) ") & r2 = ((- b) - w) * ((2 '*' a) ") holds
<%c,b,a%> = a * ((X- r1) *' (X- r2))
let w be Element of F; :: thesis: ( w ^2 = (b ^2) - ((4 '*' a) * c) implies for r1, r2 being Element of F st r1 = ((- b) + w) * ((2 '*' a) ") & r2 = ((- b) - w) * ((2 '*' a) ") holds
<%c,b,a%> = a * ((X- r1) *' (X- r2)) )
assume AS1: w ^2 = (b ^2) - ((4 '*' a) * c) ; :: thesis: for r1, r2 being Element of F st r1 = ((- b) + w) * ((2 '*' a) ") & r2 = ((- b) - w) * ((2 '*' a) ") holds
<%c,b,a%> = a * ((X- r1) *' (X- r2))
let r1, r2 be Element of F; :: thesis: ( r1 = ((- b) + w) * ((2 '*' a) ") & r2 = ((- b) - w) * ((2 '*' a) ") implies <%c,b,a%> = a * ((X- r1) *' (X- r2)) )
assume AS2: ( r1 = ((- b) + w) * ((2 '*' a) ") & r2 = ((- b) - w) * ((2 '*' a) ") ) ; :: thesis: <%c,b,a%> = a * ((X- r1) *' (X- r2))
(rpoly (1,r1)) *' (rpoly (1,r2)) = <%(r1 * r2),(- (r1 + r2)),(1. F)%> by lemred3z;
then A: <%(a * (r1 * r2)),(a * (- (r1 + r2))),(a * (1. F))%> = a * ((rpoly (1,r1)) *' (rpoly (1,r2))) by qua6;
Char F <> 2 by RING_3:def 6;
then I: 2 '*' (1. F) <> 0. F by REALALG2:24;

L: now :: thesis: not 4 '*' a = 0. F

assume 4 '*' a = 0. F ; :: thesis: contradiction
then 0. F = (2 * 2) '*' a
.= 2 '*' (2 '*' ((1. F) * a)) by RING_3:65
.= 2 '*' ((2 '*' (1. F)) * a) by REALALG2:5
.= 2 '*' (a * (2 '*' (1. F))) by GROUP_1:def 12
.= (2 '*' a) * (2 '*' (1. F)) by REALALG2:5 ;
then 2 '*' a = 0. F by I, VECTSP_2:def 1;
hence contradiction by ch2; :: thesis: verum

end;

then M: ( 2 '*' a <> 0. F & 4 '*' a <> 0. F & a <> 0. F ) by ch2;
B: a * (r1 * r2) = c

proof

(((- b) + w) * ((2 '*' a) ")) * (((- b) - w) * ((2 '*' a) ")) = (((2 '*' a) ") * ((- b) + w)) * (((- b) - w) * ((2 '*' a) ")) by GROUP_1:def 12
.= ((2 '*' a) ") * (((- b) + w) * (((- b) - w) * ((2 '*' a) "))) by GROUP_1:def 3
.= ((2 '*' a) ") * ((((- b) + w) * ((- b) - w)) * ((2 '*' a) ")) by GROUP_1:def 3
.= ((2 '*' a) ") * (((2 '*' a) ") * (((- b) + w) * ((- b) - w))) by GROUP_1:def 12
.= (((2 '*' a) ") * ((2 '*' a) ")) * (((- b) + w) * ((- b) - w)) by GROUP_1:def 3
.= (((2 '*' a) * (2 '*' a)) ") * (((- b) + w) * ((- b) - w)) by M, VECTSP_2:11
.= ((2 '*' (a * (2 '*' a))) ") * (((- b) + w) * ((- b) - w)) by REALALG2:5
.= ((2 '*' ((2 '*' a) * a)) ") * (((- b) + w) * ((- b) - w)) by GROUP_1:def 12
.= ((2 '*' (2 '*' (a * a))) ") * (((- b) + w) * ((- b) - w)) by REALALG2:5
.= (((2 * 2) '*' (a * a)) ") * (((- b) + w) * ((- b) - w)) by RING_3:65
.= ((4 '*' (a * a)) ") * (((- b) ^2) - ((b ^2) - ((4 '*' a) * c))) by AS1, REALALG2:9
.= ((4 '*' (a * a)) ") * (((- b) * (- b)) - ((b ^2) - ((4 '*' a) * c))) by O_RING_1:def 1
.= ((4 '*' (a * a)) ") * ((b * b) - ((b ^2) - ((4 '*' a) * c))) by VECTSP_1:10
.= ((4 '*' (a * a)) ") * ((b ^2) - ((b ^2) - ((4 '*' a) * c))) by O_RING_1:def 1
.= ((4 '*' (a * a)) ") * (((b ^2) - (b ^2)) + ((4 '*' a) * c)) by RLVECT_1:29
.= ((4 '*' (a * a)) ") * ((0. F) + ((4 '*' a) * c)) by RLVECT_1:15
.= (((4 '*' a) * a) ") * ((4 '*' a) * c) by REALALG2:5
.= ((a ") * ((4 '*' a) ")) * ((4 '*' a) * c) by L, VECTSP_2:11
.= (a ") * (((4 '*' a) ") * ((4 '*' a) * c)) by GROUP_1:def 3
.= (a ") * ((((4 '*' a) ") * (4 '*' a)) * c) by GROUP_1:def 3
.= (a ") * ((1. F) * c) by L, VECTSP_1:def 10 ;
hence a * (r1 * r2) = (a * (a ")) * c by AS2, GROUP_1:def 3
.= ((a ") * a) * c by GROUP_1:def 12
.= (1. F) * c by I, VECTSP_1:def 10
.= c ;
:: thesis: verum

end;

a * (- (r1 + r2)) = b

proof

per cases ( b = 0. F or b <> 0. F ) ;

suppose C0: b = 0. F ; :: thesis: a * (- (r1 + r2)) = b

(((- b) + w) * ((2 '*' a) ")) + (((- b) - w) * ((2 '*' a) ")) = (w + (- w)) * ((2 '*' a) ") by C0, VECTSP_1:def 3
.= (0. F) * ((2 '*' a) ") by RLVECT_1:5 ;
hence a * (- (r1 + r2)) = b by C0, AS2; :: thesis: verum

end;

suppose C1: b <> 0. F ; :: thesis: a * (- (r1 + r2)) = b

0. F = - (0. F) ;
then - b <> 0. F by C1;
then C: 2 '*' (- b) <> 0. F by ch2;
(((- b) + w) * ((2 '*' a) ")) + (((- b) - w) * ((2 '*' a) ")) = (((- b) + w) + ((- b) - w)) * ((2 '*' a) ") by VECTSP_1:def 3
.= ((- b) + (w + ((- b) + (- w)))) * ((2 '*' a) ") by RLVECT_1:def 3
.= ((- b) + ((w + (- w)) + (- b))) * ((2 '*' a) ") by RLVECT_1:def 3
.= ((- b) + ((0. F) + (- b))) * ((2 '*' a) ") by RLVECT_1:5
.= (2 '*' (- b)) * ((2 '*' a) ") by RING_5:2
.= (- b) * (a ") by M, C, ch0a ;
then - (r1 + r2) = (- (- b)) * (a ") by AS2, VECTSP_1:9;
hence a * (- (r1 + r2)) = a * ((a ") * b) by GROUP_1:def 12
.= (a * (a ")) * b by GROUP_1:def 3
.= ((a ") * a) * b by GROUP_1:def 12
.= (1. F) * b by I, VECTSP_1:def 10
.= b ;
:: thesis: verum

end;

end;

end;

hence <%c,b,a%> = a * ((X- r1) *' (X- r2)) by A, B; :: thesis: verum