theorem Th12: :: REAL_NS1:12

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