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 2 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= dist ((S . b₃),x) ) )
let r be Real; :: thesis: ( r <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not r <= dist ((S . b₂),x) ) )
assume A2: 0 < r ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not r <= dist ((S . b₂),x) )
take k = 0 ; :: thesis: for b₁ being set holds
( not k <= b₁ or not r <= dist ((S . b₁),x) )

now :: thesis: for n being Nat st k <= n holds
dist ((S . n),x) < r

let n be 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 Nat st k <= n holds
dist ((S . n),x) < r ; :: thesis: verum