let seq be Complex_Sequence; :: thesis: ( seq is summable iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p )
A1: ( seq is summable implies for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p ) by Th46;

now

assume for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p ; :: thesis: seq is summable
then Partial_Sums seq is convergent by Th46;
hence seq is summable by Def10; :: thesis: verum

end;

hence ( seq is summable iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p ) by A1; :: thesis: verum