:: deftheorem defSumScDM defines SumSc ZMODLAT3:def 4 :
for L being Z_Lattice
for l being Linear_Combination of DivisibleMod L
for v being Vector of (DivisibleMod L)
for b₄ being Element of F_Real holds
( b₄ = SumSc (v,l) iff ex F being FinSequence of (DivisibleMod L) st
( F is one-to-one & rng F = Carrier l & b₄ = Sum (ScFS (v,l,F)) ) );