let R be Ring; :: thesis: for V being RightMod of R
for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V
let V be RightMod of R; :: thesis: for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V
let l be Linear_Combination of {} the carrier of V; :: thesis: Sum l = 0. V
l = ZeroLC V by Th21;
hence Sum l = 0. V by Lm3; :: thesis: verum