:: deftheorem Def8 defines Sum RLVECT_2:def 8 :
for V being RealLinearSpace
for L being Linear_Combination of V
for b₃ being Element of V holds
( b₃ = Sum L iff ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & b₃ = Sum (L (#) F) ) );