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

for St being sequence of (LinearTopSpaceNorm X) st S = St & St is convergent holds

( Lim S = Lim St & lim S = lim St )

let S be sequence of (TopSpaceNorm X); :: thesis: for St being sequence of (LinearTopSpaceNorm X) st S = St & St is convergent holds

( Lim S = Lim St & lim S = lim St )

let St be sequence of (LinearTopSpaceNorm X); :: thesis: ( S = St & St is convergent implies ( Lim S = Lim St & lim S = lim St ) )

assume that

A1: S = St and

A2: St is convergent ; :: thesis: ( Lim S = Lim St & lim S = lim St )

A3: S is convergent by A1, A2, Th27;

then consider x being Point of (TopSpaceNorm X) such that

A4: S is_convergent_to x by FRECHET:def 4;

reconsider xxt = x as Point of (LinearTopSpaceNorm X) by Def4;

St is_convergent_to xxt by A1, A4, Th26;

then A5: lim St = xxt by FRECHET2:25

.= lim S by A4, FRECHET2:25 ;

reconsider Sn = S as sequence of X ;

consider xt being Point of (LinearTopSpaceNorm X) such that

A6: Lim St = {xt} by A2, FRECHET2:24;

xt in {xt} by TARSKI:def 1;

then St is_convergent_to xt by A6, FRECHET:def 5;

then Lim St = {(lim St)} by A6, FRECHET2:25

.= {(lim Sn)} by A3, A5, Th14

.= Lim S by A3, Th14 ;

hence ( Lim S = Lim St & lim S = lim St ) by A5; :: thesis: verum

for St being sequence of (LinearTopSpaceNorm X) st S = St & St is convergent holds

( Lim S = Lim St & lim S = lim St )

let S be sequence of (TopSpaceNorm X); :: thesis: for St being sequence of (LinearTopSpaceNorm X) st S = St & St is convergent holds

( Lim S = Lim St & lim S = lim St )

let St be sequence of (LinearTopSpaceNorm X); :: thesis: ( S = St & St is convergent implies ( Lim S = Lim St & lim S = lim St ) )

assume that

A1: S = St and

A2: St is convergent ; :: thesis: ( Lim S = Lim St & lim S = lim St )

A3: S is convergent by A1, A2, Th27;

then consider x being Point of (TopSpaceNorm X) such that

A4: S is_convergent_to x by FRECHET:def 4;

reconsider xxt = x as Point of (LinearTopSpaceNorm X) by Def4;

St is_convergent_to xxt by A1, A4, Th26;

then A5: lim St = xxt by FRECHET2:25

.= lim S by A4, FRECHET2:25 ;

reconsider Sn = S as sequence of X ;

consider xt being Point of (LinearTopSpaceNorm X) such that

A6: Lim St = {xt} by A2, FRECHET2:24;

xt in {xt} by TARSKI:def 1;

then St is_convergent_to xt by A6, FRECHET:def 5;

then Lim St = {(lim St)} by A6, FRECHET2:25

.= {(lim Sn)} by A3, A5, Th14

.= Lim S by A3, Th14 ;

hence ( Lim S = Lim St & lim S = lim St ) by A5; :: thesis: verum