let f be Function of [:NAT,NAT:],ExtREAL; 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; ( ( 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
; ( f is P-convergent_to_finite_number & P-lim f = r )
A2:
now 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).| < preconsider N = 1 as
Nat ;
let p be
Real;
( 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
;
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - r).| < ptake N =
N;
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - r).| < plet n,
m be
Nat;
( n >= N & m >= N implies |.((f . (n,m)) - r).| < p )assume
(
n >= N &
m >= N )
;
|.((f . (n,m)) - r).| < p
f . (
n,
m)
= r
by A1;
hence
|.((f . (n,m)) - r).| < p
by A3, XXREAL_3:7, EXTREAL1:16;
verum end;
hence A4:
f is P-convergent_to_finite_number
; P-lim f = r
then
f is P-convergent
;
hence
P-lim f = r
by A2, A4, Def5; verum