defpred S1[ ExtReal] means ( ex g being Real st
( $1 = g & ( 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)) - $1).| < p ) & f is P-convergent_to_finite_number ) or ( $1 = +infty & f is P-convergent_to_+infty ) or ( $1 = -infty & f is P-convergent_to_-infty ) );
given g1, g2 being ExtReal such that A4:
S1[g1]
and
A5:
S1[g2]
and
A6:
g1 <> g2
; contradiction
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 A7:
f is
P-convergent_to_finite_number
;
contradictionthen consider g being
Real such that A8:
g1 = g
and A9:
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)) - g1).| < p
and
f is
P-convergent_to_finite_number
by A4, Th93, Th94;
consider h being
Real such that A10:
g2 = h
and A11:
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)) - g2).| < p
and
f is
P-convergent_to_finite_number
by A5, A7, Th93, Th94;
reconsider g =
g,
h =
h as
Complex ;
A12:
g - h <> 0
by A6, A8, A10;
then consider N1 being
Nat such that A13:
for
n,
m being
Nat st
n >= N1 &
m >= N1 holds
|.((f . (n,m)) - g1).| < |.(g - h).| / 2
by A9;
consider N2 being
Nat such that A14:
for
n,
m being
Nat st
n >= N2 &
m >= N2 holds
|.((f . (n,m)) - g2).| < |.(g - h).| / 2
by A11, A12;
reconsider N1 =
N1,
N2 =
N2 as
Element of
NAT by ORDINAL1:def 12;
set N =
max (
N1,
N2);
B1:
(
max (
N1,
N2)
>= N1 &
max (
N1,
N2)
>= N2 )
by XXREAL_0:25;
then A15:
|.((f . ((max (N1,N2)),(max (N1,N2)))) - g1).| < |.(g - h).| / 2
by A13;
A16:
|.((f . ((max (N1,N2)),(max (N1,N2)))) - g2).| < |.(g - h).| / 2
by A14, B1;
reconsider g =
g,
h =
h as
Complex ;
A17:
(f . ((max (N1,N2)),(max (N1,N2)))) - g2 < |.(g - h).| / 2
by A16, EXTREAL1:21;
A18:
- (|.(g - h).| / 2) < (f . ((max (N1,N2)),(max (N1,N2)))) - g2
by A16, EXTREAL1:21;
then reconsider w =
(f . ((max (N1,N2)),(max (N1,N2)))) - g2 as
Element of
REAL by A17, XXREAL_0:48;
A19:
(f . ((max (N1,N2)),(max (N1,N2)))) - g2 in REAL
by A18, A17, XXREAL_0:48;
then A20:
f . (
(max (N1,N2)),
(max (N1,N2)))
<> +infty
by A10;
A21:
(- (f . ((max (N1,N2)),(max (N1,N2))))) + g1 = - ((f . ((max (N1,N2)),(max (N1,N2)))) - g1)
by XXREAL_3:26;
then A22:
|.((- (f . ((max (N1,N2)),(max (N1,N2))))) + g1).| < |.(g - h).| / 2
by A15, EXTREAL1:29;
then A23:
(- (f . ((max (N1,N2)),(max (N1,N2))))) + g1 < |.(g - h).| / 2
by EXTREAL1:21;
- (|.(g - h).| / 2) < (- (f . ((max (N1,N2)),(max (N1,N2))))) + g1
by A22, EXTREAL1:21;
then A24:
(- (f . ((max (N1,N2)),(max (N1,N2))))) + g1 in REAL
by A23, XXREAL_0:48;
A25:
f . (
(max (N1,N2)),
(max (N1,N2)))
<> -infty
by A10, A19;
|.(g1 - g2).| =
|.((g1 + 0.) - g2).|
by XXREAL_3:4
.=
|.((g1 + ((f . ((max (N1,N2)),(max (N1,N2)))) + (- (f . ((max (N1,N2)),(max (N1,N2))))))) - g2).|
by XXREAL_3:7
.=
|.((((- (f . ((max (N1,N2)),(max (N1,N2))))) + g1) + (f . ((max (N1,N2)),(max (N1,N2))))) - g2).|
by A8, A20, A25, XXREAL_3:29
.=
|.(((- (f . ((max (N1,N2)),(max (N1,N2))))) + g1) + ((f . ((max (N1,N2)),(max (N1,N2)))) - g2)).|
by A10, A24, XXREAL_3:30
;
then
|.(g1 - g2).| <= |.((- (f . ((max (N1,N2)),(max (N1,N2))))) + g1).| + |.((f . ((max (N1,N2)),(max (N1,N2)))) - g2).|
by EXTREAL1:24;
then A26:
|.(g1 - g2).| <= |.((f . ((max (N1,N2)),(max (N1,N2)))) - g1).| + |.((f . ((max (N1,N2)),(max (N1,N2)))) - g2).|
by A21, EXTREAL1:29;
(
|.((f . ((max (N1,N2)),(max (N1,N2)))) - g2).| < +infty &
|.((f . ((max (N1,N2)),(max (N1,N2)))) - g2).| >= 0 )
by A19, EXTREAL1:41, EXTREAL1:14;
then
|.((f . ((max (N1,N2)),(max (N1,N2)))) - g2).| in REAL
by XXREAL_0:14;
then A27:
|.((f . ((max (N1,N2)),(max (N1,N2)))) - g1).| + |.((f . ((max (N1,N2)),(max (N1,N2)))) - g2).| < (|.(g - h).| / 2) + |.((f . ((max (N1,N2)),(max (N1,N2)))) - g2).|
by A15, XXREAL_3:43;
|.(g - h).| / 2
in REAL
by XREAL_0:def 1;
then
(|.(g - h).| / 2) + |.((f . ((max (N1,N2)),(max (N1,N2)))) - g2).| < (|.(g - h).| / 2) + (|.(g - h).| / 2)
by A16, XXREAL_3:43;
then A28:
|.((f . ((max (N1,N2)),(max (N1,N2)))) - g1).| + |.((f . ((max (N1,N2)),(max (N1,N2)))) - g2).| < (|.(g - h).| / 2) + (|.(g - h).| / 2)
by A27, XXREAL_0:2;
g - h = g1 - g2
by A8, A10, SUPINF_2:3;
hence
contradiction
by A28, A26, EXTREAL1:12;
verum end;