let seq be sequence of X; :: thesis: ( seq is constant implies seq is convergent )

assume seq is constant ; :: thesis: seq is convergent

then consider x being Point of X such that

A1: for n being Nat holds seq . n = x by VALUED_0:def 18;

take g = x; :: according to BHSP_2:def 1 :: thesis: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),g) < r

let r be Real; :: thesis: ( r > 0 implies ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),g) < r )

assume A2: r > 0 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),g) < r

take m = 0 ; :: thesis: for n being Nat st n >= m holds

dist ((seq . n),g) < r

let n be Nat; :: thesis: ( n >= m implies dist ((seq . n),g) < r )

assume n >= m ; :: thesis: dist ((seq . n),g) < r

dist ((seq . n),g) = dist (x,g) by A1

.= 0 by BHSP_1:34 ;

hence dist ((seq . n),g) < r by A2; :: thesis: verum

assume seq is constant ; :: thesis: seq is convergent

then consider x being Point of X such that

A1: for n being Nat holds seq . n = x by VALUED_0:def 18;

take g = x; :: according to BHSP_2:def 1 :: thesis: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),g) < r

let r be Real; :: thesis: ( r > 0 implies ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),g) < r )

assume A2: r > 0 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),g) < r

take m = 0 ; :: thesis: for n being Nat st n >= m holds

dist ((seq . n),g) < r

let n be Nat; :: thesis: ( n >= m implies dist ((seq . n),g) < r )

assume n >= m ; :: thesis: dist ((seq . n),g) < r

dist ((seq . n),g) = dist (x,g) by A1

.= 0 by BHSP_1:34 ;

hence dist ((seq . n),g) < r by A2; :: thesis: verum