let V be RealLinearSpace; :: thesis: for w, y, u, u', u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st Gen w,y & 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 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, u', u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st Gen w,y & 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 are_DTr_wrt w,y holds
t1,t2,w1,w2 are_DTr_wrt w,y
let u, u', u1, u2, v1, v2, t1, t2, w1, w2 be VECTOR of V; :: thesis: ( Gen w,y & 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 are_DTr_wrt w,y implies t1,t2,w1,w2 are_DTr_wrt w,y )
assume that
A1: Gen w,y and
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 are_DTr_wrt w,y ; :: thesis: t1,t2,w1,w2 are_DTr_wrt w,y
A5: t1,t2 // w1,w2

proof

u1,u2 // v1,v2 by A4, Def3;
hence t1,t2 // w1,w2 by A1, A2, A3, Th39; :: thesis: verum

end;

set uu = u1 # u2;
set vv = v1 # v2;
A6: ( u,u',u1 # u2,t1 # t2 are_DTr_wrt w,y & u,u',v1 # v2,w1 # w2 are_DTr_wrt w,y ) by A1, A2, A3, Th41;
u1,u2,u1 # u2,v1 # v2 are_Ort_wrt w,y by A4, Def3;
then A7: t1,t2,t1 # t2,w1 # w2 are_Ort_wrt w,y by A1, A2, A3, A6, Th42;
v1,v2,u1 # u2,v1 # v2 are_Ort_wrt w,y by A4, Def3;
then w1,w2,t1 # t2,w1 # w2 are_Ort_wrt w,y by A1, A2, A3, A6, Th42;
hence t1,t2,w1,w2 are_DTr_wrt w,y by A5, A7, Def3; :: thesis: verum