let seq be sequence of X; ( seq is constant implies seq is Cauchy )
assume A1:
seq is constant
; seq is Cauchy
let r be Real; BHSP_3:def 1 ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r )
assume A2:
r > 0
; ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r
take k = 0 ; for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r
let n, m be Nat; ( n >= k & m >= k implies dist ((seq . n),(seq . m)) < r )
assume that
n >= k
and
m >= k
; dist ((seq . n),(seq . m)) < r
dist ((seq . n),(seq . m)) =
dist ((seq . n),(seq . n))
by A1, VALUED_0:23
.=
0
by BHSP_1:34
;
hence
dist ((seq . n),(seq . m)) < r
by A2; verum