let X be NormedLinearTopSpace; :: thesis: 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
let S be sequence of X; :: thesis: ( S is convergent implies 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 )
assume S is convergent ; :: thesis: 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
then consider x being Point of X such that
A1: S is_convergent_to x ;
( S is convergent & x = lim S ) by FRECHET2:25, A1;
hence 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 by A1, Th20; :: thesis: verum