let X be RealNormSpace; :: thesis: for S being sequence of X
for St being sequence of (TopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
let S be sequence of X; :: thesis: for St being sequence of (TopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
let St be sequence of (TopSpaceNorm X); :: thesis: ( S = St implies ( St is convergent iff S is convergent ) )
reconsider Sm = St as sequence of (MetricSpaceNorm X) ;
A1: ( St is convergent iff Sm is convergent ) by FRECHET2:29;
assume S = St ; :: thesis: ( St is convergent iff S is convergent )
hence ( St is convergent iff S is convergent ) by A1, Th5; :: thesis: verum