:: deftheorem Def2 defines Sum EXTREAL1:def 2 :
for F being FinSequence of ExtREAL
for b₂ being R_eal holds
( b₂ = Sum F iff ex f being sequence of ExtREAL st
( b₂ = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) );