for X being 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 )