for seq being Real_Sequence
for seq1 being sequence of RNS_Real st seq = seq1 holds
( seq is convergent iff seq1 is convergent )