:: deftheorem Def5 defines convergent COMSEQ_2:def 5 :
for s being complex-valued ManySortedSet of NAT holds
( s is convergent iff ex g being Complex st
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - g).| < p );