let X be RealNormSpace; :: 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 NORMSP_1:def 6 :: thesis: for b_{1} being object holds

( b_{1} <= 0 or ex b_{2} being set st

for b_{3} being set holds

( not b_{2} <= b_{3} or not b_{1} <= ||.((seq . b_{3}) - g).|| ) )

let p be Real; :: thesis: ( p <= 0 or ex b_{1} being set st

for b_{2} being set holds

( not b_{1} <= b_{2} or not p <= ||.((seq . b_{2}) - g).|| ) )

assume A2: 0 < p ; :: thesis: ex b_{1} being set st

for b_{2} being set holds

( not b_{1} <= b_{2} or not p <= ||.((seq . b_{2}) - g).|| )

take n = 0 ; :: thesis: for b_{1} being set holds

( not n <= b_{1} or not p <= ||.((seq . b_{1}) - 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

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 NORMSP_1:def 6 :: thesis: for b

( b

for b

( not b

let p be Real; :: thesis: ( p <= 0 or ex b

for b

( not b

assume A2: 0 < p ; :: thesis: ex b

for b

( not b

take n = 0 ; :: thesis: for b

( not n <= b

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