theorem Th21: :: C0SP3:21

for X being NormedLinearTopSpace
for S being sequence of X
for x being Point of X holds
( ( S is convergent & x = 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) - x).|| < r )