:: deftheorem Def12 defines Coset CLVECT_1:def 12 :
for V being ComplexLinearSpace
for W being Subspace of V
for b₃ being Subset of V holds
( b₃ is Coset of W iff ex v being VECTOR of V st b₃ = v + W );