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
now :: thesis: for k being Element of NAT holds lim seq = seq . k
let k be Element of NAT ; :: thesis: lim seq = seq . k
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
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;
hence lim seq = seq . k by A3, NORMSP_1:def 7; :: thesis: verum
end;
hence for k being Element of NAT holds lim seq = seq . k ; :: thesis: verum