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 A1: ( S = St & St is convergent ) ; :: thesis: ( Lim S = Lim St & lim S = lim St )
then A2: S is convergent by Th27;
reconsider Sn = S as sequence of X ;
consider x being Point of (TopSpaceNorm X) such that
A3: S is_convergent_to x by A2, FRECHET:def 3;
reconsider xxt = x as Point of (LinearTopSpaceNorm X) by Def4;
St is_convergent_to xxt by A1, A3, Th26;
then A4: lim St = xxt by FRECHET2:28
.= lim S by A3, FRECHET2:28 ;
consider xt being Point of (LinearTopSpaceNorm X) such that
A5: Lim St = {xt} by A1, FRECHET2:27;
xt in {xt} by TARSKI:def 1;
then St is_convergent_to xt by A5, FRECHET:def 4;
then Lim St = {(lim St)} by A5, FRECHET2:28
.= {(lim Sn)} by A2, A4, Th14
.= Lim S by A2, Th14 ;
hence ( Lim S = Lim St & lim S = lim St ) by A4; :: thesis: verum