let seq be ExtREAL_sequence; :: thesis: ( seq is nonnegative implies ( seq is summable & SUM seq = Sum seq ) )
assume seq is nonnegative ; :: thesis: ( seq is summable & SUM seq = Sum seq )
then A1: Partial_Sums seq is non-decreasing by MESFUNC9:16;
then Partial_Sums seq is convergent by RINFSUP2:37;
hence seq is summable ; :: thesis: SUM seq = Sum seq
lim (Partial_Sums seq) = sup (Partial_Sums seq) by A1, RINFSUP2:37;
hence Sum seq = SUM seq by Th1; :: thesis: verum