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