let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: for c being ExtReal st ( for n, m being Nat holds f . (n,m) = c ) holds
( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) )
let c be ExtReal; :: thesis: ( ( for n, m being Nat holds f . (n,m) = c ) implies ( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) ) )
reconsider cc = c as R_eal by XXREAL_0:def 1;
A1: dom f = [:NAT,NAT:] by FUNCT_2:def 1;
c in ExtREAL by XXREAL_0:def 1;
then A2: ( c in REAL or c in {-infty,+infty} ) by XBOOLE_0:def 3, XXREAL_0:def 4;
assume A3: for n, m being Nat holds f . (n,m) = c ; :: thesis: ( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) )
then A4: f . (1,1) = c ;

now :: thesis: for v being ExtReal st v in rng f holds
v <= c

let v be ExtReal; :: thesis: ( v in rng f implies v <= c )
assume v in rng f ; :: thesis: v <= c
then consider z being object such that
A7: ( z in dom f & v = f . z ) by FUNCT_1:def 3;
consider n, m being object such that
A8: ( n in NAT & m in NAT & z = [n,m] ) by A7, ZFMISC_1:def 2;
reconsider n = n, m = m as Element of NAT by A8;
v = f . (n,m) by A7, A8;
hence v <= c by A3; :: thesis: verum

end;

then A5: c is UpperBound of rng f by XXREAL_2:def 1;

per cases ( c in REAL or c = -infty or c = +infty ) by A2, TARSKI:def 2;

suppose c in REAL ; :: thesis: ( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) )

then reconsider rc = c as Real ;

A6: now :: thesis: for p being Real st 0 < p holds
ex N being Nat st
for n1, m1 being Nat st N <= n1 & N <= m1 holds
|.((f . (n1,m1)) - rc).| < p

reconsider N = 0 as Nat ;
let p be Real; :: thesis: ( 0 < p implies ex N being Nat st
for n1, m1 being Nat st N <= n1 & N <= m1 holds
|.((f . (n1,m1)) - rc).| < p )
assume A7: 0 < p ; :: thesis: ex N being Nat st
for n1, m1 being Nat st N <= n1 & N <= m1 holds
|.((f . (n1,m1)) - rc).| < p
take N = N; :: thesis: for n1, m1 being Nat st N <= n1 & N <= m1 holds
|.((f . (n1,m1)) - rc).| < p
let n1, m1 be Nat; :: thesis: ( N <= n1 & N <= m1 implies |.((f . (n1,m1)) - rc).| < p )
assume ( N <= n1 & N <= m1 ) ; :: thesis: |.((f . (n1,m1)) - rc).| < p
(f . (n1,m1)) - rc = (f . (n1,m1)) - (f . (n1,m1)) by A3;
hence |.((f . (n1,m1)) - rc).| < p by A7, EXTREAL1:16, XXREAL_3:7; :: thesis: verum

end;

then A8: f is P-convergent_to_finite_number ;
hence f is P-convergent ; :: thesis: ( P-lim f = c & P-lim f = sup (rng f) )
hence A9: P-lim f = c by A6, A8, Def5; :: thesis: P-lim f = sup (rng f)
[1,1] in dom f by A1, ZFMISC_1:87;
hence P-lim f = sup (rng f) by A9, A5, A4, FUNCT_1:3, XXREAL_2:55; :: thesis: verum

end;

suppose A10: c = -infty ; :: thesis: ( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) )

for p being Real st p < 0 holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
f . (n,m) <= p

proof

let p be Real; :: thesis: ( p < 0 implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
f . (n,m) <= p )
assume p < 0 ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
f . (n,m) <= p
take 0 ; :: thesis: for n, m being Nat st n >= 0 & m >= 0 holds
f . (n,m) <= p

now :: thesis: for n, m being Nat st 0 <= n & 0 <= m holds
f . (n,m) <= p

let n, m be Nat; :: thesis: ( 0 <= n & 0 <= m implies f . (n,m) <= p )
assume ( 0 <= n & 0 <= m ) ; :: thesis: f . (n,m) <= p
f . (n,m) = -infty by A3, A10;
hence f . (n,m) <= p by XREAL_0:def 1, XXREAL_0:12; :: thesis: verum

end;

hence for n, m being Nat st n >= 0 & m >= 0 holds
f . (n,m) <= p ; :: thesis: verum

end;

then A12: f is P-convergent_to_-infty ;
hence f is P-convergent ; :: thesis: ( P-lim f = c & P-lim f = sup (rng f) )
hence A13: P-lim f = c by A10, A12, Def5; :: thesis: P-lim f = sup (rng f)
[1,1] in dom f by A1, ZFMISC_1:87;
hence P-lim f = sup (rng f) by A5, A4, A13, FUNCT_1:3, XXREAL_2:55; :: thesis: verum

end;

suppose A14: c = +infty ; :: thesis: ( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) )

for p being Real st 0 < p holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
p <= f . (n,m)

proof

let p be Real; :: thesis: ( 0 < p implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
p <= f . (n,m) )
assume 0 < p ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
p <= f . (n,m)
take 0 ; :: thesis: for n, m being Nat st n >= 0 & m >= 0 holds
p <= f . (n,m)

now :: thesis: for n, m being Nat st n >= 0 & m >= 0 holds
p <= f . (n,m)

let n, m be Nat; :: thesis: ( n >= 0 & m >= 0 implies p <= f . (n,m) )
assume ( n >= 0 & m >= 0 ) ; :: thesis: p <= f . (n,m)
f . (n,m) = +infty by A3, A14;
hence p <= f . (n,m) by XREAL_0:def 1, XXREAL_0:9; :: thesis: verum

end;

hence for n, m being Nat st n >= 0 & m >= 0 holds
p <= f . (n,m) ; :: thesis: verum

end;

then A16: f is P-convergent_to_+infty ;
hence f is P-convergent ; :: thesis: ( P-lim f = c & P-lim f = sup (rng f) )
hence A17: P-lim f = c by A14, A16, Def5; :: thesis: P-lim f = sup (rng f)
[1,1] in dom f by A1, ZFMISC_1:87;
hence P-lim f = sup (rng f) by A5, A4, A17, FUNCT_1:3, XXREAL_2:55; :: thesis: verum

end;

end;