defpred S_{1}[ R_eal] means ( ex g being Real st

( $1 = g & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - $1).| < p ) & seq is convergent_to_finite_number ) or ( $1 = +infty & seq is convergent_to_+infty ) or ( $1 = -infty & seq is convergent_to_-infty ) );

given g1, g2 being R_eal such that A4: S_{1}[g1]
and

A5: S_{1}[g2]
and

A6: g1 <> g2 ; :: thesis: contradiction

( $1 = g & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - $1).| < p ) & seq is convergent_to_finite_number ) or ( $1 = +infty & seq is convergent_to_+infty ) or ( $1 = -infty & seq is convergent_to_-infty ) );

given g1, g2 being R_eal such that A4: S

A5: S

A6: g1 <> g2 ; :: thesis: contradiction

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

end;

suppose A7:
seq is 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 m being Nat st n <= m holds

|.((seq . m) - g1).| < p and

seq is convergent_to_finite_number by A4, Th50, Th51;

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 m being Nat st n <= m holds

|.((seq . m) - g2).| < p and

seq is convergent_to_finite_number by A5, A7, Th50, Th51;

reconsider g = g, h = h as Complex ;

g - h <> 0 by A6, A8, A10;

then A12: |.(g - h).| > 0 ;

then consider n1 being Nat such that

A13: for m being Nat st n1 <= m holds

|.((seq . m) - g1).| < |.(g - h).| / 2 by A9;

consider n2 being Nat such that

A14: for m being Nat st n2 <= m holds

|.((seq . m) - g2).| < |.(g - h).| / 2 by A11, A12;

reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;

set m = max (n1,n2);

A15: |.((seq . (max (n1,n2))) - g1).| < |.(g - h).| / 2 by A13, XXREAL_0:25;

A16: |.((seq . (max (n1,n2))) - g2).| < |.(g - h).| / 2 by A14, XXREAL_0:25;

reconsider g = g, h = h as Complex ;

A17: (seq . (max (n1,n2))) - g2 < |.(g - h).| / 2 by A16, EXTREAL1:21;

A18: - (|.(g - h).| / 2) < (seq . (max (n1,n2))) - g2 by A16, EXTREAL1:21;

then reconsider w = (seq . (max (n1,n2))) - g2 as Element of REAL by A17, XXREAL_0:48;

A19: (seq . (max (n1,n2))) - g2 in REAL by A18, A17, XXREAL_0:48;

then A20: seq . (max (n1,n2)) <> +infty by A10;

A21: (- (seq . (max (n1,n2)))) + g1 = - ((seq . (max (n1,n2))) - g1) by XXREAL_3:26;

then A22: |.((- (seq . (max (n1,n2)))) + g1).| < |.(g - h).| / 2 by A15, EXTREAL1:29;

then A23: (- (seq . (max (n1,n2)))) + g1 < |.(g - h).| / 2 by EXTREAL1:21;

- (|.(g - h).| / 2) < (- (seq . (max (n1,n2)))) + g1 by A22, EXTREAL1:21;

then A24: (- (seq . (max (n1,n2)))) + g1 in REAL by A23, XXREAL_0:48;

A25: seq . (max (n1,n2)) <> -infty by A10, A19;

|.(g1 - g2).| = |.((g1 + 0.) - g2).| by XXREAL_3:4

.= |.((g1 + ((seq . (max (n1,n2))) + (- (seq . (max (n1,n2)))))) - g2).| by XXREAL_3:7

.= |.((((- (seq . (max (n1,n2)))) + g1) + (seq . (max (n1,n2)))) - g2).| by A8, A20, A25, XXREAL_3:29

.= |.(((- (seq . (max (n1,n2)))) + g1) + ((seq . (max (n1,n2))) - g2)).| by A10, A24, XXREAL_3:30 ;

then |.(g1 - g2).| <= |.((- (seq . (max (n1,n2)))) + g1).| + |.((seq . (max (n1,n2))) - g2).| by EXTREAL1:24;

then A26: |.(g1 - g2).| <= |.((seq . (max (n1,n2))) - g1).| + |.((seq . (max (n1,n2))) - g2).| by A21, EXTREAL1:29;

|.w.| in REAL by XREAL_0:def 1;

then |.((seq . (max (n1,n2))) - g2).| in REAL ;

then A27: |.((seq . (max (n1,n2))) - g1).| + |.((seq . (max (n1,n2))) - g2).| < (|.(g - h).| / 2) + |.((seq . (max (n1,n2))) - g2).| by A15, XXREAL_3:43;

|.(g - h).| / 2 in REAL by XREAL_0:def 1;

then |.(g - h).| / 2 in REAL ;

then (|.(g - h).| / 2) + |.((seq . (max (n1,n2))) - g2).| < (|.(g - h).| / 2) + (|.(g - h).| / 2) by A16, XXREAL_3:43;

then A28: |.((seq . (max (n1,n2))) - g1).| + |.((seq . (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;

then |.(g - h).| = |.(g1 - g2).| by EXTREAL1:12;

then |.(g - h).| < (|.(g - h).| / 2) + (|.(g - h).| / 2) by A28, A26;

hence contradiction ; :: thesis: verum

end;A8: g1 = g and

A9: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - g1).| < p and

seq is convergent_to_finite_number by A4, Th50, Th51;

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 m being Nat st n <= m holds

|.((seq . m) - g2).| < p and

seq is convergent_to_finite_number by A5, A7, Th50, Th51;

reconsider g = g, h = h as Complex ;

g - h <> 0 by A6, A8, A10;

then A12: |.(g - h).| > 0 ;

then consider n1 being Nat such that

A13: for m being Nat st n1 <= m holds

|.((seq . m) - g1).| < |.(g - h).| / 2 by A9;

consider n2 being Nat such that

A14: for m being Nat st n2 <= m holds

|.((seq . m) - g2).| < |.(g - h).| / 2 by A11, A12;

reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;

set m = max (n1,n2);

A15: |.((seq . (max (n1,n2))) - g1).| < |.(g - h).| / 2 by A13, XXREAL_0:25;

A16: |.((seq . (max (n1,n2))) - g2).| < |.(g - h).| / 2 by A14, XXREAL_0:25;

reconsider g = g, h = h as Complex ;

A17: (seq . (max (n1,n2))) - g2 < |.(g - h).| / 2 by A16, EXTREAL1:21;

A18: - (|.(g - h).| / 2) < (seq . (max (n1,n2))) - g2 by A16, EXTREAL1:21;

then reconsider w = (seq . (max (n1,n2))) - g2 as Element of REAL by A17, XXREAL_0:48;

A19: (seq . (max (n1,n2))) - g2 in REAL by A18, A17, XXREAL_0:48;

then A20: seq . (max (n1,n2)) <> +infty by A10;

A21: (- (seq . (max (n1,n2)))) + g1 = - ((seq . (max (n1,n2))) - g1) by XXREAL_3:26;

then A22: |.((- (seq . (max (n1,n2)))) + g1).| < |.(g - h).| / 2 by A15, EXTREAL1:29;

then A23: (- (seq . (max (n1,n2)))) + g1 < |.(g - h).| / 2 by EXTREAL1:21;

- (|.(g - h).| / 2) < (- (seq . (max (n1,n2)))) + g1 by A22, EXTREAL1:21;

then A24: (- (seq . (max (n1,n2)))) + g1 in REAL by A23, XXREAL_0:48;

A25: seq . (max (n1,n2)) <> -infty by A10, A19;

|.(g1 - g2).| = |.((g1 + 0.) - g2).| by XXREAL_3:4

.= |.((g1 + ((seq . (max (n1,n2))) + (- (seq . (max (n1,n2)))))) - g2).| by XXREAL_3:7

.= |.((((- (seq . (max (n1,n2)))) + g1) + (seq . (max (n1,n2)))) - g2).| by A8, A20, A25, XXREAL_3:29

.= |.(((- (seq . (max (n1,n2)))) + g1) + ((seq . (max (n1,n2))) - g2)).| by A10, A24, XXREAL_3:30 ;

then |.(g1 - g2).| <= |.((- (seq . (max (n1,n2)))) + g1).| + |.((seq . (max (n1,n2))) - g2).| by EXTREAL1:24;

then A26: |.(g1 - g2).| <= |.((seq . (max (n1,n2))) - g1).| + |.((seq . (max (n1,n2))) - g2).| by A21, EXTREAL1:29;

|.w.| in REAL by XREAL_0:def 1;

then |.((seq . (max (n1,n2))) - g2).| in REAL ;

then A27: |.((seq . (max (n1,n2))) - g1).| + |.((seq . (max (n1,n2))) - g2).| < (|.(g - h).| / 2) + |.((seq . (max (n1,n2))) - g2).| by A15, XXREAL_3:43;

|.(g - h).| / 2 in REAL by XREAL_0:def 1;

then |.(g - h).| / 2 in REAL ;

then (|.(g - h).| / 2) + |.((seq . (max (n1,n2))) - g2).| < (|.(g - h).| / 2) + (|.(g - h).| / 2) by A16, XXREAL_3:43;

then A28: |.((seq . (max (n1,n2))) - g1).| + |.((seq . (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;

then |.(g - h).| = |.(g1 - g2).| by EXTREAL1:12;

then |.(g - h).| < (|.(g - h).| / 2) + (|.(g - h).| / 2) by A28, A26;

hence contradiction ; :: thesis: verum

suppose
( seq is convergent_to_+infty or seq is convergent_to_-infty )
; :: thesis: contradiction

end;

end;