let X be non empty MetrSpace; for x, y being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y holds
x = y
let x, y be Element of X; for S being sequence of X st S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y holds
x = y
let S be sequence of X; ( S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y implies x = y )
assume that
A1:
S is_convergent_in_metrspace_to x
and
A2:
S is_convergent_in_metrspace_to y
; x = y
A3:
lim S = y
by A2, Th12;
A4:
for n being Nat holds (sequence_of_dist (S,S)) . n = In (0,REAL)
A5:
ex n being Nat st (sequence_of_dist (S,S)) . n = 0
( lim S = x & S is convergent )
by A1, Th12;
then A6:
dist (x,y) = lim (sequence_of_dist (S,S))
by A3, Th21;
sequence_of_dist (S,S) is constant
by A4, VALUED_0:def 18;
then
dist (x,y) = 0
by A6, A5, SEQ_4:25;
hence
x = y
by METRIC_1:2; verum