let X be NormedLinearTopSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
||.((s2 . n) - y).|| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((s2 . n) - y).|| < r
then consider m being Nat such that
A3: for n being Nat st m <= n holds
||.((t2 . n) - (lim t2)).|| < r by A1, Th22;
take m ; :: thesis: for n being Nat st m <= n holds
||.((s2 . n) - y).|| < r
let n be Nat; :: thesis: ( m <= n implies ||.((s2 . n) - y).|| < r )
assume m <= n ; :: thesis: ||.((s2 . n) - y).|| < r
then ||.((t2 . n) - (lim t2)).|| < r by A3;
hence ||.((s2 . n) - y).|| < r by Th19, A1; :: thesis: verum

end;

hence s2 is convergent ; :: thesis: lim s2 = lim t2
hence lim s2 = lim t2 by A2, NORMSP_1:def 7; :: thesis: verum