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

per cases ( u1 = u2 or v1 = v2 or ( u1 <> u2 & v1 <> v2 ) ) ;

suppose u1 = u2 ; :: thesis: t1,t2 // w1,w2

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

end;

suppose v1 = v2 ; :: thesis: t1,t2 // w1,w2

then w1 = w2 by A1, A2, A4, Th24;
hence t1,t2 // w1,w2 by ANALOAF:def 1; :: thesis: verum

end;

suppose A9: ( u1 <> u2 & v1 <> v2 ) ; :: thesis: t1,t2 // w1,w2

set cc = (PProJ (w,y,(u - u9),(u - u9))) " ;
set vv = (- 2) * (PProJ (w,y,(u - u9),(v2 - v1)));
set uu = (- 2) * (PProJ (w,y,(u - u9),(u2 - u1)));
A10: w2 - w1 = (v2 - v1) + (((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)) by A1, A7, Lm21;
consider a, b being Real such that
A11: a * (u2 - u1) = b * (v2 - v1) and
A12: ( 0 < a & 0 < b ) by A5, A9, ANALOAF:7;
A13: a * ((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) = (- 2) * (a * (PProJ (w,y,(u - u9),(u2 - u1))))
.= (- 2) * (PProJ (w,y,(u - u9),(b * (v2 - v1)))) by A1, A11, Th31
.= (- 2) * (b * (PProJ (w,y,(u - u9),(v2 - v1)))) by A1, Th31
.= b * ((- 2) * (PProJ (w,y,(u - u9),(v2 - v1)))) ;
A14: a * ((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) = a * (((- 2) * (PProJ (w,y,(u - u9),(u2 - u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) by A1, A8, Lm21
.= (b * ((- 2) * (PProJ (w,y,(u - u9),(v2 - v1))))) * ((PProJ (w,y,(u - u9),(u - u9))) ") by A13, XCMPLX_1:4
.= b * (((- 2) * (PProJ (w,y,(u - u9),(v2 - v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))
.= b * ((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) by A1, A7, Lm21 ;
t2 - t1 = (u2 - u1) + (((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9)) by A1, A6, Lm21;
then a * (t2 - t1) = (a * (u2 - u1)) + (a * (((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),u1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9))) by RLVECT_1:def 5
.= (b * (v2 - v1)) + ((b * ((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")))) * (u - u9)) by A11, A14, RLVECT_1:def 7
.= (b * (v2 - v1)) + (b * (((((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v2)))) * ((PProJ (w,y,(u - u9),(u - u9))) ")) - (((PProJ (w,y,(u - u9),(u + u9))) - (2 * (PProJ (w,y,(u - u9),v1)))) * ((PProJ (w,y,(u - u9),(u - u9))) "))) * (u - u9))) by RLVECT_1:def 7
.= b * (w2 - w1) by A10, RLVECT_1:def 5 ;
hence t1,t2 // w1,w2 by A12, ANALOAF:def 1; :: thesis: verum

end;

end;