let eps be Real; :: thesis: ( eps > 0 implies ex N being Nat st
for n being Nat st n >= N holds
dseq . n > (Sum eseq) - eps )
assume A1: eps > 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
dseq . n > (Sum eseq) - eps
then consider K being Nat such that
A2: (Partial_Sums eseq) . K > (Sum eseq) - (eps / 2) by Th23, Th27, XREAL_1:139;
A3: ((Partial_Sums eseq) . K) - (eps / 2) > ((Sum eseq) - (eps / 2)) - (eps / 2) by A2, XREAL_1:9;
deffunc H₁( Nat) -> set = (Partial_Sums (cseq $1)) . K;
consider dseqK being Real_Sequence such that
A4: for n being Nat holds dseqK . n = H₁(n) from SEQ_1:sch 1();
( dseqK is convergent & lim dseqK = (Partial_Sums eseq) . K ) by A4, Th24;
then consider N being Nat such that
A5: for n being Nat st n >= N holds
dseqK . n > ((Partial_Sums eseq) . K) - (eps / 2) by A1, Th25, XREAL_1:139;
take N1 = N + 1; :: thesis: for n being Nat st n >= N1 holds
dseq . n > (Sum eseq) - eps
let n be Nat; :: thesis: ( n >= N1 implies dseq . n > (Sum eseq) - eps )
assume A6: n >= N1 ; :: thesis: dseq . n > (Sum eseq) - eps
then ( ( for k being Nat holds (cseq n) . k >= 0 ) & cseq n is summable ) by Th14, Th21;
then Sum (cseq n) >= (Partial_Sums (cseq n)) . K by Th29;
then dseq . n >= (Partial_Sums (cseq n)) . K by A6, Th21;
then A7: dseq . n >= dseqK . n by A4;
N + 1 >= N + 0 by XREAL_1:6;
then n >= N by A6, XXREAL_0:2;
then dseqK . n > ((Partial_Sums eseq) . K) - (eps / 2) by A5;
then dseq . n > ((Partial_Sums eseq) . K) - (eps / 2) by A7, XXREAL_0:2;
hence dseq . n > (Sum eseq) - eps by A3, XXREAL_0:2; :: thesis: verum