:: deftheorem Def6 defines Sum VECTSP_6:def 6 :
for GF being non empty addLoopStr
for V being non empty ModuleStr over GF
for L being Linear_Combination of V st V is Abelian & V is add-associative & V is right_zeroed & V is right_complementable holds
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) ) );