theorem :: REAL_NS1:17

for n being Nat
for seq1 being sequence of (REAL-NS n)
for seq2 being sequence of (REAL-US n) st seq1 = seq2 & seq1 is Cauchy_sequence_by_Norm holds
seq2 is Cauchy