let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V holds {v} is Coset of (0). V
let v be VECTOR of V; :: thesis: {v} is Coset of (0). V
v + ((0). V) = {v} by Th64;
hence {v} is Coset of (0). V by Def12; :: thesis: verum