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 st u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y holds
u,u9,u1 # u2,t1 # t2 are_DTr_wrt w,y
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, u9, u1, u2, t1, t2 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 holds
u,u9,u1 # u2,t1 # t2 are_DTr_wrt w,y )
assume A1: Gen w,y ; :: thesis: for u, u9, u1, u2, t1, t2 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 holds
u,u9,u1 # u2,t1 # t2 are_DTr_wrt w,y
let u, u9, u1, u2, t1, t2 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 implies u,u9,u1 # u2,t1 # t2 are_DTr_wrt w,y )
assume that
A2: u <> u9 and
A3: u,u9,u1,t1 are_DTr_wrt w,y and
A4: u,u9,u2,t2 are_DTr_wrt w,y ; :: thesis: u,u9,u1 # u2,t1 # t2 are_DTr_wrt w,y
u1,t1,u2,t2 are_DTr_wrt w,y by A1, A2, A3, A4, Th19;
then A5: u1,t1,u1 # u2,t1 # t2 are_DTr_wrt w,y by A1, Th26;
u2,t2,u1,t1 are_DTr_wrt w,y by A1, A2, A3, A4, Th19;
then A6: u2,t2,u2 # u1,t2 # t1 are_DTr_wrt w,y by A1, Th26;

per cases ( u1 <> t1 or u2 <> t2 or ( u1 = t1 & u2 = t2 ) ) ;

suppose A7: u1 <> t1 ; :: thesis: u,u9,u1 # u2,t1 # t2 are_DTr_wrt w,y

u1,t1,u,u9 are_DTr_wrt w,y by A3, Th21;
hence u,u9,u1 # u2,t1 # t2 are_DTr_wrt w,y by A1, A5, A7, Th19; :: thesis: verum

end;

suppose A8: u2 <> t2 ; :: thesis: u,u9,u1 # u2,t1 # t2 are_DTr_wrt w,y

u2,t2,u,u9 are_DTr_wrt w,y by A4, Th21;
hence u,u9,u1 # u2,t1 # t2 are_DTr_wrt w,y by A1, A6, A8, Th19; :: thesis: verum

end;

suppose that A9: u1 = t1 and
A10: u2 = t2 ; :: thesis: u,u9,u1 # u2,t1 # t2 are_DTr_wrt w,y

u # u9,(u1 # u2) # (t1 # t2),u1 # u2,t1 # t2 are_Ort_wrt w,y by A1, A9, A10, Lm6;
then A11: u1 # u2,t1 # t2,u # u9,(u1 # u2) # (t1 # t2) are_Ort_wrt w,y by Lm5;
A12: u,u9,u # u9,u1 # u2 are_Ort_wrt w,y

proof

set uu9 = u # u9;
A13: 2 * (u1 # u2) = (1 + 1) * (u1 # u2)
.= (1 * (u1 # u2)) + (1 * (u1 # u2)) by RLVECT_1:def 6
.= (u1 # u2) + (1 * (u1 # u2)) by RLVECT_1:def 8
.= (u1 # u2) + (u1 # u2) by RLVECT_1:def 8
.= u1 + u2 by Def2 ;
A14: - (2 * (u # u9)) = - ((1 + 1) * (u # u9))
.= - ((1 * (u # u9)) + (1 * (u # u9))) by RLVECT_1:def 6
.= - ((u # u9) + (1 * (u # u9))) by RLVECT_1:def 8
.= - ((u # u9) + (u # u9)) by RLVECT_1:def 8
.= (- (u # u9)) + (- (u # u9)) by Lm19 ;
u,u9,u # u9,u2 # t2 are_Ort_wrt w,y by A4;
then u9 - u,u2 - (u # u9) are_Ort_wrt w,y by A10, ANALMETR:def 3;
then A15: u9 - u,(2 ") * (u2 - (u # u9)) are_Ort_wrt w,y by ANALMETR:7;
u,u9,u # u9,u1 # t1 are_Ort_wrt w,y by A3;
then u9 - u,u1 - (u # u9) are_Ort_wrt w,y by A9, ANALMETR:def 3;
then A16: u9 - u,(2 ") * (u1 - (u # u9)) are_Ort_wrt w,y by ANALMETR:7;
(u1 # u2) - (u # u9) = ((2 ") * 2) * ((u1 # u2) - (u # u9)) by RLVECT_1:def 8
.= (2 ") * (2 * ((u1 # u2) - (u # u9))) by RLVECT_1:def 7
.= (2 ") * ((u1 + u2) - (2 * (u # u9))) by A13, RLVECT_1:34
.= (2 ") * (((u1 + u2) + (- (u # u9))) + (- (u # u9))) by A14, RLVECT_1:def 3
.= (2 ") * (((u1 - (u # u9)) + u2) + (- (u # u9))) by RLVECT_1:def 3
.= (2 ") * ((u1 - (u # u9)) + (u2 - (u # u9))) by RLVECT_1:def 3
.= ((2 ") * (u1 - (u # u9))) + ((2 ") * (u2 - (u # u9))) by RLVECT_1:def 5 ;
then u9 - u,(u1 # u2) - (u # u9) are_Ort_wrt w,y by A1, A16, A15, ANALMETR:10;
hence u,u9,u # u9,u1 # u2 are_Ort_wrt w,y by ANALMETR:def 3; :: thesis: verum

end;

u,u9 // u1 # u2,t1 # t2 by A9, A10, ANALOAF:9;
hence u,u9,u1 # u2,t1 # t2 are_DTr_wrt w,y by A9, A10, A11, A12; :: thesis: verum

end;

end;