theorem :: ZMODUL01:61

for R being Ring
for V being LeftMod of R
for v being Vector of V holds v + ((Omega). V) = the carrier of V by VECTSP_4:47;