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 ) )
assume A1: S = St ; :: thesis: ( St is convergent iff S is convergent )
reconsider Sm = St as sequence of (MetricSpaceNorm X) ;
( St is convergent iff Sm is convergent ) by FRECHET2:32;
hence ( St is convergent iff S is convergent ) by A1, Th5; :: thesis: verum