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 consider x being Element of X such that
A1: S is_convergent_in_metrspace_to x by Th22;
thus ex x being Element of X st
( S is_convergent_in_metrspace_to x & lim S = x ) by A1, Th26; :: thesis: verum