let X be non empty MetrSpace; :: thesis: for S being sequence of X st S is convergent holds
ex x being Element of X st S is_convergent_in_metrspace_to x
let S be sequence of X; :: thesis: ( S is convergent implies ex x being Element of X st S is_convergent_in_metrspace_to x )
assume S is convergent ; :: thesis: ex x being Element of X st S is_convergent_in_metrspace_to x
then consider x being Element of X such that
A1: 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 ;
S is_convergent_in_metrspace_to x by A1;
hence ex x being Element of X st S is_convergent_in_metrspace_to x ; :: thesis: verum