let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for u, u', u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st u <> u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y & u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y & u1,u2 // v1,v2 holds
t1,t2 // w1,w2
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, u', u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st u <> u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y & u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y & u1,u2 // v1,v2 holds
t1,t2 // w1,w2 )
assume A1: Gen w,y ; :: thesis: for u, u', u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st u <> u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y & u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y & u1,u2 // v1,v2 holds
t1,t2 // w1,w2
let u, u', u1, u2, v1, v2, t1, t2, w1, w2 be VECTOR of V; :: thesis: ( u <> u' & u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y & u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y & u1,u2 // v1,v2 implies t1,t2 // w1,w2 )
assume that
A2: u <> u' and
A3: ( u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y & u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y ) and
A4: u1,u2 // v1,v2 ; :: thesis: t1,t2 // w1,w2
set A1 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) * ((PProJ w,y,(u - u'),(u - u')) " );
set A2 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) * ((PProJ w,y,(u - u'),(u - u')) " );
set A3 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),v1))) * ((PProJ w,y,(u - u'),(u - u')) " );
set A4 = ((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),v2))) * ((PProJ w,y,(u - u'),(u - u')) " );
A5: ( u1 + ((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) * ((PProJ w,y,(u - u'),(u - u')) " )) * (u - u')) = t1 & u2 + ((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) * ((PProJ w,y,(u - u'),(u - u')) " )) * (u - u')) = t2 & v1 + ((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),v1))) * ((PProJ w,y,(u - u'),(u - u')) " )) * (u - u')) = w1 & v2 + ((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),v2))) * ((PProJ w,y,(u - u'),(u - u')) " )) * (u - u')) = w2 ) by A1, A2, A3, Th38;
A6: ( t1 = u1 + ((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) * ((PProJ w,y,(u - u'),(u - u')) " )) * (u - u')) & t2 = u2 + ((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) * ((PProJ w,y,(u - u'),(u - u')) " )) * (u - u')) ) by A1, A2, A3, Th38;

A7: now

assume u1 = u2 ; :: thesis: t1,t2 // w1,w2
then t1 = t2 by A1, A2, A3, Th26;
hence t1,t2 // w1,w2 by ANALOAF:def 1; :: thesis: verum

end;

A8: now

assume v1 = v2 ; :: thesis: t1,t2 // w1,w2
then w1 = w2 by A1, A2, A3, Th26;
hence t1,t2 // w1,w2 by ANALOAF:def 1; :: thesis: verum

end;

now

assume ( u1 <> u2 & v1 <> v2 ) ; :: thesis: t1,t2 // w1,w2
then consider a, b being Real such that
A9: ( a * (u2 - u1) = b * (v2 - v1) & 0 < a & 0 < b ) by A4, ANALOAF:16;
set uu = (- 2) * (PProJ w,y,(u - u'),(u2 - u1));
set vv = (- 2) * (PProJ w,y,(u - u'),(v2 - v1));
set cc = (PProJ w,y,(u - u'),(u - u')) " ;
A10: a * ((- 2) * (PProJ w,y,(u - u'),(u2 - u1))) = b * ((- 2) * (PProJ w,y,(u - u'),(v2 - v1)))

proof

thus a * ((- 2) * (PProJ w,y,(u - u'),(u2 - u1))) = (- 2) * (a * (PProJ w,y,(u - u'),(u2 - u1)))
.= (- 2) * (PProJ w,y,(u - u'),(b * (v2 - v1))) by A1, A9, Th33
.= (- 2) * (b * (PProJ w,y,(u - u'),(v2 - v1))) by A1, Th33
.= b * ((- 2) * (PProJ w,y,(u - u'),(v2 - v1))) ; :: thesis: verum

end;

A11: a * ((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) * ((PProJ w,y,(u - u'),(u - u')) " )) - (((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) * ((PProJ w,y,(u - u'),(u - u')) " ))) = b * ((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),v2))) * ((PProJ w,y,(u - u'),(u - u')) " )) - (((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),v1))) * ((PProJ w,y,(u - u'),(u - u')) " )))

proof

thus a * ((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) * ((PProJ w,y,(u - u'),(u - u')) " )) - (((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) * ((PProJ w,y,(u - u'),(u - u')) " ))) = a * (((- 2) * (PProJ w,y,(u - u'),(u2 - u1))) * ((PProJ w,y,(u - u'),(u - u')) " )) by A1, A2, A6, Lm20
.= (b * ((- 2) * (PProJ w,y,(u - u'),(v2 - v1)))) * ((PProJ w,y,(u - u'),(u - u')) " ) by A10, XCMPLX_1:4
.= b * (((- 2) * (PProJ w,y,(u - u'),(v2 - v1))) * ((PProJ w,y,(u - u'),(u - u')) " ))
.= b * ((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),v2))) * ((PProJ w,y,(u - u'),(u - u')) " )) - (((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),v1))) * ((PProJ w,y,(u - u'),(u - u')) " ))) by A1, A2, A5, Lm20 ; :: thesis: verum

end;

A12: t2 - t1 = (u2 - u1) + (((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) * ((PProJ w,y,(u - u'),(u - u')) " )) - (((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) * ((PProJ w,y,(u - u'),(u - u')) " ))) * (u - u')) by A1, A2, A5, Lm20;
A13: w2 - w1 = (v2 - v1) + (((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),v2))) * ((PProJ w,y,(u - u'),(u - u')) " )) - (((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),v1))) * ((PProJ w,y,(u - u'),(u - u')) " ))) * (u - u')) by A1, A2, A5, Lm20;
a * (t2 - t1) = (a * (u2 - u1)) + (a * (((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u2))) * ((PProJ w,y,(u - u'),(u - u')) " )) - (((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),u1))) * ((PProJ w,y,(u - u'),(u - u')) " ))) * (u - u'))) by A12, RLVECT_1:def 9
.= (b * (v2 - v1)) + ((b * ((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),v2))) * ((PProJ w,y,(u - u'),(u - u')) " )) - (((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),v1))) * ((PProJ w,y,(u - u'),(u - u')) " )))) * (u - u')) by A9, A11, RLVECT_1:def 9
.= (b * (v2 - v1)) + (b * (((((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),v2))) * ((PProJ w,y,(u - u'),(u - u')) " )) - (((PProJ w,y,(u - u'),(u + u')) - (2 * (PProJ w,y,(u - u'),v1))) * ((PProJ w,y,(u - u'),(u - u')) " ))) * (u - u'))) by RLVECT_1:def 9
.= b * (w2 - w1) by A13, RLVECT_1:def 9 ;
hence t1,t2 // w1,w2 by A9, ANALOAF:def 1; :: thesis: verum

end;

hence t1,t2 // w1,w2 by A7, A8; :: thesis: verum