let X be RealNormSpace; :: thesis: for S being sequence of X
for St being sequence of (TopSpaceNorm X)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_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 (TopSpaceNorm X)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_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 (TopSpaceNorm X); :: thesis: for x being Point of X
for xt being Point of (TopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_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 (TopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_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 (TopSpaceNorm X); :: thesis: ( S = St & x = xt implies ( St is_convergent_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 that
A1: S = St and
A2: x = xt ; :: thesis: ( St is_convergent_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 )
reconsider Sm = St as sequence of (MetricSpaceNorm X) ;
reconsider xm = x as Point of (MetricSpaceNorm X) ;
( St is_convergent_to xt iff Sm is_convergent_in_metrspace_to xm ) by A2, FRECHET2:28;
hence ( St is_convergent_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 A1, Th4; :: thesis: verum