theorem :: CLVECT_1:96

for V being ComplexLinearSpace
for W being Subspace of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )