theorem :: ZMODUL01:60

for V being Z_Module
for v being Vector of V holds v + ((0). V) = {v} by VECTSP_4:46;