let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: for a being Real st ( for n, m being Nat holds Rseq . (n,m) = a ) holds
( Rseq is P-convergent & P-lim Rseq = a )
let a be Real; :: thesis: ( ( for n, m being Nat holds Rseq . (n,m) = a ) implies ( Rseq is P-convergent & P-lim Rseq = a ) )
assume a1: for n, m being Nat holds Rseq . (n,m) = a ; :: thesis: ( Rseq is P-convergent & P-lim Rseq = a )

a3: now :: thesis: 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)) - a).| < e

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - a).| < e )
assume a2: 0 < e ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - a).| < e

a4: now :: thesis: for n, m being Nat st n >= 0 & m >= 0 holds
|.((Rseq . (n,m)) - a).| < e

let n, m be Nat; :: thesis: ( n >= 0 & m >= 0 implies |.((Rseq . (n,m)) - a).| < e )
assume ( n >= 0 & m >= 0 ) ; :: thesis: |.((Rseq . (n,m)) - a).| < e
Rseq . (n,m) = a by a1;
hence |.((Rseq . (n,m)) - a).| < e by a2, COMPLEX1:44; :: thesis: verum

end;

reconsider N = 0 as Nat ;
take N = N; :: thesis: for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - a).| < e
thus for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - a).| < e by a4; :: thesis: verum

end;

hence Rseq is P-convergent ; :: thesis: P-lim Rseq = a
hence P-lim Rseq = a by a3, def6; :: thesis: verum