for R being Ring
for V being LeftMod of R
for v being Vector of V holds {v} is Coset of (0). V by VECTSP_4:71;