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