theorem LmSumScDM11: :: ZMODLAT3:14

for L being Z_Lattice
for v being Vector of (DivisibleMod L) holds SumSc (v,(ZeroLC (DivisibleMod L))) = 0. F_Real