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 b1 being object holds
( b1 <= 0 or ex b2 being set st
for b3 being set holds
( not b2 <= b3 or not b1 <= ||.((seq . b3) - g).|| ) )

let p be Real; :: thesis: ( p <= 0 or ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not p <= ||.((seq . b2) - g).|| ) )

assume A2: 0 < p ; :: thesis: ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not p <= ||.((seq . b2) - g).|| )

take n = 0 ; :: thesis: for b1 being set holds
( not n <= b1 or not p <= ||.((seq . b1) - 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