for V being RealLinearSpace
for w, y being VECTOR of V
for x being set holds
( x is Element of the carrier of (DTrSpace (V,w,y)) iff x is VECTOR of V ) ;