for X being NormedLinearTopSpace
for RNS being RealNormSpace
for s being sequence of X
for t 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 #) & s = t holds
( s is convergent iff t is convergent )