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 A1: ( S = St & St is convergent ) ; :: thesis: ( Lim St = {(lim S)} & lim St = lim S )
reconsider Sm = St as sequence of (MetricSpaceNorm X) ;
A2: Sm is convergent by A1, FRECHET2:32;
then A3: lim St = lim Sm by FRECHET2:33
.= lim S by A1, A2, Th6 ;
consider x being Point of (TopSpaceNorm X) such that
A4: Lim St = {x} by A1, FRECHET2:27;
x in Lim St by A4, TARSKI:def 1;
then St is_convergent_to x by FRECHET:def 4;
hence Lim St = {(lim S)} by A3, A4, FRECHET2:28; :: thesis: lim St = lim S
thus lim St = lim S by A3; :: thesis: verum