let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: for r being Real st ( for n, m being Nat holds f . (n,m) = r ) holds
( f is P-convergent_to_finite_number & P-lim f = r )
let r be Real; :: thesis: ( ( for n, m being Nat holds f . (n,m) = r ) implies ( f is P-convergent_to_finite_number & P-lim f = r ) )
assume A1: for n, m being Nat holds f . (n,m) = r ; :: thesis: ( f is P-convergent_to_finite_number & P-lim f = r )

A2: now :: thesis: for p being Real st 0 < p holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - r).| < p

reconsider N = 1 as Nat ;
let p be Real; :: thesis: ( 0 < p implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - r).| < p )
assume A3: 0 < p ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - r).| < p
take N = N; :: thesis: for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - r).| < p
let n, m be Nat; :: thesis: ( n >= N & m >= N implies |.((f . (n,m)) - r).| < p )
assume ( n >= N & m >= N ) ; :: thesis: |.((f . (n,m)) - r).| < p
f . (n,m) = r by A1;
hence |.((f . (n,m)) - r).| < p by A3, XXREAL_3:7, EXTREAL1:16; :: thesis: verum

end;

hence A4: f is P-convergent_to_finite_number ; :: thesis: P-lim f = r
then f is P-convergent ;
hence P-lim f = r by A2, A4, Def5; :: thesis: verum