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
S is convergent
let x be Element of X; :: thesis: for S being sequence of X st S is_convergent_in_metrspace_to x holds
S is convergent
let S be sequence of X; :: thesis: ( S is_convergent_in_metrspace_to x implies S is convergent )
assume A1: S is_convergent_in_metrspace_to x ; :: thesis: S is convergent
take x ; :: according to TBSP_1:def 2 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= dist ((S . b₃),x) ) )
thus for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= dist ((S . b₃),x) ) ) by A1, Def8; :: thesis: verum