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 Nat st
for n being Nat st m <= n holds
dist ((S . n),x) < r ) ) ;
hence lim S = x by TBSP_1:def 3; :: thesis: verum