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