let R be Ring; :: thesis: for V being RightMod of R
for v being Vector of V holds {v} is Coset of (0). V
let V be RightMod of R; :: 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 Th46;
hence {v} is Coset of (0). V by Def6; :: thesis: verum