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