for V being RealLinearSpace
for u, v being VECTOR of V
for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds
W1 = W2