theorem LmSumSc1X: :: ZMODLAT3:9

for L being Z_Lattice
for v being Vector of L
for l1, l2 being Linear_Combination of L holds SumSc (v,(l1 + l2)) = (SumSc (v,l1)) + (SumSc (v,l2))