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:47
.= - (2 * (u2 - u1)) by RLVECT_1:48
.= 2 * (- (u2 - u1)) by RLVECT_1:39
.= (- 2) * (u2 - u1) by RLVECT_1:38 ;
((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, Th33
.= ((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, Th33
.= (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, Th32 ;
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, Th33;
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;