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