theorem :: ZMODUL01:61

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