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 & lim S = 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 & lim S = x ) )
assume S is convergent ; :: thesis: ex x being Element of X st
( S is_convergent_in_metrspace_to x & lim S = x )
then ex x being Element of X st S is_convergent_in_metrspace_to x by Th10;
hence ex x being Element of X st
( S is_convergent_in_metrspace_to x & lim S = x ) by Th11; :: thesis: verum