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 & ( 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 ) & seq is convergent_to_finite_number ) by A3, Th56, Th57;
consider h being real number such that
A8: ( g2 = h & ( 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 ) & 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, A8;
then B9: |.(g - h).| > 0 by COMPLEX1:133;
consider n1 being Nat such that
A10: for m being Nat st n1 <= m holds
|.((seq . m) - g1).| < R_EAL (|.(g - h).| / 2) by A7, B9;
consider n2 being Nat such that
A11: for m being Nat st n2 <= m holds
|.((seq . m) - g2).| < R_EAL (|.(g - h).| / 2) by A8, B9;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 13;
set m = max n1,n2;
( n1 <= max n1,n2 & n2 <= max n1,n2 ) by XXREAL_0:25;
then A12: ( |.((seq . (max n1,n2)) - g1).| < R_EAL (|.(g - h).| / 2) & |.((seq . (max n1,n2)) - g2).| < R_EAL (|.(g - h).| / 2) ) by A10, A11;
reconsider g = g, h = h as Real by XREAL_0:def 1;
A13: (- (seq . (max n1,n2))) + g1 = - ((seq . (max n1,n2)) - g1) by XXREAL_3:27;
then |.((- (seq . (max n1,n2))) + g1).| < R_EAL (|.(g - h).| / 2) by A12, EXTREAL2:66;
then A14: ( - (R_EAL (|.(g - h).| / 2)) < (- (seq . (max n1,n2))) + g1 & (- (seq . (max n1,n2))) + g1 < R_EAL (|.(g - h).| / 2) & - (R_EAL (|.(g - h).| / 2)) < (seq . (max n1,n2)) - g2 & (seq . (max n1,n2)) - g2 < R_EAL (|.(g - h).| / 2) ) by A12, EXTREAL2:58;
then A15: ( (- (seq . (max n1,n2))) + g1 in REAL & (seq . (max n1,n2)) - g2 in REAL ) by XXREAL_0:48;
reconsider w = (seq . (max n1,n2)) - g2 as Real by A14, XXREAL_0:48;
|.w.| in REAL by XREAL_0:def 1;
then |.((seq . (max n1,n2)) - g2).| in REAL by EXTREAL2:49;
then ( |.((seq . (max n1,n2)) - g1).| + |.((seq . (max n1,n2)) - g2).| < (R_EAL (|.(g - h).| / 2)) + |.((seq . (max n1,n2)) - g2).| & (R_EAL (|.(g - h).| / 2)) + |.((seq . (max n1,n2)) - g2).| < (R_EAL (|.(g - h).| / 2)) + (R_EAL (|.(g - h).| / 2)) ) by A12, XXREAL_3:47;
then A16: |.((seq . (max n1,n2)) - g1).| + |.((seq . (max n1,n2)) - g2).| < (R_EAL (|.(g - h).| / 2)) + (R_EAL (|.(g - h).| / 2)) by XXREAL_0:2;
( (- (seq . (max n1,n2))) + g1 <> +infty & (- (seq . (max n1,n2))) + g1 <> -infty & (seq . (max n1,n2)) - g2 <> +infty & (seq . (max n1,n2)) - g2 <> -infty & (seq . (max n1,n2)) - g2 < +infty & -infty < (seq . (max n1,n2)) - g2 ) by A15, XXREAL_0:9, XXREAL_0:12;
then A18: ( seq . (max n1,n2) <> +infty & seq . (max n1,n2) <> -infty ) by A8, XXREAL_3:13, XXREAL_3:14;
|.(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, A18, XXREAL_3:30
.= |.(((- (seq . (max n1,n2))) + g1) + ((seq . (max n1,n2)) - g2)).| by A8, A15, XXREAL_3:31 ;
then |.(g1 - g2).| <= |.((- (seq . (max n1,n2))) + g1).| + |.((seq . (max n1,n2)) - g2).| by A15, EXTREAL2:61;
then A19: |.(g1 - g2).| <= |.((seq . (max n1,n2)) - g1).| + |.((seq . (max n1,n2)) - g2).| by A13, EXTREAL2:66;
A20: (R_EAL (|.(g - h).| / 2)) + (R_EAL (|.(g - h).| / 2)) = (|.(g - h).| / 2) + (|.(g - h).| / 2) by SUPINF_2:1;
g - h = g1 - g2 by A7, A8, SUPINF_2:5;
hence contradiction by A16, A19, A20, 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;