let M be non empty MetrSpace; :: thesis: for S being non empty Subset of M holds
( S is sequentially_compact iff M | S is sequentially_compact )
let S be non empty Subset of M; :: thesis: ( S is sequentially_compact iff M | S is sequentially_compact )
A1: the carrier of (M | S) = S by TOPMETR:def 2;
set X = [#] (M | S);

hereby :: thesis: ( M | S is sequentially_compact implies S is sequentially_compact )

assume A2: S is sequentially_compact ; :: thesis: M | S is sequentially_compact
for S1 being sequence of (M | S) st rng S1 c= [#] (M | S) holds
ex S2 being sequence of (M | S) st
( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in [#] (M | S) )

proof

let S1 be sequence of (M | S); :: thesis: ( rng S1 c= [#] (M | S) implies ex S2 being sequence of (M | S) st
( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in [#] (M | S) ) )
assume rng S1 c= [#] (M | S) ; :: thesis: ex S2 being sequence of (M | S) st
( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in [#] (M | S) )
A3: rng S1 c= S by A1;
rng S1 c= [#] M by A1, XBOOLE_1:1;
then reconsider SS1 = S1 as sequence of M by FUNCT_2:6;
consider SS2 being sequence of M such that
A4: ( ex N being increasing sequence of NAT st SS2 = SS1 * N & SS2 is convergent & lim SS2 in S ) by A2, A3;
consider N being increasing sequence of NAT such that
A5: SS2 = SS1 * N by A4;
rng SS2 c= rng SS1 by A5, RELAT_1:26;
then rng SS2 c= [#] (M | S) by A3, XBOOLE_1:1;
then reconsider S2 = SS2 as sequence of (M | S) by FUNCT_2:6;
take S2 ; :: thesis: ( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in [#] (M | S) )
thus ex N being increasing sequence of NAT st S2 = S1 * N by A5; :: thesis: ( S2 is convergent & lim S2 in [#] (M | S) )
reconsider x = lim SS2 as Element of (M | S) by A4, TOPMETR:def 2;

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

let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
dist ((S2 . m),x) < r )
assume 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
dist ((S2 . m),x) < r
then consider n being Nat such that
A6: for m being Nat st n <= m holds
dist ((SS2 . m),(lim SS2)) < r by A4, TBSP_1:def 3;
take n = n; :: thesis: for m being Nat st n <= m holds
dist ((S2 . m),x) < r
thus for m being Nat st n <= m holds
dist ((S2 . m),x) < r :: thesis: verum

proof

let m be Nat; :: thesis: ( n <= m implies dist ((S2 . m),x) < r )
assume n <= m ; :: thesis: dist ((S2 . m),x) < r
then dist ((SS2 . m),(lim SS2)) < r by A6;
hence dist ((S2 . m),x) < r by TOPMETR:def 1; :: thesis: verum

end;

end;

hence S2 is convergent ; :: thesis: lim S2 in [#] (M | S)
thus lim S2 in [#] (M | S) ; :: thesis: verum

end;

then [#] (M | S) is sequentially_compact ;
hence M | S is sequentially_compact ; :: thesis: verum

end;

assume A7: M | S is sequentially_compact ; :: thesis: S is sequentially_compact
for S1 being sequence of M st rng S1 c= S holds
ex S2 being sequence of M st
( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in S )

proof

let S1 be sequence of M; :: thesis: ( rng S1 c= S implies ex S2 being sequence of M st
( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in S ) )
assume rng S1 c= S ; :: thesis: ex S2 being sequence of M st
( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in S )
then A8: rng S1 c= [#] (M | S) by TOPMETR:def 2;
then reconsider SS1 = S1 as sequence of (M | S) by FUNCT_2:6;
consider SS2 being sequence of (M | S) such that
A9: ( ex N being increasing sequence of NAT st SS2 = SS1 * N & SS2 is convergent & lim SS2 in [#] (M | S) ) by A7, A8, Def1;
consider N being increasing sequence of NAT such that
A10: SS2 = SS1 * N by A9;
rng SS2 c= [#] M by A1, XBOOLE_1:1;
then reconsider S2 = SS2 as sequence of M by FUNCT_2:6;
take S2 ; :: thesis: ( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in S )
thus ex N being increasing sequence of NAT st S2 = S1 * N by A10; :: thesis: ( S2 is convergent & lim S2 in S )
reconsider x = lim SS2 as Element of M by A1, A9;

A11: now :: thesis: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S2 . m),x) < r

let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
dist ((S2 . m),x) < r )
assume 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
dist ((S2 . m),x) < r
then consider n being Nat such that
A12: for m being Nat st n <= m holds
dist ((SS2 . m),(lim SS2)) < r by A9, TBSP_1:def 3;
take n = n; :: thesis: for m being Nat st n <= m holds
dist ((S2 . m),x) < r
thus for m being Nat st n <= m holds
dist ((S2 . m),x) < r :: thesis: verum

proof

let m be Nat; :: thesis: ( n <= m implies dist ((S2 . m),x) < r )
assume n <= m ; :: thesis: dist ((S2 . m),x) < r
then dist ((SS2 . m),(lim SS2)) < r by A12;
hence dist ((S2 . m),x) < r by TOPMETR:def 1; :: thesis: verum

end;

end;

hence S2 is convergent ; :: thesis: lim S2 in S
then lim S2 = x by A11, TBSP_1:def 3;
hence lim S2 in S by A1; :: thesis: verum

end;

hence S is sequentially_compact ; :: thesis: verum