theorem LmSumSc11: :: ZMODLAT3:5

for L being Z_Lattice
for v being Vector of L holds SumSc (v,(ZeroLC L)) = 0. F_Real