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

let S be sequence of (); :: thesis: for St being sequence of st S = St & St is convergent holds
( Lim S = Lim St & lim S = lim St )

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