let seq be Complex_Sequence; :: thesis: ( seq is constant implies seq is convergent )
assume seq is constant ; :: thesis: seq is convergent
then consider t being Element of COMPLEX such that
A1: for n being Nat holds seq . n = t by VALUED_0:def 18;
take g = t; :: according to COMSEQ_2:def 4 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= |.((seq . b₃) - g).| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= |.((seq . b₂) - g).| ) )
assume A2: 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= |.((seq . b₂) - g).| )
take n = 0 ; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not p <= |.((seq . b₁) - g).| )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= |.((seq . m) - g).| )
assume n <= m ; :: thesis: not p <= |.((seq . m) - g).|
|.((seq . m) - g).| = |.(t - g).| by A1
.= 0 by COMPLEX1:44 ;
hence |.((seq . m) - g).| < p by A2; :: thesis: verum