let V be Z_Module; :: thesis: for l being Z_Linear_Combination of {} the carrier of V holds Sum l = 0. V
let l be Z_Linear_Combination of {} the carrier of V; :: thesis: Sum l = 0. V
l = Z_ZeroLC V by Th12;
hence Sum l = 0. V by Lm1; :: thesis: verum