theorem Th20: :: C0SP3:20

for X being NormedLinearTopSpace
for S being sequence of X
for x being Point of X holds
( S is_convergent_to x iff for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r )