:: deftheorem defines P-convergent DBLSEQ_1:def 1 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is P-convergent 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
|.((Rseq . (n,m)) - p).| < e );