for V being RealLinearSpace
for u, v being VECTOR of V
for W being Subspace of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v - v1 = u )