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