let V be RealLinearSpace; :: thesis: for w, y, u, u9, u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st Gen w,y & 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 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, u9, u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st Gen w,y & 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 are_DTr_wrt w,y holds
t1,t2,w1,w2 are_DTr_wrt w,y
let u, u9, u1, u2, v1, v2, t1, t2, w1, w2 be VECTOR of V; :: thesis: ( Gen w,y & 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 are_DTr_wrt w,y implies t1,t2,w1,w2 are_DTr_wrt w,y )
assume that
A1: ( Gen w,y & u <> u9 ) and
A2: ( u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y ) and
A3: ( u,u9,v1,w1 are_DTr_wrt w,y & u,u9,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
set uu = u1 # u2;
set vv = v1 # v2;
A5: ( u,u9,u1 # u2,t1 # t2 are_DTr_wrt w,y & u,u9,v1 # v2,w1 # w2 are_DTr_wrt w,y ) by A1, A2, A3, Th39;
v1,v2,u1 # u2,v1 # v2 are_Ort_wrt w,y by A4;
then A6: w1,w2,t1 # t2,w1 # w2 are_Ort_wrt w,y by A1, A3, A5, Th40;
u1,u2,u1 # u2,v1 # v2 are_Ort_wrt w,y by A4;
then A7: t1,t2,t1 # t2,w1 # w2 are_Ort_wrt w,y by A1, A2, A5, Th40;
u1,u2 // v1,v2 by A4;
then t1,t2 // w1,w2 by A1, A2, A3, Th37;
hence t1,t2,w1,w2 are_DTr_wrt w,y by A7, A6; :: thesis: verum