let X be non empty MetrSpace; :: thesis: for x being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x holds
lim S = x
let x be Element of X; :: thesis: for S being sequence of X st S is_convergent_in_metrspace_to x holds
lim S = x
let S be sequence of X; :: thesis: ( S is_convergent_in_metrspace_to x implies lim S = x )
assume A1: S is_convergent_in_metrspace_to x ; :: thesis: lim S = x
then A2: S is convergent by Th21;
for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist (S . n),x < r by A1, Def8;
hence lim S = x by A2, TBSP_1:def 4; :: thesis: verum