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 by SEQ_2:27;
then sup (Partial_Sums seq) = sup (rng (Ser Eseq)) by A1, Th10, Th11;
then sup (Partial_Sums seq) = SUM Eseq by SUPINF_2:def 23;
hence Sum seq = SUM Eseq by A4, A3, RINFSUP1:24, SERIES_1:19; :: thesis: verum