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