theorem :: ZMODUL01:13

for V being Z_Module
for a being Element of INT.Ring holds a * (Sum (<*> the carrier of V)) = 0. V by Lm1, Th1;