for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V holds
( u + v in v + W iff u in W )