let X be non empty MetrSpace; :: thesis: for S being sequence of X st S is constant holds
S is convergent
let S be sequence of X; :: thesis: ( S is constant implies S is convergent )
assume S is constant ; :: thesis: S is convergent
then consider x being Element of X such that
A1: for n being Nat holds S . n = x by VALUED_0:def 18;
take x ; :: according to TBSP_1:def 3 :: 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 ) )
let r be Real; :: thesis: ( r <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not r <= dist (S . b₂),x ) )
assume A2: 0 < r ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not r <= dist (S . b₂),x )
take k = 0 ; :: thesis: for b₁ being Element of NAT holds
( not k <= b₁ or not r <= dist (S . b₁),x )

now

let n be Element of NAT ; :: thesis: ( k <= n implies dist (S . n),x < r )
assume k <= n ; :: thesis: dist (S . n),x < r
dist (S . n),x = dist x,x by A1
.= 0 by METRIC_1:1 ;
hence dist (S . n),x < r by A2; :: thesis: verum

end;

hence for n being Element of NAT st k <= n holds
dist (S . n),x < r ; :: thesis: verum