let X be RealUnitarySpace; :: thesis: for S being sequence of X
for St being sequence of (MetricSpaceNorm (RUSp2RNSp 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 (RUSp2RNSp X)) st S = St holds
( St is convergent iff S is convergent )
let St be sequence of (MetricSpaceNorm (RUSp2RNSp X)); :: thesis: ( S = St implies ( St is convergent iff S is convergent ) )
assume A1: S = St ; :: thesis: ( St is convergent iff S is convergent )

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

assume St is convergent ; :: thesis: S is convergent
then consider xt being Point of (MetricSpaceNorm (RUSp2RNSp 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 BHSP_2:9; :: thesis: verum

end;

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 BHSP_2:9;
reconsider xt = x as Point of (MetricSpaceNorm (RUSp2RNSp X)) ;
St is_convergent_in_metrspace_to xt by A1, A3, Th4;
hence St is convergent ; :: thesis: verum