:: deftheorem defines convergent CLVECT_1:def 15 :
for CNS being ComplexNormSpace
for S being sequence of CNS holds
( S is convergent iff ex g being Point of CNS st
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - g).|| < r );