let X be RealNormSpace; :: thesis: for S being sequence of X
for St being sequence of (MetricSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
let S be sequence of X; :: thesis: for St being sequence of (MetricSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )
let St be sequence of (MetricSpaceNorm 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 X such that
A3: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r by NORMSP_1:def 6;
reconsider xt = x as Point of (MetricSpaceNorm X) ;
St is_convergent_in_metrspace_to xt by A1, A3, Th4;
hence St is convergent by METRIC_6:9; :: 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 (MetricSpaceNorm X) such that
A4: St is_convergent_in_metrspace_to xt by METRIC_6:10;
reconsider x = xt as Point of X ;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r by A1, A4, Th4;
hence S is convergent by NORMSP_1:def 6; :: thesis: verum

end;

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