let X be RealNormSpace; :: thesis: for S being sequence of X

for St being sequence of (LinearTopSpaceNorm X) st S = St holds

( St is convergent iff S is convergent )

let S be sequence of X; :: thesis: for St being sequence of (LinearTopSpaceNorm X) st S = St holds

( St is convergent iff S is convergent )

let St be sequence of (LinearTopSpaceNorm X); :: thesis: ( S = St implies ( St is convergent iff S is convergent ) )

assume A1: S = St ; :: thesis: ( St is convergent iff S is convergent )

the carrier of (LinearTopSpaceNorm X) = the carrier of (TopSpaceNorm X) by Def4;

then reconsider SSt = St as sequence of (TopSpaceNorm X) ;

( St is convergent iff SSt is convergent ) by Th27;

hence ( St is convergent iff S is convergent ) by A1, Th13; :: thesis: verum

for St being sequence of (LinearTopSpaceNorm X) st S = St holds

( St is convergent iff S is convergent )

let S be sequence of X; :: thesis: for St being sequence of (LinearTopSpaceNorm X) st S = St holds

( St is convergent iff S is convergent )

let St be sequence of (LinearTopSpaceNorm X); :: thesis: ( S = St implies ( St is convergent iff S is convergent ) )

assume A1: S = St ; :: thesis: ( St is convergent iff S is convergent )

the carrier of (LinearTopSpaceNorm X) = the carrier of (TopSpaceNorm X) by Def4;

then reconsider SSt = St as sequence of (TopSpaceNorm X) ;

( St is convergent iff SSt is convergent ) by Th27;

hence ( St is convergent iff S is convergent ) by A1, Th13; :: thesis: verum