given g1, g2 being Point of (TOP-REAL N) such that A2:
for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g1).| < r
and
A3:
for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g2).| < r
and
A4:
g1 <> g2
; contradiction
then consider n1 being Nat such that
A6:
for m being Nat st n1 <= m holds
|.((seq . m) - g1).| < |.(g1 - g2).| / 4
by A2, XREAL_1:224;
consider n2 being Nat such that
A7:
for m being Nat st n2 <= m holds
|.((seq . m) - g2).| < |.(g1 - g2).| / 4
by A3, A5, XREAL_1:224;
A8:
|.((seq . (n1 + n2)) - g2).| < |.(g1 - g2).| / 4
by A7, NAT_1:12;
|.((seq . (n1 + n2)) - g1).| < |.(g1 - g2).| / 4
by A6, NAT_1:12;
then A9:
|.((seq . (n1 + n2)) - g2).| + |.((seq . (n1 + n2)) - g1).| < (|.(g1 - g2).| / 4) + (|.(g1 - g2).| / 4)
by A8, XREAL_1:8;
|.(g1 - g2).| =
|.((g1 - g2) + (0. (TOP-REAL N))).|
by RLVECT_1:4
.=
|.((g1 - g2) + ((- 1) * (0. (TOP-REAL N)))).|
by RLVECT_1:10
.=
|.((g1 - g2) + (- (0. (TOP-REAL N)))).|
by RLVECT_1:16
.=
|.((g1 - g2) - (0. (TOP-REAL N))).|
.=
|.((g1 - g2) - ((seq . (n1 + n2)) - (seq . (n1 + n2)))).|
by RLVECT_1:5
.=
|.(((g1 - g2) - (seq . (n1 + n2))) + (seq . (n1 + n2))).|
by RLVECT_1:29
.=
|.((g1 - ((seq . (n1 + n2)) + g2)) + (seq . (n1 + n2))).|
by RLVECT_1:27
.=
|.(((g1 - (seq . (n1 + n2))) - g2) + (seq . (n1 + n2))).|
by RLVECT_1:27
.=
|.((g1 - (seq . (n1 + n2))) - (g2 - (seq . (n1 + n2)))).|
by RLVECT_1:29
.=
|.((g1 - (seq . (n1 + n2))) + (- (g2 - (seq . (n1 + n2))))).|
.=
|.((g1 - (seq . (n1 + n2))) + ((seq . (n1 + n2)) - g2)).|
by RLVECT_1:33
.=
|.((- ((seq . (n1 + n2)) - g1)) + ((seq . (n1 + n2)) - g2)).|
by RLVECT_1:33
;
then
|.(g1 - g2).| <= |.(- ((seq . (n1 + n2)) - g1)).| + |.((seq . (n1 + n2)) - g2).|
by Th29;
then A10:
|.(g1 - g2).| <= |.((seq . (n1 + n2)) - g1).| + |.((seq . (n1 + n2)) - g2).|
by EUCLID:71;
|.(g1 - g2).| / 2 < |.(g1 - g2).|
by A5, XREAL_1:216;
hence
contradiction
by A9, A10, XXREAL_0:2; verum