let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X st seq is constant holds
seq is convergent
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 CLVECT_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 CSSPACE:50 ;
hence dist ((seq . n),g) < r by A2; :: thesis: verum