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