let seq be sequence of REAL; :: thesis: for Eseq being sequence of ExtREAL st seq = Eseq & seq is nonnegative & seq is summable holds
Sum seq = SUM Eseq
let Eseq be sequence of ExtREAL; :: thesis: ( seq = Eseq & seq is nonnegative & seq is summable implies Sum seq = SUM Eseq )
assume that
A1: seq = Eseq and
A2: ( seq is nonnegative & seq is summable ) ; :: thesis: Sum seq = SUM Eseq
A3: for n being Nat holds seq . n >= 0 by A2, RINFSUP1:def 3;
Partial_Sums seq is convergent by A2;
then A4: Partial_Sums seq is bounded ;
then upper_bound (Partial_Sums seq) = sup (rng (Ser Eseq)) by A1, Th9, Th10;
then upper_bound (Partial_Sums seq) = SUM Eseq ;
hence Sum seq = SUM Eseq by A4, A3, RINFSUP1:24, SERIES_1:16; :: thesis: verum