let X be NormedLinearTopSpace; for RNS being RealNormSpace
for t being sequence of X
for s being sequence of RNS st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & t = s & t is convergent holds
( s is convergent & lim s = lim t )
let RNS be RealNormSpace; for t being sequence of X
for s being sequence of RNS st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & t = s & t is convergent holds
( s is convergent & lim s = lim t )
let t2 be sequence of X; for s being sequence of RNS st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & t2 = s & t2 is convergent holds
( s is convergent & lim s = lim t2 )
let s2 be sequence of RNS; ( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & t2 = s2 & t2 is convergent implies ( s2 is convergent & lim s2 = lim t2 ) )
assume A1:
( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & t2 = s2 & t2 is convergent )
; ( s2 is convergent & lim s2 = lim t2 )
reconsider y = lim t2 as Point of RNS by A1;
A2:
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((s2 . n) - y).|| < r
hence
s2 is convergent
; lim s2 = lim t2
hence
lim s2 = lim t2
by A2, NORMSP_1:def 7; verum