:: deftheorem defines P-convergent_to_finite_number DBLSEQ_3:def 1 :
for Eseq being Function of [:NAT,NAT:],ExtREAL holds
( Eseq is P-convergent_to_finite_number iff ex p being Real st
for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Eseq . (n,m)) - p).| < e );