theorem Th71: :: CLVECT_1:71

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