let X be RealNormSpace; :: thesis: for S being sequence of (TopSpaceNorm X)
for St being sequence of (LinearTopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
let S be sequence of (TopSpaceNorm 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 )

A2: now :: thesis: ( S is convergent implies St is convergent )

assume S is convergent ; :: thesis: St is convergent
then consider x being Point of (TopSpaceNorm X) such that
A3: S is_convergent_to x by FRECHET:def 4;
reconsider xt = x as Point of (LinearTopSpaceNorm X) by Def4;
St is_convergent_to xt by A1, A3, Th26;
hence St is convergent by FRECHET:def 4; :: thesis: verum

end;

now :: thesis: ( St is convergent implies S is convergent )

assume St is convergent ; :: thesis: S is convergent
then consider xt being Point of (LinearTopSpaceNorm X) such that
A4: St is_convergent_to xt by FRECHET:def 4;
reconsider x = xt as Point of (TopSpaceNorm X) by Def4;
S is_convergent_to x by A1, A4, Th26;
hence S is convergent by FRECHET:def 4; :: thesis: verum

end;

hence ( St is convergent iff S is convergent ) by A2; :: thesis: verum