let X be NormedLinearTopSpace; :: thesis: 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 )
let S be sequence of X; :: thesis: 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 )
let x be Point of X; :: thesis: ( ( 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 )

hereby :: thesis: ( ( 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 ) implies ( S is convergent & x = lim S ) )

assume ( S is convergent & lim S = x ) ; :: thesis: 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
then S is_convergent_to x by FRECHET2:25;
hence 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 by Th20; :: thesis: verum

end;

assume 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 ; :: thesis: ( S is convergent & x = lim S )
then S is_convergent_to x by Th20;
hence ( S is convergent & x = lim S ) by FRECHET2:25; :: thesis: verum