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