:: deftheorem def6 defines P-lim DBLSEQ_1:def 2 :
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is P-convergent holds
for b₂ being Real holds
( b₂ = P-lim Rseq iff 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)) - b₂).| < e );