let X be NormedLinearTopSpace; :: thesis:
let S be sequence of X; :: thesis:
let x be Point of X; :: thesis:
consider RNS being RealNormSpace such that
A1: ( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) ) by Def7;
reconsider N = S as sequence of RNS by A1;
reconsider xn = x as Point of RNS by A1;
reconsider T = S as sequence of (TopSpaceNorm RNS) by A1;
reconsider xt = x as Point of (TopSpaceNorm RNS) by A1;
A2: ( S is_convergent_to x iff T is_convergent_to xt )

let U1 be Subset of (TopSpaceNorm RNS); :: thesis:
assume A4: ( U1 is open & xt in U1 ) ; :: thesis:
reconsider U0 = U1 as Subset of X by A1;
( U0 is open & x in U0 ) by A1, A4;
then consider n being Nat such that
A5: for m being Nat st n <= m holds
S . m in U0 by A3;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
hence S . m in U1 by A5; :: thesis:

end;

end;

let U1 be Subset of X; :: thesis:
assume A7: ( U1 is open & x in U1 ) ; :: thesis:
reconsider U0 = U1 as Subset of (TopSpaceNorm RNS) by A1;
( U0 is open & xt in U0 ) by A1, A7;
then consider n being Nat such that
A8: for m being Nat st n <= m holds
T . m in U0 by A6;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
hence S . m in U1 by A8; :: thesis:

end;

end;

( ( for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((N . n) - xn).|| < r ) 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 )

assume A9: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((N . n) - xn).|| < r ; :: thesis:
let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider m being Nat such that
A10: for n being Nat st m <= n holds
||.((N . n) - xn).|| < r by A9;
take m = m; :: thesis:
let n be Nat; :: thesis:
assume m <= n ; :: thesis:
then ||.((N . n) - xn).|| < r by A10;
hence ||.((S . n) - x).|| < r by Th19, A1; :: thesis:

end;

assume A12: 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:
let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider m being Nat such that
A13: for n being Nat st m <= n holds
||.((S . n) - x).|| < r by A12;
take m ; :: thesis:
let n be Nat; :: thesis:
assume m <= n ; :: thesis:
then ||.((S . n) - x).|| < r by A13;
hence ||.((N . n) - xn).|| < r by Th19, A1; :: thesis:

end;

hence ( 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 ) by A2, NORMSP_2:12; :: thesis: