theorem :: COMSEQ_3:47

for seq being Complex_Sequence st seq is convergent holds
for p being Real st 0 < p holds
ex n being Nat st
for m, l being Nat st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p