let X be non empty MetrSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: x = y
A3: lim S = y by A2, Th12;
A4: for n being Nat holds (sequence_of_dist (S,S)) . n = In (0,REAL)

proof

let n be Nat; :: thesis: (sequence_of_dist (S,S)) . n = In (0,REAL)
(sequence_of_dist (S,S)) . n = dist ((S . n),(S . n)) by Def7
.= 0 by METRIC_1:1 ;
hence (sequence_of_dist (S,S)) . n = In (0,REAL) ; :: thesis: verum

end;

A5: ex n being Nat st (sequence_of_dist (S,S)) . n = 0

proof

take 0 ; :: thesis: (sequence_of_dist (S,S)) . 0 = 0
thus (sequence_of_dist (S,S)) . 0 = 0 by A4; :: thesis: verum

end;

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