:: deftheorem Def3 defines sum RLAFFIN1:def 3 :
for S being non empty addLoopStr
for LS being Linear_Combination of S
for b₃ being Real holds
( b₃ = sum LS iff ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & b₃ = Sum (LS * F) ) );