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

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