for f being nonnegative FinSequence of ExtREAL
for s being ExtREAL_sequence st ( for n being object st n in dom f holds
f . n = s . n ) & ( for n being Element of NAT st not n in dom f holds
s . n = 0 ) holds
( Sum f = Sum s & Sum f = SUM s )