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 A1: ( S = St & x = xt ) ; :: thesis: ( St is_convergent_to xt iff S is_convergent_to x )

A2: now

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

now

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

end;

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

end;

now

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

now

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

end;

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

end;

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