for V being ComplexLinearSpace
for u being VECTOR of V
for W being Subspace of V
for B, C being Coset of W st u in B & u in C holds
B = C