:: deftheorem Def2 defines lim CLVECT_2:def 2 :
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
for b₃ being Point of X holds
( b₃ = lim seq iff for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),b₃) < r );