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 ; :: thesis: 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 ; :: thesis: contradiction
then 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; :: thesis: verum
end;
suppose ( f is P-convergent_to_+infty or f is P-convergent_to_-infty ) ; :: thesis: contradiction
hence contradiction by A4, A5, A6, Th93, Th94; :: thesis: verum
end;
end;