for R being Ring
for V being LeftMod of R holds the carrier of V is Coset of (Omega). V by VECTSP_4:74;