:: deftheorem defines Cauchy CLVECT_3:def 9 :
for Cseq being Complex_Sequence holds
( Cseq is Cauchy iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
|.((Cseq . n) - (Cseq . m)).| < r );