let X be RealNormSpace; :: thesis: for S being sequence of X
for St being sequence of (TopSpaceNorm 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 (TopSpaceNorm X) st S = St & St is convergent holds
( Lim St = {(lim S)} & lim St = lim S )
let St be sequence of (TopSpaceNorm 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 )
consider x being Point of (TopSpaceNorm X) such that
A3: Lim St = {x} by A2, FRECHET2:24;
reconsider Sm = St as sequence of (MetricSpaceNorm X) ;
A4: Sm is convergent by A2, FRECHET2:29;
then A5: lim St = lim Sm by FRECHET2:30
.= lim S by A1, A4, Th6 ;
x in Lim St by A3, TARSKI:def 1;
then St is_convergent_to x by FRECHET:def 5;
hence Lim St = {(lim S)} by A5, A3, FRECHET2:25; :: thesis: lim St = lim S
thus lim St = lim S by A5; :: thesis: verum