let V be RealLinearSpace; :: thesis: for w, y, u, u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st Gen w,y & u = u1 # t1 & u = u2 # t2 & u = v1 # w1 & u = v2 # w2 & u1,u2,v1,v2 are_DTr_wrt w,y holds
t1,t2,w1,w2 are_DTr_wrt w,y
let w, y be VECTOR of V; :: thesis: for u, u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st Gen w,y & u = u1 # t1 & u = u2 # t2 & u = v1 # w1 & u = v2 # w2 & u1,u2,v1,v2 are_DTr_wrt w,y holds
t1,t2,w1,w2 are_DTr_wrt w,y
let u, u1, u2, v1, v2, t1, t2, w1, w2 be VECTOR of V; :: thesis: ( Gen w,y & u = u1 # t1 & u = u2 # t2 & u = v1 # w1 & u = v2 # w2 & u1,u2,v1,v2 are_DTr_wrt w,y implies t1,t2,w1,w2 are_DTr_wrt w,y )
assume that
A1: Gen w,y and
A2: ( u = u1 # t1 & u = u2 # t2 & u = v1 # w1 & u = v2 # w2 ) and
A3: u1,u2,v1,v2 are_DTr_wrt w,y ; :: thesis: t1,t2,w1,w2 are_DTr_wrt w,y
set p = u1 # u2;
set q = v1 # v2;
set r = t1 # t2;
set s = w1 # w2;
A4: ( u1,u2 // v1,v2 & u1,u2,u1 # u2,v1 # v2 are_Ort_wrt w,y & v1,v2,u1 # u2,v1 # v2 are_Ort_wrt w,y ) by A3, Def3;
A5: ( u2 - u1 = - (t2 - t1) & v2 - v1 = - (w2 - w1) ) by A2, Lm3;

A6: now

assume u1 = u2 ; :: thesis: ( t1,t2 // w1,w2 & t1,t2,t1 # t2,w1 # w2 are_Ort_wrt w,y )
then t1 = t2 by A2, Th9;
hence ( t1,t2 // w1,w2 & t1,t2,t1 # t2,w1 # w2 are_Ort_wrt w,y ) by A1, Lm8, ANALOAF:18; :: thesis: verum

end;

A7: now

assume v1 = v2 ; :: thesis: ( t1,t2 // w1,w2 & w1,w2,t1 # t2,w1 # w2 are_Ort_wrt w,y )
then w1 = w2 by A2, Th9;
hence ( t1,t2 // w1,w2 & w1,w2,t1 # t2,w1 # w2 are_Ort_wrt w,y ) by A1, Lm8, ANALOAF:18; :: thesis: verum

end;

A8: t1,t2 // w1,w2

proof

now

assume ( u1 <> u2 & v1 <> v2 ) ; :: thesis: t1,t2 // w1,w2
then consider a, b being Real such that
A9: ( 0 < a & 0 < b & a * (u2 - u1) = b * (v2 - v1) ) by A4, ANALOAF:def 1;
a * (t2 - t1) = a * (- (- (t2 - t1))) by RLVECT_1:30
.= - (b * (- (w2 - w1))) by A5, A9, RLVECT_1:39
.= b * (- (- (w2 - w1))) by RLVECT_1:39
.= b * (w2 - w1) by RLVECT_1:30 ;
hence t1,t2 // w1,w2 by A9, ANALOAF:def 1; :: thesis: verum

end;

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

end;

( u = (u1 # u2) # (t1 # t2) & u = (v1 # v2) # (w1 # w2) )

proof

thus (u1 # u2) # (t1 # t2) = u # u by A2, Th8
.= u ; :: thesis: u = (v1 # v2) # (w1 # w2)
thus (v1 # v2) # (w1 # w2) = u # u by A2, Th8
.= u ; :: thesis: verum

end;

then A10: (w1 # w2) - (t1 # t2) = - ((v1 # v2) - (u1 # u2)) by Lm3
.= (- 1) * ((v1 # v2) - (u1 # u2)) by RLVECT_1:29 ;
( t2 - t1 = - (u2 - u1) & w2 - w1 = - (v2 - v1) ) by A2, Lm3;
then A11: ( t2 - t1 = (- 1) * (u2 - u1) & w2 - w1 = (- 1) * (v2 - v1) ) by RLVECT_1:29;
( u2 - u1,(v1 # v2) - (u1 # u2) are_Ort_wrt w,y & v2 - v1,(v1 # v2) - (u1 # u2) are_Ort_wrt w,y ) by A4, ANALMETR:def 3;
then ( t2 - t1,(w1 # w2) - (t1 # t2) are_Ort_wrt w,y & w2 - w1,(w1 # w2) - (t1 # t2) are_Ort_wrt w,y ) by A10, A11, ANALMETR:10;
then ( t1,t2,t1 # t2,w1 # w2 are_Ort_wrt w,y & w1,w2,t1 # t2,w1 # w2 are_Ort_wrt w,y ) by ANALMETR:def 3;
hence t1,t2,w1,w2 are_DTr_wrt w,y by A8, Def3; :: thesis: verum