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