let seq be Real_Sequence; :: thesis: ( seq is summable implies for eps being real number st eps > 0 holds
ex K being Element of NAT st (Partial_Sums seq) . K > (Sum seq) - eps )
assume seq is summable ; :: thesis: for eps being real number st eps > 0 holds
ex K being Element of 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 number ; :: thesis: ( eps > 0 implies ex K being Element of NAT st (Partial_Sums seq) . K > (Sum seq) - eps )
assume eps > 0 ; :: thesis: ex K being Element of NAT st (Partial_Sums seq) . K > (Sum seq) - eps
then consider K being Element of NAT such that
A2: for k being Element of NAT st k >= K holds
(Partial_Sums seq) . k > (lim (Partial_Sums seq)) - eps by A1, Th26;
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