theorem :: ZMODUL02:30

for V being Z_Module
for L being Linear_Combination of V holds (0. INT.Ring) * L = ZeroLC V by VECTSP_6:30;