let X be RealNormSpace; :: thesis: for S being sequence of (TopSpaceNorm X)
for St being sequence of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )
let S be sequence of (TopSpaceNorm X); :: thesis: for St being sequence of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )
let St be sequence of (LinearTopSpaceNorm X); :: thesis: for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )
let x be Point of (TopSpaceNorm X); :: thesis: for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )
let xt be Point of (LinearTopSpaceNorm X); :: thesis: ( S = St & x = xt implies ( St is_convergent_to xt iff S is_convergent_to x ) )
assume that
A1: S = St and
A2: x = xt ; :: thesis: ( St is_convergent_to xt iff S is_convergent_to x )

A3: now :: thesis: ( S is_convergent_to x implies St is_convergent_to xt )

assume A4: S is_convergent_to x ; :: thesis: St is_convergent_to xt

now :: thesis: for U1t being Subset of (LinearTopSpaceNorm X) st U1t is open & xt in U1t holds
ex n being Nat st
for m being Nat st n <= m holds
St . m in U1t

let U1t be Subset of (LinearTopSpaceNorm X); :: thesis: ( U1t is open & xt in U1t implies ex n being Nat st
for m being Nat st n <= m holds
St . m in U1t )
assume that
A5: U1t is open and
A6: xt in U1t ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
St . m in U1t
reconsider U1 = U1t as open Subset of (TopSpaceNorm X) by A5, Def4, Th20;
consider n being Nat such that
A7: for m being Nat st n <= m holds
S . m in U1 by A2, A4, A6, FRECHET:def 3;
take n = n; :: thesis: for m being Nat st n <= m holds
St . m in U1t
let m be Nat; :: thesis: ( n <= m implies St . m in U1t )
assume n <= m ; :: thesis: St . m in U1t
hence St . m in U1t by A1, A7; :: thesis: verum

end;

hence St is_convergent_to xt by FRECHET:def 3; :: thesis: verum

end;

now :: thesis: ( St is_convergent_to xt implies S is_convergent_to x )

assume A8: St is_convergent_to xt ; :: thesis: S is_convergent_to x

now :: thesis: for U1 being Subset of (TopSpaceNorm 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 (TopSpaceNorm 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 that
A9: U1 is open and
A10: x in U1 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
S . m in U1
reconsider U1t = U1 as open Subset of (LinearTopSpaceNorm X) by A9, Def4, Th20;
consider n being Nat such that
A11: for m being Nat st n <= m holds
St . m in U1t by A2, A8, A10, FRECHET:def 3;
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 A1, A11; :: thesis: verum

end;

hence S is_convergent_to x by FRECHET:def 3; :: thesis: verum

end;

hence ( St is_convergent_to xt iff S is_convergent_to x ) by A3; :: thesis: verum