let X be RealNormSpace; :: thesis: for S being sequence of X
for St being sequence of (LinearTopSpaceNorm X) st S = St & St is convergent holds
( Lim St = {(lim S)} & lim St = lim S )
let S be sequence of X; :: thesis: for St being sequence of (LinearTopSpaceNorm X) st S = St & St is convergent holds
( Lim St = {(lim S)} & lim St = lim S )
let St be sequence of (LinearTopSpaceNorm X); :: thesis: ( S = St & St is convergent implies ( Lim St = {(lim S)} & lim St = lim S ) )
assume that
A1: S = St and
A2: St is convergent ; :: thesis: ( Lim St = {(lim S)} & lim St = lim S )
the carrier of (LinearTopSpaceNorm X) = the carrier of (TopSpaceNorm X) by Def4;
then reconsider SSt = St as sequence of (TopSpaceNorm X) ;
SSt is convergent by A2, Th27;
then ( Lim SSt = {(lim S)} & lim SSt = lim S ) by A1, Th14;
hence ( Lim St = {(lim S)} & lim St = lim S ) by A2, Th28; :: thesis: verum