for seq being ExtREAL_sequence st seq is nonnegative holds
( seq is summable & SUM seq = Sum seq )