let seq be Real_Sequence; :: thesis: ( seq is summable implies for eps being Real st eps > 0 holds

ex K being Nat st (Partial_Sums seq) . K > (Sum seq) - eps )

assume seq is summable ; :: thesis: for eps being Real st eps > 0 holds

ex K being Nat st (Partial_Sums seq) . K > (Sum seq) - eps

then A1: Partial_Sums seq is convergent by SERIES_1:def 2;

let eps be Real; :: thesis: ( eps > 0 implies ex K being Nat st (Partial_Sums seq) . K > (Sum seq) - eps )

assume eps > 0 ; :: thesis: ex K being Nat st (Partial_Sums seq) . K > (Sum seq) - eps

then consider K being Nat such that

A2: for k being Nat st k >= K holds

(Partial_Sums seq) . k > (lim (Partial_Sums seq)) - eps by A1, Th25;

take K ; :: thesis: (Partial_Sums seq) . K > (Sum seq) - eps

Sum seq = lim (Partial_Sums seq) by SERIES_1:def 3;

hence (Partial_Sums seq) . K > (Sum seq) - eps by A2; :: thesis: verum

ex K being Nat st (Partial_Sums seq) . K > (Sum seq) - eps )

assume seq is summable ; :: thesis: for eps being Real st eps > 0 holds

ex K being Nat st (Partial_Sums seq) . K > (Sum seq) - eps

then A1: Partial_Sums seq is convergent by SERIES_1:def 2;

let eps be Real; :: thesis: ( eps > 0 implies ex K being Nat st (Partial_Sums seq) . K > (Sum seq) - eps )

assume eps > 0 ; :: thesis: ex K being Nat st (Partial_Sums seq) . K > (Sum seq) - eps

then consider K being Nat such that

A2: for k being Nat st k >= K holds

(Partial_Sums seq) . k > (lim (Partial_Sums seq)) - eps by A1, Th25;

take K ; :: thesis: (Partial_Sums seq) . K > (Sum seq) - eps

Sum seq = lim (Partial_Sums seq) by SERIES_1:def 3;

hence (Partial_Sums seq) . K > (Sum seq) - eps by A2; :: thesis: verum