theorem LmSumSc14: :: ZMODLAT3:8

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