let V be RealUnitarySpace; :: 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 Th39;
hence {v} is Coset of (0). V by Def5; :: thesis: verum