theorem :: GEOMTRAP:45

for V being RealLinearSpace
for u, v, w, y being VECTOR of V
for a, b being Element of (DTrSpace (V,w,y)) st Gen w,y & u = a & v = b holds
u # v = a # b by Def8;