let seq be sequence of X; :: thesis: ( seq is constant implies seq is Cauchy )
assume A1: seq is constant ; :: thesis: seq is Cauchy
let r be Real; :: according to BHSP_3:def 1 :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r
let n, m be Nat; :: thesis: ( n >= k & m >= k implies dist ((seq . n),(seq . m)) < r )
assume that
n >= k and
m >= k ; :: thesis: 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; :: thesis: verum