let seq be Real_Sequence; :: thesis: ( seq is constant implies seq is convergent )
assume seq is constant ; :: thesis: seq is convergent
then consider r being Element of REAL such that
A1: for n being Nat holds seq . n = r by VALUED_0:def 18;
take g = r; :: according to SEQ_2:def 6 :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p )
assume A2: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p
take n = 0 ; :: thesis: for m being Nat st n <= m holds
|.((seq . m) - g).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - g).| < p )
assume n <= m ; :: thesis: |.((seq . m) - g).| < p
|.((seq . m) - g).| = |.(r - g).| by A1
.= 0 by ABSVALUE:2 ;
hence |.((seq . m) - g).| < p by A2; :: thesis: verum