theorem Th75: :: CLVECT_1:75

for V being ComplexLinearSpace
for u, v1, v2 being VECTOR of V
for W being Subspace of V st u in v1 + W & u in v2 + W holds
v1 + W = v2 + W