theorem :: ZMODUL02:20

for V being Z_Module
for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V by VECTSP_6:16;