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 that
A1: seq = Eseq and
A2: ( seq is nonnegative & seq is summable ) ; :: thesis: Sum seq = SUM Eseq
A3: for n being Element of NAT holds seq . n >= 0 by A2, RINFSUP1:def 3;
Partial_Sums seq is convergent by A2, SERIES_1:def 2;
then A4: Partial_Sums seq is bounded ;
then upper_bound (Partial_Sums seq) = sup (rng (Ser Eseq)) by A1, Th10, Th11;
then upper_bound (Partial_Sums seq) = SUM Eseq by SUPINF_2:def 17;
hence Sum seq = SUM Eseq by A4, A3, RINFSUP1:24, SERIES_1:16; :: thesis: verum