:: deftheorem Def5 defines Sum MEASURE9:def 5 :
for e being FinSequence of ExtREAL *
for b₂ being FinSequence of ExtREAL holds
( b₂ = Sum e iff ( len b₂ = len e & ( for k being Nat st k in dom b₂ holds
b₂ . k = Sum (e . k) ) ) );