for eps being Real st eps > 0 holds

ex N being Nat st

for n being Nat st n >= N holds

dseq . n > (Sum eseq) - eps

ex N being Nat st

for n being Nat st n >= N holds

dseq . n > (Sum eseq) - eps

proof

hence
( dseq is convergent & lim dseq = Sum eseq )
by Th26, Th28; :: thesis: verum
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_{1}( Nat) -> set = (Partial_Sums (cseq $1)) . K;

consider dseqK being Real_Sequence such that

A4: for n being Nat holds dseqK . n = H_{1}(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

end;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

consider dseqK being Real_Sequence such that

A4: for n being Nat holds dseqK . n = H

( 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