for V being RealLinearSpace
for u, u1, v, v1, w, y being VECTOR of V
for a, b, a1, b1 being Element of (DTrSpace (V,w,y)) st u = a & v = b & u1 = a1 & v1 = b1 holds
( a,b // a1,b1 iff u,v,u1,v1 are_DTr_wrt w,y )