let X be ComplexNormSpace; :: 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 r being Element of X such that
A1: for n being Nat holds seq . n = r by VALUED_0:def 18;
take g = r; :: according to CLVECT_1:def 15 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= ||.((seq . b₃) - g).|| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= ||.((seq . b₂) - g).|| ) )
assume A2: 0 < p ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= ||.((seq . b₂) - g).|| )
take n = 0 ; :: thesis: for b₁ being set holds
( not n <= b₁ or not p <= ||.((seq . b₁) - g).|| )
let m be Nat; :: thesis: ( not n <= m or not p <= ||.((seq . m) - g).|| )
assume n <= m ; :: thesis: not p <= ||.((seq . m) - g).||
||.((seq . m) - g).|| = ||.(r - g).|| by A1
.= ||.(0. X).|| by RLVECT_1:15
.= 0 ;
hence not p <= ||.((seq . m) - g).|| by A2; :: thesis: verum