for V being RealLinearSpace
for u, u1, v, v1 being VECTOR of V st u,v // u1,v1 holds
u,v // u # u1,v # v1