let X be RealNormSpace; :: thesis: for S being sequence of X

for St being sequence of (LinearTopSpaceNorm X)

for x being Point of X

for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds

( St is_convergent_to xt 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 St being sequence of (LinearTopSpaceNorm X)

for x being Point of X

for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds

( St is_convergent_to xt 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 St be sequence of (LinearTopSpaceNorm X); :: thesis: for x being Point of X

for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds

( St is_convergent_to xt 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: for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds

( St is_convergent_to xt 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 xt be Point of (LinearTopSpaceNorm X); :: thesis: ( S = St & x = xt implies ( St is_convergent_to xt 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 ) )

reconsider xxt = xt as Point of (TopSpaceNorm X) by Def4;

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

the carrier of (LinearTopSpaceNorm X) = the carrier of (TopSpaceNorm X) by Def4;

then reconsider SSt = St as sequence of (TopSpaceNorm X) ;

( St is_convergent_to xt iff SSt is_convergent_to xxt ) by Th26;

hence ( St is_convergent_to xt 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 A1, Th12; :: thesis: verum

for St being sequence of (LinearTopSpaceNorm X)

for x being Point of X

for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds

( St is_convergent_to xt 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 St being sequence of (LinearTopSpaceNorm X)

for x being Point of X

for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds

( St is_convergent_to xt 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 St be sequence of (LinearTopSpaceNorm X); :: thesis: for x being Point of X

for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds

( St is_convergent_to xt 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: for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds

( St is_convergent_to xt 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 xt be Point of (LinearTopSpaceNorm X); :: thesis: ( S = St & x = xt implies ( St is_convergent_to xt 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 ) )

reconsider xxt = xt as Point of (TopSpaceNorm X) by Def4;

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

the carrier of (LinearTopSpaceNorm X) = the carrier of (TopSpaceNorm X) by Def4;

then reconsider SSt = St as sequence of (TopSpaceNorm X) ;

( St is_convergent_to xt iff SSt is_convergent_to xxt ) by Th26;

hence ( St is_convergent_to xt 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 A1, Th12; :: thesis: verum