theorem :: ZMODLAT3:6

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