let X be RealNormSpace; :: thesis: for S being sequence of X
for St being sequence of (MetricSpaceNorm X)
for x being Point of X
for xt being Point of (MetricSpaceNorm X) st S = St & x = xt holds
( St is_convergent_in_metrspace_to xt iff 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 )
let S be sequence of X; :: thesis: for St being sequence of (MetricSpaceNorm X)
for x being Point of X
for xt being Point of (MetricSpaceNorm X) st S = St & x = xt holds
( St is_convergent_in_metrspace_to xt iff 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 )
let St be sequence of (MetricSpaceNorm X); :: thesis: for x being Point of X
for xt being Point of (MetricSpaceNorm X) st S = St & x = xt holds
( St is_convergent_in_metrspace_to xt iff 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 )
let x be Point of X; :: thesis: for xt being Point of (MetricSpaceNorm X) st S = St & x = xt holds
( St is_convergent_in_metrspace_to xt iff 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 )
let xt be Point of (MetricSpaceNorm X); :: thesis: ( S = St & x = xt implies ( St is_convergent_in_metrspace_to xt iff 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 ) )
assume A1: ( S = St & x = xt ) ; :: thesis: ( St is_convergent_in_metrspace_to xt iff 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 )

A2: now :: thesis: ( ( 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 ) implies St is_convergent_in_metrspace_to xt )

assume 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 ; :: thesis: St is_convergent_in_metrspace_to xt

now :: thesis: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st m <= n holds
dist ((St . n),xt) < r

let r be Real; :: thesis: ( r > 0 implies ex m being Nat st
for n being Nat st m <= n holds
dist ((St . n),xt) < r )
assume r > 0 ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
dist ((St . n),xt) < r
then consider m being Nat such that
A4: for n being Nat st m <= n holds
||.((S . n) - x).|| < r by A3;
take m = m; :: thesis: for n being Nat st m <= n holds
dist ((St . n),xt) < r
let n be Nat; :: thesis: ( m <= n implies dist ((St . n),xt) < r )
assume m <= n ; :: thesis: dist ((St . n),xt) < r
then ||.((S . n) - x).|| < r by A4;
hence dist ((St . n),xt) < r by A1, Def1; :: thesis: verum

end;

hence St is_convergent_in_metrspace_to xt by METRIC_6:def 2; :: thesis: verum

end;

now :: thesis: ( St is_convergent_in_metrspace_to xt implies 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 )

assume A5: St is_convergent_in_metrspace_to xt ; :: thesis: 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
let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r
then consider m being Nat such that
A6: for n being Nat st m <= n holds
dist ((St . n),xt) < r by A5, METRIC_6:def 2;
take m = m; :: thesis: for n being Nat st m <= n holds
||.((S . n) - x).|| < r
let n be Nat; :: thesis: ( m <= n implies ||.((S . n) - x).|| < r )
assume m <= n ; :: thesis: ||.((S . n) - x).|| < r
then dist ((St . n),xt) < r by A6;
hence ||.((S . n) - x).|| < r by A1, Def1; :: thesis: verum

end;

hence ( St is_convergent_in_metrspace_to xt iff 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 A2; :: thesis: verum