theorem :: CLVECT_2:58

for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is Cauchy iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )