per cases ( f is P-convergent_to_finite_number or f is P-convergent_to_+infty or f is P-convergent_to_-infty ) by A1;

suppose A2: f is P-convergent_to_finite_number ; :: thesis: ex b₁ being ExtReal st
( ex p being Real st
( b₁ = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - b₁).| < e ) & f is P-convergent_to_finite_number ) or ( b₁ = +infty & f is P-convergent_to_+infty ) or ( b₁ = -infty & f is P-convergent_to_-infty ) )

then consider p being Real such that
A3: for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - p).| < e ;
reconsider p = p as R_eal by XXREAL_0:def 1;
take p ; :: thesis: ( ex p being Real st
( p = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - p).| < e ) & f is P-convergent_to_finite_number ) or ( p = +infty & f is P-convergent_to_+infty ) or ( p = -infty & f is P-convergent_to_-infty ) )
thus ( ex p being Real st
( p = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - p).| < e ) & f is P-convergent_to_finite_number ) or ( p = +infty & f is P-convergent_to_+infty ) or ( p = -infty & f is P-convergent_to_-infty ) ) by A2, A3; :: thesis: verum

end;

suppose ( f is P-convergent_to_+infty or f is P-convergent_to_-infty ) ; :: thesis: ex b₁ being ExtReal st
( ex p being Real st
( b₁ = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - b₁).| < e ) & f is P-convergent_to_finite_number ) or ( b₁ = +infty & f is P-convergent_to_+infty ) or ( b₁ = -infty & f is P-convergent_to_-infty ) )

hence ex b₁ being ExtReal st
( ex p being Real st
( b₁ = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - b₁).| < e ) & f is P-convergent_to_finite_number ) or ( b₁ = +infty & f is P-convergent_to_+infty ) or ( b₁ = -infty & f is P-convergent_to_-infty ) ) ; :: thesis: verum

end;

end;