for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent holds
( lim seq = g iff for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((seq . n) - g).|| < r )