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