let s be Real_Sequence; :: thesis: ( s is summable iff for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r )
thus ( s is summable implies for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r ) :: thesis: ( ( for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r ) implies s is summable )

proof

assume s is summable ; :: thesis: for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r
then Partial_Sums s is convergent by Def2;
hence for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r by SEQ_4:58; :: thesis: verum

end;

assume for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r ; :: thesis: s is summable
then Partial_Sums s is convergent by SEQ_4:58;
hence s is summable by Def2; :: thesis: verum