for L being Z_Lattice
for v being Vector of (DivisibleMod L)
for l1, l2 being Linear_Combination of DivisibleMod L holds SumSc (v,(l1 + l2)) = (SumSc (v,l1)) + (SumSc (v,l2))