for L being Z_Lattice
for l being Linear_Combination of DivisibleMod L
for v being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)