let seq be Function of NAT ,REAL ; :: thesis: for Eseq being Function of NAT ,ExtREAL st seq = Eseq & seq is nonnegative & seq is summable holds
Sum seq = SUM Eseq
let Eseq be Function of NAT ,ExtREAL ; :: thesis: ( seq = Eseq & seq is nonnegative & seq is summable implies Sum seq = SUM Eseq )
assume A1: ( seq = Eseq & seq is nonnegative & seq is summable ) ; :: thesis: Sum seq = SUM Eseq
Partial_Sums seq is convergent by A1, SERIES_1:def 2;
then Partial_Sums seq is bounded by SEQ_2:27;
then A2: Partial_Sums seq is bounded_above ;
then sup (Partial_Sums seq) = sup (rng (Ser Eseq)) by A1, Th10, Th11;
then A3: sup (Partial_Sums seq) = SUM Eseq by SUPINF_2:def 23;
for n being Element of NAT holds seq . n >= 0 by A1, RINFSUP1:def 3;
then Partial_Sums seq is non-decreasing by SERIES_1:19;
hence Sum seq = SUM Eseq by A2, A3, RINFSUP1:24; :: thesis: verum