for X being ComplexNormSpace
for seq being sequence of X st seq is convergent holds
for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < s