theorem RNS11: :: DUALSP03:7

for seq1 being sequence of RNS_Real st seq1 is Cauchy_sequence_by_Norm holds
seq1 is convergent