let z1, z2 be Real; :: thesis: ( ( for e being Real st 0 < e holds
ex M being Nat st
for m being Nat st m >= M holds
|.(((lim_in_cod1 Rseq) . m) - z1).| < e ) & ( for e being Real st 0 < e holds
ex M being Nat st
for m being Nat st m >= M holds
|.(((lim_in_cod1 Rseq) . m) - z2).| < e ) implies z1 = z2 )
assume that
a4: for e being Real st 0 < e holds
ex M being Nat st
for m being Nat st m >= M holds
|.(((lim_in_cod1 Rseq) . m) - z1).| < e and
a5: for e being Real st 0 < e holds
ex M being Nat st
for m being Nat st m >= M holds
|.(((lim_in_cod1 Rseq) . m) - z2).| < e ; :: thesis: z1 = z2
assume a6: z1 <> z2 ; :: thesis: contradiction
set p = |.(z1 - z2).| / 2;
a7: |.(z1 - z2).| > 0 by a6, COMPLEX1:62;
then consider M1 being Nat such that
a8: for m being Nat st M1 <= m holds
|.(((lim_in_cod1 Rseq) . m) - z1).| < |.(z1 - z2).| / 2 by a4;
consider M2 being Nat such that
a9: for m being Nat st M2 <= m holds
|.(((lim_in_cod1 Rseq) . m) - z2).| < |.(z1 - z2).| / 2 by a5, a7;
set M = max (M1,M2);
a0: max (M1,M2) is Nat by TARSKI:1;
for m being Nat st max (M1,M2) <= m holds
2 * (|.(z1 - z2).| / 2) < 2 * (|.(z1 - z2).| / 2)

proof

let m be Nat; :: thesis: ( max (M1,M2) <= m implies 2 * (|.(z1 - z2).| / 2) < 2 * (|.(z1 - z2).| / 2) )
set s = lim_in_cod1 Rseq;
assume a10: max (M1,M2) <= m ; :: thesis: 2 * (|.(z1 - z2).| / 2) < 2 * (|.(z1 - z2).| / 2)
M2 <= max (M1,M2) by XXREAL_0:25;
then (max (M1,M2)) + M2 <= (max (M1,M2)) + m by a10, XREAL_1:7;
then M2 <= m by XREAL_1:6;
then a11: |.(((lim_in_cod1 Rseq) . m) - z2).| < |.(z1 - z2).| / 2 by a9;
|.(z1 - z2).| = |.((z1 - ((lim_in_cod1 Rseq) . m)) - (z2 - ((lim_in_cod1 Rseq) . m))).| ;
then |.(z1 - z2).| <= |.(z1 - ((lim_in_cod1 Rseq) . m)).| + |.(z2 - ((lim_in_cod1 Rseq) . m)).| by COMPLEX1:57;
then a12: |.(z1 - z2).| <= |.(((lim_in_cod1 Rseq) . m) - z1).| + |.(z2 - ((lim_in_cod1 Rseq) . m)).| by COMPLEX1:60;
M1 <= max (M1,M2) by XXREAL_0:25;
then (max (M1,M2)) + M1 <= (max (M1,M2)) + m by a10, XREAL_1:7;
then M1 <= m by XREAL_1:6;
then |.(((lim_in_cod1 Rseq) . m) - z1).| < |.(z1 - z2).| / 2 by a8;
then |.(((lim_in_cod1 Rseq) . m) - z1).| + |.(((lim_in_cod1 Rseq) . m) - z2).| < (|.(z1 - z2).| / 2) + (|.(z1 - z2).| / 2) by a11, XREAL_1:8;
hence 2 * (|.(z1 - z2).| / 2) < 2 * (|.(z1 - z2).| / 2) by a12, COMPLEX1:60; :: thesis: verum

end;

hence contradiction by a0; :: thesis: verum