theorem LmSumSc13: :: ZMODLAT3:7

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