let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X st seq is constant holds
seq is Cauchy
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 CLVECT_2:def 8 :: thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (seq . n),(seq . m) < r )
assume A2: r > 0 ; :: thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (seq . n),(seq . m) < r
take k = 0 ; :: thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist (seq . n),(seq . m) < r
let n, m be Element of NAT ; :: thesis: ( n >= k & m >= k implies dist (seq . n),(seq . m) < r )
assume ( n >= k & 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 CSSPACE:53 ;
hence dist (seq . n),(seq . m) < r by A2; :: thesis: verum