for seq being sequence of REAL
for Eseq being sequence of ExtREAL st seq = Eseq & seq is nonnegative & seq is summable holds
Sum seq = SUM Eseq