theorem LmSumScDM14: :: ZMODLAT3:17

for L being Z_Lattice
for v, u being Vector of (DivisibleMod L)
for l being Linear_Combination of {u} holds SumSc (v,l) = (ScProductDM L) . (v,((l . u) * u))