theorem Th87: :: CLVECT_1:87
for V being ComplexLinearSpace
for v being VECTOR of V
for W1, W2 being strict Subspace of V holds
( v + W1 = v + W2 iff W1 = W2 )