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

proof

hereby :: thesis: ( T is_convergent_to xt implies S is_convergent_to x )

assume A3: S is_convergent_to x ; :: thesis: T is_convergent_to xt

now :: thesis: for U1 being Subset of (TopSpaceNorm RNS) st U1 is open & xt in U1 holds
ex n being Nat st
for m being Nat st n <= m holds
S . m in U1

let U1 be Subset of (TopSpaceNorm RNS); :: thesis: ( U1 is open & xt in U1 implies ex n being Nat st
for m being Nat st n <= m holds
S . m in U1 )
assume A4: ( U1 is open & xt in U1 ) ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
S . m in U1
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: for m being Nat st n <= m holds
S . m in U1
let m be Nat; :: thesis: ( n <= m implies S . m in U1 )
assume n <= m ; :: thesis: S . m in U1
hence S . m in U1 by A5; :: thesis: verum

end;

hence T is_convergent_to xt ; :: thesis: verum

end;

assume A6: T is_convergent_to xt ; :: thesis: S is_convergent_to x

now :: thesis: for U1 being Subset of X st U1 is open & x in U1 holds
ex n being Nat st
for m being Nat st n <= m holds
S . m in U1

let U1 be Subset of X; :: thesis: ( U1 is open & x in U1 implies ex n being Nat st
for m being Nat st n <= m holds
S . m in U1 )
assume A7: ( U1 is open & x in U1 ) ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
S . m in U1
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: for m being Nat st n <= m holds
S . m in U1
let m be Nat; :: thesis: ( n <= m implies S . m in U1 )
assume n <= m ; :: thesis: S . m in U1
hence S . m in U1 by A8; :: thesis: verum

end;

hence S is_convergent_to x ; :: thesis: verum

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 )

proof

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 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 )

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: 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 r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r
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: for n being Nat st m <= n holds
||.((S . n) - x).|| < r
let n be Nat; :: thesis: ( m <= n implies ||.((S . n) - x).|| < r )
assume m <= n ; :: thesis: ||.((S . n) - x).|| < r
then ||.((N . n) - xn).|| < r by A10;
hence ||.((S . n) - x).|| < r by Th19, A1; :: thesis: verum

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

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: verum