theorem :: ZMODUL01:82

for R being Ring
for V being LeftMod of R
for V1 being Subset of V st V1 is Coset of (0). V holds
ex v being Vector of V st V1 = {v} by VECTSP_4:72;