let M be non empty MetrSpace; :: thesis: for S being sequence of M
for x being Point of M
for S9 being sequence of (TopSpaceMetr M)
for x9 being Point of (TopSpaceMetr M) st S = S9 & x = x9 holds
( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 )
let S be sequence of M; :: thesis: for x being Point of M
for S9 being sequence of (TopSpaceMetr M)
for x9 being Point of (TopSpaceMetr M) st S = S9 & x = x9 holds
( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 )
let x be Point of M; :: thesis: for S9 being sequence of (TopSpaceMetr M)
for x9 being Point of (TopSpaceMetr M) st S = S9 & x = x9 holds
( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 )
let S9 be sequence of (TopSpaceMetr M); :: thesis: for x9 being Point of (TopSpaceMetr M) st S = S9 & x = x9 holds
( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 )
let x9 be Point of (TopSpaceMetr M); :: thesis: ( S = S9 & x = x9 implies ( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 ) )
assume that
A1: S = S9 and
A2: x = x9 ; :: thesis: ( S is_convergent_in_metrspace_to x iff S9 is_convergent_to x9 )
thus ( S is_convergent_in_metrspace_to x implies S9 is_convergent_to x9 ) :: thesis: ( S9 is_convergent_to x9 implies S is_convergent_in_metrspace_to x )

proof

assume A3: S is_convergent_in_metrspace_to x ; :: thesis: S9 is_convergent_to x9
let U1 be Subset of (TopSpaceMetr M); :: according to FRECHET:def 3 :: thesis: ( not U1 is open or not x9 in U1 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or S9 . b₂ in U1 ) )
assume ( U1 is open & x9 in U1 ) ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or S9 . b₂ in U1 )
then consider r being Real such that
A4: r > 0 and
A5: Ball (x,r) c= U1 by A2, TOPMETR:15;
reconsider r = r as Real ;
Ball (x,r) contains_almost_all_sequence S by A3, A4, METRIC_6:15;
then consider n being Nat such that
A6: for m being Nat st n <= m holds
S . m in Ball (x,r) ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis: for b₁ being set holds
( not n <= b₁ or S9 . b₁ in U1 )
let m be Nat; :: thesis: ( not n <= m or S9 . m in U1 )
assume n <= m ; :: thesis: S9 . m in U1
then S . m in Ball (x,r) by A6;
hence S9 . m in U1 by A1, A5; :: thesis: verum

end;

assume A7: S9 is_convergent_to x9 ; :: thesis: S is_convergent_in_metrspace_to x
for V being Subset of M st x in V & V in Family_open_set M holds
V contains_almost_all_sequence S

proof

let V be Subset of M; :: thesis: ( x in V & V in Family_open_set M implies V contains_almost_all_sequence S )
assume that
A8: x in V and
A9: V in Family_open_set M ; :: thesis: V contains_almost_all_sequence S
reconsider V9 = V as Subset of (TopSpaceMetr M) by TOPMETR:12;
reconsider V9 = V9 as Subset of (TopSpaceMetr M) ;
V9 in the topology of (TopSpaceMetr M) by A9, TOPMETR:12;
then V9 is open ;
then consider n being Nat such that
A10: for m being Nat st n <= m holds
S9 . m in V9 by A2, A7, A8;
take n ; :: according to METRIC_6:def 5 :: thesis: for b₁ being set holds
( not n <= b₁ or S . b₁ in V )
let m be Nat; :: thesis: ( not n <= m or S . m in V )
assume n <= m ; :: thesis: S . m in V
hence S . m in V by A1, A10; :: thesis: verum

end;

hence S is_convergent_in_metrspace_to x by METRIC_6:17; :: thesis: verum