theorem Th11: :: COUSIN:14

for n being Nat
for s1 being sequence of (Euclid n)
for s2 being sequence of (REAL-NS n) st s1 = s2 holds
( s1 is Cauchy iff s2 is Cauchy_sequence_by_Norm )