for V being RealLinearSpace
for u, w being VECTOR of V ex y being VECTOR of V st u # y = w