for X being RealUnitarySpace
for s1 being sequence of X
for s2 being sequence of (RUSp2RNSp X) st s1 = s2 holds
( s1 is convergent iff s2 is convergent )