for n being Nat
for f being sequence of (REAL-NS n) st f is Cauchy_sequence_by_Norm holds
f is convergent