let X be RealNormSpace; :: thesis: for seq being sequence of X st seq is constant holds

( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) )

let seq be sequence of X; :: thesis: ( seq is constant implies ( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) ) )

assume A1: seq is constant ; :: thesis: ( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) )

then consider r being Point of X such that

A2: for n being Nat holds seq . n = r by VALUED_0:def 18;

thus A3: seq is convergent by A1, LOPBAN_3:12; :: thesis: for k being Element of NAT holds lim seq = seq . k

( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) )

let seq be sequence of X; :: thesis: ( seq is constant implies ( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) ) )

assume A1: seq is constant ; :: thesis: ( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) )

then consider r being Point of X such that

A2: for n being Nat holds seq . n = r by VALUED_0:def 18;

thus A3: seq is convergent by A1, LOPBAN_3:12; :: thesis: for k being Element of NAT holds lim seq = seq . k

now :: thesis: for k being Element of NAT holds lim seq = seq . k

hence
for k being Element of NAT holds lim seq = seq . k
; :: thesis: verumlet k be Element of NAT ; :: thesis: lim seq = seq . k

end;now :: thesis: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . k)).|| < p

hence
lim seq = seq . k
by A3, NORMSP_1:def 7; :: thesis: verumex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . k)).|| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . k)).|| < p )

assume A4: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . k)).|| < p

reconsider n = 0 as Nat ;

take n = n; :: thesis: for m being Nat st n <= m holds

||.((seq . m) - (seq . k)).|| < p

let m be Nat; :: thesis: ( n <= m implies ||.((seq . m) - (seq . k)).|| < p )

assume n <= m ; :: thesis: ||.((seq . m) - (seq . k)).|| < p

||.((seq . m) - (seq . k)).|| = ||.(r - (seq . k)).|| by A2

.= ||.(r - r).|| by A2

.= ||.(0. X).|| by RLVECT_1:15

.= 0 by NORMSP_1:1 ;

hence ||.((seq . m) - (seq . k)).|| < p by A4; :: thesis: verum

end;for m being Nat st n <= m holds

||.((seq . m) - (seq . k)).|| < p )

assume A4: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . k)).|| < p

reconsider n = 0 as Nat ;

take n = n; :: thesis: for m being Nat st n <= m holds

||.((seq . m) - (seq . k)).|| < p

let m be Nat; :: thesis: ( n <= m implies ||.((seq . m) - (seq . k)).|| < p )

assume n <= m ; :: thesis: ||.((seq . m) - (seq . k)).|| < p

||.((seq . m) - (seq . k)).|| = ||.(r - (seq . k)).|| by A2

.= ||.(r - r).|| by A2

.= ||.(0. X).|| by RLVECT_1:15

.= 0 by NORMSP_1:1 ;

hence ||.((seq . m) - (seq . k)).|| < p by A4; :: thesis: verum