theorem LmSumScDM13: :: ZMODLAT3:16

for L being Z_Lattice
for v being Vector of (DivisibleMod L)
for l being Linear_Combination of DivisibleMod L st Carrier l = {} holds
SumSc (v,l) = 0. F_Real