defpred S₁[ R_eal] means ( ex g being real number st
( $1 = g & ( for p being real number 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 A3: S₁[g1] and
A4: S₁[g2] and
A5: 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, Def11;

suppose A6: seq is convergent_to_finite_number ; :: thesis: contradiction

then consider g being real number such that
A7: g1 = g and
A8: for p being real number 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 A3, Th56, Th57;
consider h being real number such that
A9: g2 = h and
A10: for p being real number 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 A4, A6, Th56, Th57;
reconsider g = g, h = h as complex number ;
g - h <> 0 by A5, A7, A9;
then A11: |.(g - h).| > 0 by COMPLEX1:133;
then consider n1 being Nat such that
A12: for m being Nat st n1 <= m holds
|.((seq . m) - g1).| < R_EAL (|.(g - h).| / 2) by A8;
consider n2 being Nat such that
A13: for m being Nat st n2 <= m holds
|.((seq . m) - g2).| < R_EAL (|.(g - h).| / 2) by A10, A11;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 13;
set m = max n1,n2;
A14: |.((seq . (max n1,n2)) - g1).| < R_EAL (|.(g - h).| / 2) by A12, XXREAL_0:25;
A15: |.((seq . (max n1,n2)) - g2).| < R_EAL (|.(g - h).| / 2) by A13, XXREAL_0:25;
reconsider g = g, h = h as Real by XREAL_0:def 1;
A16: (seq . (max n1,n2)) - g2 < R_EAL (|.(g - h).| / 2) by A15, EXTREAL2:58;
A17: - (R_EAL (|.(g - h).| / 2)) < (seq . (max n1,n2)) - g2 by A15, EXTREAL2:58;
then reconsider w = (seq . (max n1,n2)) - g2 as Real by A16, XXREAL_0:48;
A18: (seq . (max n1,n2)) - g2 in REAL by A17, A16, XXREAL_0:48;
then A19: seq . (max n1,n2) <> +infty by A9;
A20: (- (seq . (max n1,n2))) + g1 = - ((seq . (max n1,n2)) - g1) by XXREAL_3:27;
then A21: |.((- (seq . (max n1,n2))) + g1).| < R_EAL (|.(g - h).| / 2) by A14, EXTREAL2:66;
then A22: (- (seq . (max n1,n2))) + g1 < R_EAL (|.(g - h).| / 2) by EXTREAL2:58;
- (R_EAL (|.(g - h).| / 2)) < (- (seq . (max n1,n2))) + g1 by A21, EXTREAL2:58;
then A23: (- (seq . (max n1,n2))) + g1 in REAL by A22, XXREAL_0:48;
A24: seq . (max n1,n2) <> -infty by A9, A18;
|.(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 A7, A19, A24, XXREAL_3:30
.= |.(((- (seq . (max n1,n2))) + g1) + ((seq . (max n1,n2)) - g2)).| by A9, A23, XXREAL_3:31 ;
then |.(g1 - g2).| <= |.((- (seq . (max n1,n2))) + g1).| + |.((seq . (max n1,n2)) - g2).| by EXTREAL2:61;
then A25: |.(g1 - g2).| <= |.((seq . (max n1,n2)) - g1).| + |.((seq . (max n1,n2)) - g2).| by A20, EXTREAL2:66;
A26: (R_EAL (|.(g - h).| / 2)) + (R_EAL (|.(g - h).| / 2)) = (|.(g - h).| / 2) + (|.(g - h).| / 2) by SUPINF_2:1;
|.w.| in REAL by XREAL_0:def 1;
then |.((seq . (max n1,n2)) - g2).| in REAL by EXTREAL2:49;
then A27: |.((seq . (max n1,n2)) - g1).| + |.((seq . (max n1,n2)) - g2).| < (R_EAL (|.(g - h).| / 2)) + |.((seq . (max n1,n2)) - g2).| by A14, XXREAL_3:47;
(R_EAL (|.(g - h).| / 2)) + |.((seq . (max n1,n2)) - g2).| < (R_EAL (|.(g - h).| / 2)) + (R_EAL (|.(g - h).| / 2)) by A15, XXREAL_3:47;
then A28: |.((seq . (max n1,n2)) - g1).| + |.((seq . (max n1,n2)) - g2).| < (R_EAL (|.(g - h).| / 2)) + (R_EAL (|.(g - h).| / 2)) by A27, XXREAL_0:2;
g - h = g1 - g2 by A7, A9, SUPINF_2:5;
hence contradiction by A28, A25, A26, EXTREAL2:49; :: thesis: verum

end;

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

hence contradiction by A3, A4, A5, Th56, Th57; :: thesis: verum

end;

end;