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

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