for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V
for C being Coset of W st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u + v1 = v )