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 ; :: thesis: 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; :: thesis: verum