for eps being real number st eps > 0 holds
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
dseq . n > (Sum eseq) - eps

proof

let eps be real number ; :: thesis: ( eps > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
dseq . n > (Sum eseq) - eps )
assume A1: eps > 0 ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
dseq . n > (Sum eseq) - eps
then consider K being Element of NAT such that
A2: (Partial_Sums eseq) . K > (Sum eseq) - (eps / 2) by Th24, Th28, XREAL_1:139;
A3: ((Partial_Sums eseq) . K) - (eps / 2) > ((Sum eseq) - (eps / 2)) - (eps / 2) by A2, XREAL_1:9;
deffunc H₁( Element of NAT ) -> Element of REAL = (Partial_Sums (cseq $1)) . K;
consider dseqK being Real_Sequence such that
A4: for n being Element of NAT holds dseqK . n = H₁(n) from SEQ_1:sch 1();
( dseqK is convergent & lim dseqK = (Partial_Sums eseq) . K ) by A4, Th25;
then consider N being Element of NAT such that
A5: for n being Element of NAT st n >= N holds
dseqK . n > ((Partial_Sums eseq) . K) - (eps / 2) by A1, Th26, XREAL_1:139;
take N1 = N + 1; :: thesis: for n being Element of NAT st n >= N1 holds
dseq . n > (Sum eseq) - eps
let n be Element of NAT ; :: thesis: ( n >= N1 implies dseq . n > (Sum eseq) - eps )
assume A6: n >= N1 ; :: thesis: dseq . n > (Sum eseq) - eps
then ( ( for k being Element of NAT holds (cseq n) . k >= 0 ) & cseq n is summable ) by Th15, Th22;
then Sum (cseq n) >= (Partial_Sums (cseq n)) . K by Th30;
then dseq . n >= (Partial_Sums (cseq n)) . K by A6, Th22;
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

end;

hence ( dseq is convergent & lim dseq = Sum eseq ) by Th27, Th29; :: thesis: verum