theorem Th97: :: CLVECT_1:97

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