theorem Th22: :: C0SP3:22

for X being NormedLinearTopSpace
for S being sequence of X st S is convergent holds
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - (lim S)).|| < r