theorem Th5: :: CLOPBAN3:5

for X being ComplexNormSpace
for seq being sequence of X holds
( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < p )