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: ( S is convergent & lim S = x ) by A1, Th27;
( S is convergent & lim S = y ) by A2, Th27;
then A4: dist x,y = lim (sequence_of_dist S,S) by A3, Th36;
A5: for n being Nat holds (sequence_of_dist S,S) . n = 0

proof

let n be Nat; :: thesis: (sequence_of_dist S,S) . n = 0
n in NAT by ORDINAL1:def 13;
then (sequence_of_dist S,S) . n = dist (S . n),(S . n) by Def15
.= 0 by METRIC_1:1 ;
hence (sequence_of_dist S,S) . n = 0 ; :: thesis: verum

end;

then A6: sequence_of_dist S,S is constant by VALUED_0:def 18;
ex n being Element of 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 A5; :: thesis: verum

end;

then dist x,y = 0 by A4, A6, SEQ_4:40;
hence x = y by METRIC_1:2; :: thesis: verum