theorem :: ZMODUL02:12

for V being Z_Module
for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V by VECTSP_6:6;