:: deftheorem defines Cauchy DBLSEQ_1:def 13 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is Cauchy iff for e being Real st e > 0 holds
ex N being Nat st
for n1, n2, m1, m2 being Nat st N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 holds
|.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e );