for L being Z_Lattice
for l being Linear_Combination of L
for v being Vector of L holds <;v,(Sum l);> = SumSc (v,l)