theorem Th46: :: COMSEQ_3:46

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