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 )

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

end;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

hence
St is_convergent_to xt
by FRECHET:def 3; :: thesis: verumex 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;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

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

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

end;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

hence
S is_convergent_to x
by FRECHET:def 3; :: thesis: verumex 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;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