let z1, z2 be Real; ( ( for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 Rseq) . n) - z1).| < e ) & ( for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 Rseq) . n) - 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_cod2 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_cod2 Rseq) . m) - z2).| < e
; z1 = z2
assume a6:
z1 <> z2
; 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_cod2 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_cod2 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;
( max (M1,M2) <= m implies 2 * (|.(z1 - z2).| / 2) < 2 * (|.(z1 - z2).| / 2) )
set s =
lim_in_cod2 Rseq;
assume a10:
max (
M1,
M2)
<= m
;
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_cod2 Rseq) . m) - z2).| < |.(z1 - z2).| / 2
by a9;
|.(z1 - z2).| = |.((z1 - ((lim_in_cod2 Rseq) . m)) - (z2 - ((lim_in_cod2 Rseq) . m))).|
;
then
|.(z1 - z2).| <= |.(z1 - ((lim_in_cod2 Rseq) . m)).| + |.(z2 - ((lim_in_cod2 Rseq) . m)).|
by COMPLEX1:57;
then a12:
|.(z1 - z2).| <= |.(((lim_in_cod2 Rseq) . m) - z1).| + |.(z2 - ((lim_in_cod2 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_cod2 Rseq) . m) - z1).| < |.(z1 - z2).| / 2
by a8;
then
|.(((lim_in_cod2 Rseq) . m) - z1).| + |.(((lim_in_cod2 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;
verum
end;
hence
contradiction
by a0; verum