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 S is_convergent_in_metrspace_to x ; :: thesis: lim S = x
then ( S is convergent & ( 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 Def8, Th21;
hence lim S = x by TBSP_1:def 3; :: thesis: verum