:: deftheorem Def6 defines Sum CONVEX4:def 6 :
for V being non empty right_complementable Abelian add-associative right_zeroed CLSStruct
for L being C_Linear_Combination of V
for b₃ being Element of V holds
( b₃ = Sum L iff ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & b₃ = Sum (L (#) F) ) );