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

proof

set uu = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) - ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),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 - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) - ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) = ((PProJ w,y,(u - u'),(u + u')) - (PProJ w,y,(u - u'),(2 * u2))) - ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) by A1, Th33
.= ((PProJ w,y,(u - u'),(u + u')) - (PProJ w,y,(u - u'),(2 * u2))) - ((PProJ w,y,(u - u'),(u + u')) - (PProJ w,y,(u - u'),(2 * u1))) by A1, Th33
.= (PProJ w,y,(u - u'),(2 * u1)) - (PProJ w,y,(u - u'),(2 * u2))
.= PProJ w,y,(u - u'),((2 * u1) - (2 * u2)) by A1, Th32 ;
then ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) - ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) = (- 2) * (PProJ w,y,(u - u'),(u2 - u1)) by A1, A3, Th33;
hence ( t2 - t1 = (u2 - u1) + ((A2 - A1) * (u - u')) & A2 - A1 = ((- 2) * (PProJ w,y,(u - u'),(u2 - u1))) * ((PProJ w,y,(u - u'),(u - u')) " ) ) by A2, Lm20, XCMPLX_1:40; :: thesis: verum

end;