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

proof

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

end;

assume A6: S' is_convergent_to x' ; :: 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
A7: x in V and
A8: V in Family_open_set M ; :: thesis: V contains_almost_all_sequence S
reconsider V' = V as Subset of (TopSpaceMetr M) by TOPMETR:16;
reconsider V' = V' as Subset of (TopSpaceMetr M) ;
V' in the topology of (TopSpaceMetr M) by A8, TOPMETR:16;
then V' is open by PRE_TOPC:def 5;
then consider n being Element of NAT such that
A9: for m being Element of NAT st n <= m holds
S' . m in V' by A1, A6, A7, FRECHET:def 2;
take n ; :: according to METRIC_6:def 12 :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or S . b₁ in V )
let m be Element of 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, A9; :: thesis: verum

end;

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