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