for V being RealLinearSpace
for w, y, u, u1, u2, v1, v2, t1, t2, w1, w2 being VECTOR of V st 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