let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for u, u9, u1, u2, t1, t2 being VECTOR of V
for A1, A2 being Real st A1 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & A2 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & t1 = u1 + (A1 * (u - u9)) & t2 = u2 + (A2 * (u - u9)) holds
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") )
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, u9, u1, u2, t1, t2 being VECTOR of V
for A1, A2 being Real st A1 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & A2 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & t1 = u1 + (A1 * (u - u9)) & t2 = u2 + (A2 * (u - u9)) holds
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") ) )
assume A1: Gen w,y ; :: thesis: for u, u9, u1, u2, t1, t2 being VECTOR of V
for A1, A2 being Real st A1 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & A2 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & t1 = u1 + (A1 * (u - u9)) & t2 = u2 + (A2 * (u - u9)) holds
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") )
let u, u9, u1, u2, t1, t2 be VECTOR of V; :: thesis: for A1, A2 being Real st A1 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & A2 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & t1 = u1 + (A1 * (u - u9)) & t2 = u2 + (A2 * (u - u9)) holds
( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") )
let A1, A2 be Real; :: thesis: ( A1 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & A2 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & t1 = u1 + (A1 * (u - u9)) & t2 = u2 + (A2 * (u - u9)) implies ( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") ) )
assume A2: ( A1 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & A2 = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") & t1 = u1 + (A1 * (u - u9)) & t2 = u2 + (A2 * (u - u9)) ) ; :: thesis: ( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") )
thus ( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") ) :: thesis: verum

proof

set uu = ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) - ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1))));
A3: (2 * u1) - (2 * u2) = - ((2 * u2) - (2 * u1)) by RLVECT_1:33
.= - (2 * (u2 - u1)) by RLVECT_1:34
.= 2 * (- (u2 - u1)) by RLVECT_1:25
.= (- 2) * (u2 - u1) by RLVECT_1:24 ;
((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) - ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) = ((PProJ (w,y,(u - u9),(u + u9))) - (PProJ (w,y,(u - u9),(2 * u2)))) - ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) by A1, Th31
.= ((PProJ (w,y,(u - u9),(u + u9))) - (PProJ (w,y,(u - u9),(2 * u2)))) - ((PProJ (w,y,(u - u9),(u + u9))) - (PProJ (w,y,(u - u9),(2 * u1)))) by A1, Th31
.= (PProJ (w,y,(u - u9),(2 * u1))) - (PProJ (w,y,(u - u9),(2 * u2)))
.= PProJ (w,y,(u - u9),((2 * u1) - (2 * u2))) by A1, Th30 ;
then ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) - ((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) = (- 2) * (PProJ (w,y,(u - u9),(u2 - u1))) by A1, A3, Th31;
hence ( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u9)) & A2 - A1 = ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ") ) by A2, Lm20, XCMPLX_1:40; :: thesis: verum

end;