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

for St being sequence of (MetricSpaceNorm X) st S = St & St is convergent holds

lim St = lim S

let S be sequence of X; :: thesis: for St being sequence of (MetricSpaceNorm X) st S = St & St is convergent holds

lim St = lim S

let St be sequence of (MetricSpaceNorm X); :: thesis: ( S = St & St is convergent implies lim St = lim S )

assume that

A1: S = St and

A2: St is convergent ; :: thesis: lim St = lim S

reconsider xt = lim S as Point of (MetricSpaceNorm X) ;

S is convergent by A1, A2, Th5;

then for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - (lim S)).|| < r by NORMSP_1:def 7;

then St is_convergent_in_metrspace_to xt by A1, Th4;

hence lim St = lim S by METRIC_6:11; :: thesis: verum

for St being sequence of (MetricSpaceNorm X) st S = St & St is convergent holds

lim St = lim S

let S be sequence of X; :: thesis: for St being sequence of (MetricSpaceNorm X) st S = St & St is convergent holds

lim St = lim S

let St be sequence of (MetricSpaceNorm X); :: thesis: ( S = St & St is convergent implies lim St = lim S )

assume that

A1: S = St and

A2: St is convergent ; :: thesis: lim St = lim S

reconsider xt = lim S as Point of (MetricSpaceNorm X) ;

S is convergent by A1, A2, Th5;

then for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - (lim S)).|| < r by NORMSP_1:def 7;

then St is_convergent_in_metrspace_to xt by A1, Th4;

hence lim St = lim S by METRIC_6:11; :: thesis: verum