topmetr4.miz



    begin

    theorem :: TOPMETR4:1

    

     LM1: for M be non empty set, x be sequence of M st ( rng x) is finite holds ex z be Element of M st (x " {z}) c= NAT & (x " {z}) is infinite

    proof

      let M be non empty set, x be sequence of M;

      assume

       A1: ( rng x) is finite;

      assume

       A2: not (ex z be Element of M st (x " {z}) c= NAT & (x " {z}) is infinite);

      deffunc X( object) = (x " {$1});

      set K = { X(w) where w be Element of M : w in ( rng x) };

      

       A3: K is finite from FRAENKEL:sch 21( A1);

      for Y be set st Y in K holds Y is finite

      proof

        let Y be set;

        assume Y in K;

        then

        consider w be Element of M such that

         A4: Y = (x " {w}) & w in ( rng x);

        thus Y is finite by A2, A4;

      end;

      then

       A5: ( union K) is finite by A3, FINSET_1: 7;

      ( dom x) c= ( union K)

      proof

        let s be object;

        assume

         A6: s in ( dom x);

        then

        reconsider sn = s as Element of NAT ;

        reconsider w = (x . sn) as Element of M;

        w in ( rng x) by A6, FUNCT_1: 3;

        then

         A7: (x " {w}) in K;

        w in {w} by TARSKI:def 1;

        then s in (x " {w}) by A6, FUNCT_1:def 7;

        hence s in ( union K) by A7, TARSKI:def 4;

      end;

      hence contradiction by A5, FUNCT_2:def 1;

    end;

    theorem :: TOPMETR4:2

    

     LM2: for X be Subset of NAT st X is infinite holds ex N be increasing sequence of NAT st ( rng N) c= X

    proof

      let X be Subset of NAT ;

      assume

       A1: X is infinite;

      reconsider BX = ( bool X) as non empty set by ZFMISC_1:def 1;

      reconsider N0 = ( min* X) as Element of NAT ;

      reconsider Y0 = X as Element of BX by ZFMISC_1:def 1;

      defpred P[ object, object, set, object, set] means $5 = ($3 \ {$2}) & $4 = ( min* $5);

      

       A2: for n be Nat, x be Element of NAT , y be Element of BX holds ex x1 be Element of NAT , y1 be Element of BX st P[n, x, y, x1, y1]

      proof

        let n be Nat, x be Element of NAT , y be Element of BX;

        reconsider y1 = (y \ {x}) as Element of BX by XBOOLE_1: 1;

        set x1 = ( min* y1);

        take x1, y1;

        thus thesis;

      end;

      consider N be sequence of NAT , Y be sequence of BX such that

       A3: (N . 0 ) = N0 & (Y . 0 ) = Y0 & for n be Nat holds P[n, (N . n), (Y . n), (N . (n + 1)), (Y . (n + 1))] from RECDEF_2:sch 3( A2);

      defpred Q[ Nat] means (N . $1) = ( min* (Y . $1)) & (N . $1) in (Y . $1) & (Y . $1) is infinite & (Y . $1) c= NAT ;

      

       A4: Q[ 0 ] by A1, A3, NAT_1:def 1;

      

       A5: for i be Nat st Q[i] holds Q[(i + 1)]

      proof

        let i be Nat;

        assume

         A6: Q[i];

        

         A7: (Y . (i + 1)) = ((Y . i) \ {(N . i)}) & (N . (i + 1)) = ( min* (Y . (i + 1))) by A3;

        

         A8: (Y . (i + 1)) is infinite

        proof

          assume (Y . (i + 1)) is finite;

          then ((Y . (i + 1)) \/ {(N . i)}) is finite;

          hence contradiction by A6, A7, XBOOLE_1: 45, ZFMISC_1: 31;

        end;

        (Y . (i + 1)) c= NAT by XBOOLE_1: 1;

        hence thesis by A7, A8, NAT_1:def 1;

      end;

      

       A9: for i be Nat holds Q[i] from NAT_1:sch 2( A4, A5);

      

       A11: ( rng N) c= X

      proof

        let y be object;

        assume y in ( rng N);

        then

        consider i be object such that

         A10: i in NAT & (N . i) = y by FUNCT_2: 11;

        reconsider i as Nat by A10;

        (N . i) = ( min* (Y . i)) & (N . i) in (Y . i) & (Y . i) is infinite & (Y . i) c= NAT by A9;

        hence y in X by A10;

      end;

      for i be Nat holds (N . i) < (N . (i + 1))

      proof

        let i be Nat;

        

         A12: (N . i) = ( min* (Y . i)) & (N . i) in (Y . i) & (Y . i) is infinite & (Y . i) c= NAT by A9;

        (Y . (i + 1)) = ((Y . i) \ {(N . i)}) & (N . (i + 1)) = ( min* (Y . (i + 1))) by A3;

        then

         A13: (N . (i + 1)) in ((Y . i) \ {(N . i)}) by A9;

        then (N . (i + 1)) in (Y . i) & not (N . (i + 1)) in {(N . i)} by XBOOLE_0:def 5;

        then

         A14: (N . (i + 1)) <> (N . i) by TARSKI:def 1;

        (N . i) <= (N . (i + 1)) by A12, A13, NAT_1:def 1;

        hence (N . i) < (N . (i + 1)) by A14, XXREAL_0: 1;

      end;

      then N is increasing;

      hence thesis by A11;

    end;

    theorem :: TOPMETR4:3

    for M be non empty MetrSpace, V be Subset of ( TopSpaceMetr M) st V is open holds ex F be Subset-Family of M st F = { ( Ball (x,r)) where x be Element of M, r be Real : r > 0 & ( Ball (x,r)) c= V } & V = ( union F)

    proof

      let M be non empty MetrSpace, V be Subset of ( TopSpaceMetr M);

      assume

       A1: V is open;

      set F = { ( Ball (x,r)) where x be Element of M, r be Real : r > 0 & ( Ball (x,r)) c= V };

      for z be object st z in F holds z in ( Family_open_set M)

      proof

        let z be object;

        assume z in F;

        then ex x be Element of M, r be Real st z = ( Ball (x,r)) & r > 0 & ( Ball (x,r)) c= V;

        hence z in ( Family_open_set M) by PCOMPS_1: 29;

      end;

      then F c= ( Family_open_set M) by TARSKI:def 3;

      then

      reconsider F as Subset-Family of M by XBOOLE_1: 1;

      take F;

      thus F = { ( Ball (x,r)) where x be Element of M, r be Real : r > 0 & ( Ball (x,r)) c= V };

      reconsider Q = ( union F) as Subset of ( TopSpaceMetr M);

      for z be object holds z in V iff z in Q

      proof

        let z be object;

        hereby

          assume

           A2: z in V;

          then

          reconsider x = z as Element of M;

          consider r be Real such that

           A3: r > 0 & ( Ball (x,r)) c= V by A1, A2, TOPMETR: 15;

          ( dist (x,x)) = 0 by METRIC_1: 1;

          then

           A4: x in ( Ball (x,r)) by A3, METRIC_1: 11;

          ( Ball (x,r)) in F by A3;

          hence z in Q by A4, TARSKI:def 4;

        end;

        assume z in Q;

        then

        consider B be set such that

         A5: z in B & B in F by TARSKI:def 4;

        consider x be Element of M, r be Real such that

         A6: B = ( Ball (x,r)) & r > 0 & ( Ball (x,r)) c= V by A5;

        thus z in V by A5, A6;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TOPMETR4:4

    for M be non empty MetrSpace, X be Subset of ( TopSpaceMetr M), p be Element of M holds (p in ( Cl X) iff for r be Real st 0 < r holds X meets ( Ball (p,r)))

    proof

      let M be non empty MetrSpace, X be Subset of ( TopSpaceMetr M), p be Element of M;

      hereby

        assume

         A1: p in ( Cl X);

        let r be Real;

        assume

         A2: 0 < r;

        reconsider G = ( Ball (p,r)) as Subset of ( TopSpaceMetr M);

        ( dist (p,p)) = 0 by METRIC_1: 1;

        then G is open & p in G by A2, METRIC_1: 11, TOPMETR: 14;

        hence X meets ( Ball (p,r)) by A1, PRE_TOPC:def 7;

      end;

      assume

       A3: for r be Real st 0 < r holds X meets ( Ball (p,r));

      now

        let G be Subset of ( TopSpaceMetr M);

        assume G is open & p in G;

        then

        consider r be Real such that

         A4: 0 < r & ( Ball (p,r)) c= G by PCOMPS_1:def 4;

        X meets ( Ball (p,r)) by A3, A4;

        hence X meets G by A4, XBOOLE_1: 63;

      end;

      hence p in ( Cl X) by PRE_TOPC:def 7;

    end;

    theorem :: TOPMETR4:5

    

     Th3: for M be non empty MetrSpace, X be Subset of ( TopSpaceMetr M) holds for x be object holds x in ( Cl X) iff ex S be sequence of M st (for n be Nat holds (S . n) in X) & S is convergent & ( lim S) = x

    proof

      let M be non empty MetrSpace, X be Subset of ( TopSpaceMetr M);

      let x be object;

      hereby

        assume

         A1: x in ( Cl X);

        reconsider x0 = x as Element of M by A1;

        defpred P[ Element of NAT , object] means $2 in X & $2 in ( Ball (x0,(1 / ($1 + 1))));

        

         A2: for n be Element of NAT holds ex p be Element of M st P[n, p]

        proof

          let n be Element of NAT ;

          set r = (1 / (n + 1));

          reconsider G = ( Ball (x0,r)) as Subset of ( TopSpaceMetr M);

          ( dist (x0,x0)) = 0 by METRIC_1: 1;

          then G is open & x0 in G by METRIC_1: 11, TOPMETR: 14;

          then X meets ( Ball (x0,r)) by A1, PRE_TOPC:def 7;

          then

          consider p be object such that

           A3: p in (X /\ ( Ball (x0,r))) by XBOOLE_0:def 1;

          reconsider p as Element of M by A3;

          take p;

          thus thesis by A3, XBOOLE_0:def 4;

        end;

        consider S be sequence of M such that

         A4: for n be Element of NAT holds P[n, (S . n)] from FUNCT_2:sch 3( A2);

         A5:

        now

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          then (S . n) in X & (S . n) in ( Ball (x0,(1 / (n + 1)))) by A4;

          hence (S . n) in X & ( dist ((S . n),x0)) < (1 / (n + 1)) by METRIC_1: 11;

        end;

         A6:

        now

          let s be Real;

          assume

           A7: 0 < s;

          consider n be Nat such that

           A8: (s " ) < n by SEQ_4: 3;

          take k = n;

          let m be Nat;

          assume k <= m;

          then (k + 1) <= (m + 1) by XREAL_1: 6;

          then

           A9: (1 / (m + 1)) <= (1 / (k + 1)) by XREAL_1: 118;

          ((s " ) + 0 ) < (n + 1) by A8, XREAL_1: 8;

          then (1 / (n + 1)) < (1 / (s " )) by A7, XREAL_1: 76;

          then (1 / (m + 1)) < s by A9, XXREAL_0: 2;

          hence ( dist ((S . m),x0)) < s by A5, XXREAL_0: 2;

        end;

        then

         A10: S is convergent;

        then ( lim S) = x by A6, TBSP_1:def 3;

        hence ex S be sequence of M st (for n be Nat holds (S . n) in X) & S is convergent & ( lim S) = x by A5, A10;

      end;

      given S be sequence of M such that

       A11: for n be Nat holds (S . n) in X and

       A12: S is convergent and

       A13: ( lim S) = x;

      X c= ( Cl X) by PRE_TOPC: 18;

      then

       A14: for n be Nat holds (S . n) in ( Cl X) by A11, TARSKI:def 3;

      ( Cl ( Cl X)) = ( Cl X);

      hence x in ( Cl X) by A12, A13, A14, PRE_TOPC: 22, TOPMETR3: 1;

    end;

    theorem :: TOPMETR4:6

    

     Th4: for M be non empty MetrSpace, X be Subset of ( TopSpaceMetr M) holds X is closed iff for S be sequence of M st (for n be Nat holds (S . n) in X) & S is convergent holds ( lim S) in X

    proof

      let M be non empty MetrSpace, X be Subset of ( TopSpaceMetr M);

      thus X is closed implies for S be sequence of M st (for n be Nat holds (S . n) in X) & S is convergent holds ( lim S) in X by TOPMETR3: 1;

      assume

       A1: for S be sequence of M st (for n be Nat holds (S . n) in X) & S is convergent holds ( lim S) in X;

      for x be object st x in ( Cl X) holds x in X

      proof

        let x be object;

        assume x in ( Cl X);

        then

        consider S be sequence of M such that

         A2: (for n be Nat holds (S . n) in X) & S is convergent & ( lim S) = x by Th3;

        thus x in X by A1, A2;

      end;

      then ( Cl X) = X by PRE_TOPC: 18, TARSKI:def 3;

      hence X is closed by PRE_TOPC: 22;

    end;

    theorem :: TOPMETR4:7

    for X,Y be non empty MetrSpace holds for f be Function of ( TopSpaceMetr X), ( TopSpaceMetr Y) holds f is continuous iff for S be sequence of X, T be sequence of Y st S is convergent & T = (f * S) holds T is convergent & ( lim T) = (f . ( lim S))

    proof

      let X,Y be non empty MetrSpace;

      let f be Function of ( TopSpaceMetr X), ( TopSpaceMetr Y);

      hereby

        assume

         A1: f is continuous;

        let S be sequence of X, T be sequence of Y;

        assume that

         A2: S is convergent and

         A3: T = (f * S);

        set z0 = ( lim S);

        reconsider p = z0 as Point of ( TopSpaceMetr X);

        

         A4: ( dom f) = the carrier of X by FUNCT_2:def 1;

        then (f . ( lim S)) in ( rng f) by FUNCT_1: 3;

        then

        reconsider x0 = (f . ( lim S)) as Element of Y;

        

         A5: for r be Real st r > 0 holds ex n be Nat st for m be Nat st n <= m holds ( dist ((T . m),x0)) < r

        proof

          let r be Real;

          reconsider V = ( Ball (x0,r)) as Subset of ( TopSpaceMetr Y);

          assume r > 0 ;

          then V is open & x0 in V by GOBOARD6: 1, TOPMETR: 14;

          then

          consider W be Subset of ( TopSpaceMetr X) such that

           A6: p in W & W is open and

           A7: (f .: W) c= V by A1, JGRAPH_2: 10;

          consider r0 be Real such that

           A8: r0 > 0 and

           A9: ( Ball (z0,r0)) c= W by A6, TOPMETR: 15;

          reconsider r00 = r0 as Real;

          consider n0 be Nat such that

           A10: for m be Nat st n0 <= m holds ( dist ((S . m),z0)) < r00 by A2, A8, TBSP_1:def 3;

          for m be Nat st n0 <= m holds ( dist ((T . m),x0)) < r

          proof

            let m be Nat;

            assume n0 <= m;

            then ( dist ((S . m),z0)) < r0 by A10;

            then (S . m) in ( Ball (z0,r0)) by METRIC_1: 11;

            then

             A11: (f . (S . m)) in (f .: W) by A4, A9, FUNCT_1:def 6;

            ( dom T) = NAT by FUNCT_2:def 1;

            then (T . m) in (f .: W) by A3, A11, FUNCT_1: 12, ORDINAL1:def 12;

            hence thesis by A7, METRIC_1: 11;

          end;

          hence thesis;

        end;

        hence T is convergent;

        hence ( lim T) = (f . ( lim S)) by A5, TBSP_1:def 3;

      end;

      assume

       A12: for S be sequence of X, T be sequence of Y st S is convergent & T = (f * S) holds T is convergent & ( lim T) = (f . ( lim S));

      for B be Subset of ( TopSpaceMetr Y) st B is closed holds (f " B) is closed

      proof

        let B be Subset of ( TopSpaceMetr Y);

        reconsider A = (f " B) as Subset of ( TopSpaceMetr X);

        assume

         A13: B is closed;

        for S be sequence of X st (for n be Nat holds (S . n) in (f " B)) & S is convergent holds ( lim S) in (f " B)

        proof

          let S be sequence of X;

          assume that

           A14: for n be Nat holds (S . n) in (f " B) and

           A15: S is convergent;

          reconsider T = (f * S) as sequence of Y;

          for n be Nat holds (T . n) in B

          proof

            let n be Nat;

            (S . n) in (f " B) by A14;

            then (f . (S . n)) in B by FUNCT_1:def 7;

            hence (T . n) in B by FUNCT_2: 15, ORDINAL1:def 12;

          end;

          then ( lim T) in B by A12, A13, A15, Th4;

          then

           A16: (f . ( lim S)) in B by A12, A15;

          ( dom f) = the carrier of X by FUNCT_2:def 1;

          hence ( lim S) in (f " B) by A16, FUNCT_1:def 7;

        end;

        hence (f " B) is closed by Th4;

      end;

      hence f is continuous;

    end;

    begin

    definition

      let M be non empty MetrSpace;

      let X be Subset of M;

      :: TOPMETR4:def1

      attr X is sequentially_compact means

      : Def1: for S1 be sequence of M st ( rng S1) c= X holds ex S2 be sequence of M st (ex N be increasing sequence of NAT st S2 = (S1 * N)) & S2 is convergent & ( lim S2) in X;

    end

    

     Th6: for M be non empty MetrSpace, X be Subset of M st X = {} holds X is sequentially_compact

    proof

      let M be non empty MetrSpace;

      let X be Subset of M;

      assume

       A1: X = {} ;

      let S1 be sequence of M;

      assume

       A2: ( rng S1) c= X;

      (S1 . 0 ) in ( rng S1) by FUNCT_2: 4;

      hence ex S2 be sequence of M st (ex N be increasing sequence of NAT st S2 = (S1 * N)) & S2 is convergent & ( lim S2) in X by A1, A2;

    end;

    registration

      let M be non empty MetrSpace;

      cluster empty -> sequentially_compact for Subset of M;

      coherence by Th6;

    end

    definition

      let M be non empty MetrSpace;

      :: TOPMETR4:def2

      attr M is sequentially_compact means ( [#] M) is sequentially_compact;

    end

    theorem :: TOPMETR4:8

    

     Th7: for M be non empty MetrSpace, X be Subset of M, Y be Subset of ( TopSpaceMetr M), x be Element of M, y be Element of ( TopSpaceMetr M) st X = Y & x = y holds y is_an_accumulation_point_of Y iff for r be Real st 0 < r holds ( Ball (x,r)) meets (X \ {x})

    proof

      let M be non empty MetrSpace, X be Subset of M, Y be Subset of ( TopSpaceMetr M), x be Element of M, y be Element of ( TopSpaceMetr M);

      assume

       A1: X = Y & x = y;

      hereby

        assume y is_an_accumulation_point_of Y;

        then

         A2: y in ( Der Y) by TOPGEN_1: 16;

        let r be Real;

        assume

         A3: 0 < r;

        reconsider U = ( Ball (x,r)) as Subset of ( TopSpaceMetr M);

        

         A4: U is open by TOPMETR: 14;

        ( dist (x,x)) = 0 by METRIC_1: 1;

        then

        consider z be Point of ( TopSpaceMetr M) such that

         A5: z in (Y /\ U) & y <> z by A1, A2, A3, A4, METRIC_1: 11, TOPGEN_1: 17;

        z in Y & z in U & not z in {y} by A5, TARSKI:def 1, XBOOLE_0:def 4;

        then z in (Y \ {y}) & z in U by XBOOLE_0:def 5;

        hence ( Ball (x,r)) meets (X \ {x}) by A1, XBOOLE_0:def 4;

      end;

      assume

       A6: for r be Real st 0 < r holds ( Ball (x,r)) meets (X \ {x});

      for U be open Subset of ( TopSpaceMetr M) st y in U holds ex z be Point of ( TopSpaceMetr M) st z in (Y /\ U) & y <> z

      proof

        let U be open Subset of ( TopSpaceMetr M);

        assume

         A7: y in U;

        U is open;

        then

        consider r be Real such that

         A8: 0 < r & ( Ball (x,r)) c= U by A1, A7, PCOMPS_1:def 4;

        ( Ball (x,r)) meets (X \ {x}) by A6, A8;

        then

        consider z be object such that

         A9: z in (( Ball (x,r)) /\ (X \ {x})) by XBOOLE_0:def 1;

        z in ( Ball (x,r)) & z in (X \ {x}) by A9, XBOOLE_0:def 4;

        then

         A10: z in U & z in Y & not z in {x} by A1, A8, XBOOLE_0:def 5;

        reconsider z as Point of ( TopSpaceMetr M) by A9;

        take z;

        thus z in (Y /\ U) & y <> z by A1, A10, TARSKI:def 1, XBOOLE_0:def 4;

      end;

      then y in ( Der Y) by TOPGEN_1: 17;

      hence y is_an_accumulation_point_of Y by TOPGEN_1: 16;

    end;

    

     LM3: for M be non empty MetrSpace, X be Subset of M, x be Element of M st (for r be Real st 0 < r holds ( Ball (x,r)) meets (X \ {x})) holds for r be Real st 0 < r holds (( Ball (x,r)) /\ (X \ {x})) is infinite

    proof

      let M be non empty MetrSpace, X be Subset of M, x be Element of M;

      assume

       A1: for r be Real st 0 < r holds ( Ball (x,r)) meets (X \ {x});

      assume not (for r be Real st 0 < r holds (( Ball (x,r)) /\ (X \ {x})) is infinite);

      then

      consider r be Real such that

       A2: 0 < r & (( Ball (x,r)) /\ (X \ {x})) is finite;

      

       A3: (( Ball (x,r)) /\ (X \ {x})) is finite by A2;

      

       A4: ( Ball (x,r)) meets (X \ {x}) by A1, A2;

      deffunc F( Point of M) = ( dist (x,$1));

      set D = { F(y) where y be Element of the carrier of M : y in (( Ball (x,r)) /\ (X \ {x})) };

      

       A5: D is finite from FRAENKEL:sch 21( A3);

      

       A7: D c= REAL

      proof

        let z be object;

        assume z in D;

        then

        consider y be Point of M such that

         A6: z = ( dist (x,y)) & y in (( Ball (x,r)) /\ (X \ {x}));

        thus z in REAL by A6, XREAL_0:def 1;

      end;

      consider w be object such that

       A8: w in (( Ball (x,r)) /\ (X \ {x})) by A4, XBOOLE_0:def 1;

      reconsider w as Point of M by A8;

      ( dist (x,w)) in D by A8;

      then

      reconsider D as non empty real-membered set by A7;

      reconsider D as left_end real-membered set by A5;

      set r0 = ( min D);

      

       A9: r0 in D & for s be Real st s in D holds r0 <= s by XXREAL_2:def 7;

      consider y be Point of M such that

       A10: r0 = ( dist (x,y)) & y in (( Ball (x,r)) /\ (X \ {x})) by A9;

      

       A11: y in ( Ball (x,r)) by A10, XBOOLE_0:def 4;

      y in (X \ {x}) by A10, XBOOLE_0:def 4;

      then not y in {x} by XBOOLE_0:def 5;

      then

       A12: y <> x by TARSKI:def 1;

      then 0 < r0 by A10, METRIC_1: 7;

      then ( Ball (x,(r0 / 2))) meets (X \ {x}) by A1;

      then

      consider z be object such that

       A13: z in (( Ball (x,(r0 / 2))) /\ (X \ {x})) by XBOOLE_0:def 1;

      

       A14: z in ( Ball (x,(r0 / 2))) & z in (X \ {x}) by A13, XBOOLE_0:def 4;

      reconsider z as Point of M by A13;

      (r0 / 2) < r0 by A10, A12, METRIC_1: 7, XREAL_1: 216;

      then

       A15: ( dist (x,z)) < r0 by A14, METRIC_1: 11, XXREAL_0: 2;

      then ( dist (x,z)) < r by A10, A11, METRIC_1: 11, XXREAL_0: 2;

      then z in ( Ball (x,r)) by METRIC_1: 11;

      then z in (( Ball (x,r)) /\ (X \ {x})) by A14, XBOOLE_0:def 4;

      then ( dist (x,z)) in D;

      hence thesis by A15, XXREAL_2:def 7;

    end;

    theorem :: TOPMETR4:9

    

     Th8: for M be non empty MetrSpace st ( TopSpaceMetr M) is countably_compact holds M is sequentially_compact

    proof

      let M be non empty MetrSpace;

      assume

       A1: ( TopSpaceMetr M) is countably_compact;

      

       A2: ( TopSpaceMetr M) is T_2 by PCOMPS_1: 34;

      

       A3: for X be Subset of M st X is infinite holds ex x be Element of M st for r be Real st 0 < r holds ( Ball (x,r)) meets (X \ {x})

      proof

        let X be Subset of M;

        assume

         A4: X is infinite;

        reconsider A = X as Subset of ( TopSpaceMetr M);

        ( Der A) is non empty by A1, A2, A4, COMPL_SP: 28;

        then

        consider z be object such that

         A5: z in ( Der A);

        

         A6: z is_an_accumulation_point_of A by A5, TOPGEN_1: 16;

        reconsider z as Point of ( TopSpaceMetr M) by A5;

        reconsider x = z as Element of M;

        take x;

        thus for r be Real st 0 < r holds ( Ball (x,r)) meets (X \ {x}) by A6, Th7;

      end;

      for x be sequence of M st ( rng x) c= ( [#] M) holds ex xN be sequence of M st (ex N be increasing sequence of NAT st xN = (x * N)) & xN is convergent & ( lim xN) in ( [#] M)

      proof

        let x be sequence of M such that ( rng x) c= ( [#] M);

        per cases ;

          suppose ( rng x) is finite;

          then

          consider z be Element of the carrier of M such that

           A7: (x " {z}) c= NAT & (x " {z}) is infinite by LM1;

          consider N be increasing sequence of NAT such that

           A8: ( rng N) c= (x " {z}) by A7, LM2;

          set xN = (x * N);

          take xN;

          

           A9: for n be Nat holds (xN . n) = z

          proof

            let n be Nat;

            (N . n) in ( rng N) by FUNCT_2: 4, ORDINAL1:def 12;

            then (x . (N . n)) in {z} by A8, FUNCT_2: 38;

            then (x . (N . n)) = z by TARSKI:def 1;

            hence (xN . n) = z by FUNCT_2: 15, ORDINAL1:def 12;

          end;

          now

            let r be Real;

            assume

             A10: 0 < r;

            reconsider n = 0 as Nat;

            take n;

            thus for m be Nat st n <= m holds ( dist ((xN . m),z)) < r

            proof

              let m be Nat;

              assume n <= m;

              ( dist ((xN . m),z)) = ( dist (z,z)) by A9

              .= 0 by METRIC_1: 1;

              hence ( dist ((xN . m),z)) < r by A10;

            end;

          end;

          hence thesis;

        end;

          suppose ( rng x) is infinite;

          then

          consider z be Element of M such that

           A12: for r be Real st 0 < r holds ( Ball (z,r)) meets (( rng x) \ {z}) by A3;

          ( Ball (z,1)) meets (( rng x) \ {z}) by A12;

          then

          consider w be object such that

           A13: w in (( Ball (z,1)) /\ (( rng x) \ {z})) by XBOOLE_0:def 1;

          reconsider w as Point of M by A13;

          w in (( rng x) \ {z}) by A13, XBOOLE_0:def 4;

          then w in ( rng x) by XBOOLE_0:def 5;

          then

          consider N0 be Element of NAT such that

           A14: w = (x . N0) by FUNCT_2: 113;

          defpred P[ Nat, Nat, Nat] means $2 < $3 & (x . $3) in ( Ball (z,(1 / (2 + $1))));

          

           A15: for n be Nat holds for ix be Element of NAT holds ex iy be Element of NAT st P[n, ix, iy]

          proof

            let n be Nat, ix be Element of NAT ;

            assume

             A16: not ex iy be Element of NAT st P[n, ix, iy];

            

             A17: (( Ball (z,(1 / (2 + n)))) /\ (( rng x) \ {z})) c= ( Ball (z,(1 / (2 + n)))) by XBOOLE_1: 17;

            for g be object st g in (( Ball (z,(1 / (2 + n)))) /\ (( rng x) \ {z})) holds g in (x .: ( Segm (ix + 1)))

            proof

              let g be object;

              assume

               A18: g in (( Ball (z,(1 / (2 + n)))) /\ (( rng x) \ {z}));

              then g in ( Ball (z,(1 / (2 + n)))) & g in (( rng x) \ {z}) by XBOOLE_0:def 4;

              then g in ( rng x) by XBOOLE_0:def 5;

              then

              consider iy be Element of NAT such that

               A19: g = (x . iy) by FUNCT_2: 113;

              iy <= ix by A16, A17, A18, A19;

              then iy < (ix + 1) by NAT_1: 13;

              then iy in ( Segm (ix + 1)) by NAT_1: 44;

              hence g in (x .: ( Segm (ix + 1))) by A19, FUNCT_2: 35;

            end;

            then (( Ball (z,(1 / (2 + n)))) /\ (( rng x) \ {z})) c= (x .: ( Segm (ix + 1))) by TARSKI:def 3;

            hence contradiction by A12, LM3;

          end;

          consider N be sequence of NAT such that

           A20: (N . 0 ) = N0 & for n be Nat holds P[n, (N . n), (N . (n + 1))] from RECDEF_1:sch 2( A15);

          N is increasing by A20;

          then

          reconsider N as increasing sequence of NAT ;

          defpred Q[ Nat] means (x . (N . $1)) in ( Ball (z,(1 / (1 + $1))));

          

           A21: Q[ 0 ] by A13, A14, A20, XBOOLE_0:def 4;

          

           A22: for k be Nat st Q[k] holds Q[(k + 1)]

          proof

            let k be Nat;

            assume Q[k];

            (N . k) < (N . (k + 1)) & (x . (N . (k + 1))) in ( Ball (z,(1 / (2 + k)))) by A20;

            hence thesis;

          end;

          

           A23: for i be Nat holds Q[i] from NAT_1:sch 2( A21, A22);

          now

            let r be Real;

            assume

             A24: 0 < r;

            consider n be Nat such that

             A25: (r " ) < n by SEQ_4: 3;

            

             A26: (1 / n) < (1 / (r " )) by A24, A25, XREAL_1: 76;

            

             A27: 0 < n by A24, A25;

            take n;

            thus for m be Nat st n <= m holds ( dist (((x * N) . m),z)) < r

            proof

              let m be Nat;

              assume n <= m;

              then (n + 0 ) < (m + 1) by XREAL_1: 8;

              then

               A28: (1 / (1 + m)) <= (1 / n) by A27, XREAL_1: 118;

              (x . (N . m)) in ( Ball (z,(1 / (1 + m)))) by A23;

              then

               A29: ( dist ((x . (N . m)),z)) < (1 / n) by A28, METRIC_1: 11, XXREAL_0: 2;

              (x . (N . m)) = ((x * N) . m) by FUNCT_2: 15, ORDINAL1:def 12;

              hence ( dist (((x * N) . m),z)) < r by A26, A29, XXREAL_0: 2;

            end;

          end;

          then

           A30: (x * N) is convergent;

          ( lim (x * N)) in ( [#] M);

          hence thesis by A30;

        end;

      end;

      then ( [#] M) is sequentially_compact;

      hence M is sequentially_compact;

    end;

    theorem :: TOPMETR4:10

    for M be non empty MetrSpace st M is sequentially_compact holds ( TopSpaceMetr M) is countably_compact

    proof

      let M be non empty MetrSpace;

      assume

       A1: M is sequentially_compact;

      

       A2: for X be Subset of M st X is infinite holds ex x be Element of M st for r be Real st 0 < r holds ( Ball (x,r)) meets (X \ {x})

      proof

        let X be Subset of M;

        assume

         A3: X is infinite;

        then

        consider S1 be sequence of X such that

         A4: S1 is one-to-one by DICKSON: 3;

        

         A5: ( rng S1) c= X;

        ( rng S1) c= ( [#] M) by XBOOLE_1: 1;

        then S1 is Function of ( dom S1), ( [#] M) by FUNCT_2: 2;

        then

        reconsider S1 as sequence of ( [#] M) by A3, FUNCT_2:def 1;

        ( rng S1) c= ( [#] M);

        then

        consider S2 be sequence of M such that

         A6: (ex N be increasing sequence of NAT st S2 = (S1 * N)) & S2 is convergent & ( lim S2) in ( [#] M) by A1, Def1;

        set x = ( lim S2);

        ( rng S2) c= ( rng S1) by A6, RELAT_1: 26;

        then

         A7: ( rng S2) c= X by A5, XBOOLE_1: 1;

        take x;

        thus for r be Real st 0 < r holds ( Ball (x,r)) meets (X \ {x})

        proof

          let r be Real;

          assume 0 < r;

          then

          consider n be Nat such that

           A8: for m be Nat st m >= n holds ( dist ((S2 . m),x)) < r by A6, TBSP_1:def 3;

          per cases ;

            suppose (S2 . n) <> x;

            then

             A9: not (S2 . n) in {x} by TARSKI:def 1;

            n in NAT by ORDINAL1:def 12;

            then (S2 . n) in ( rng S2) by FUNCT_2: 112;

            then

             A10: (S2 . n) in (X \ {x}) by A7, A9, XBOOLE_0:def 5;

            ( dist ((S2 . n),x)) < r by A8;

            then (S2 . n) in ( Ball (x,r)) by METRIC_1: 11;

            hence ( Ball (x,r)) meets (X \ {x}) by A10, XBOOLE_0:def 4;

          end;

            suppose

             A11: (S2 . n) = x;

            consider N be increasing sequence of NAT such that

             A12: S2 = (S1 * N) by A6;

            for x1,x2 be object st x1 in NAT & x2 in NAT & (N . x1) = (N . x2) holds x1 = x2

            proof

              let x1,x2 be object;

              assume

               A13: x1 in NAT & x2 in NAT ;

              then

              reconsider n = x1, m = x2 as Nat;

              assume

               A14: (N . x1) = (N . x2);

              assume x1 <> x2;

              then

               A15: n < m or m < n by XXREAL_0: 1;

              ( dom N) = NAT by FUNCT_2:def 1;

              hence contradiction by A13, A14, A15, SEQM_3:def 1;

            end;

            then N is one-to-one by FUNCT_2: 19;

            then

             A16: S2 is one-to-one by A4, A12, FUNCT_1: 24;

            

             A17: n < (n + 1) by NAT_1: 16;

            n in NAT & (n + 1) in NAT by ORDINAL1:def 12;

            then (S2 . (n + 1)) <> x by A11, A16, A17, FUNCT_2: 19;

            then

             A18: not (S2 . (n + 1)) in {x} by TARSKI:def 1;

            (S2 . (n + 1)) in ( rng S2) by FUNCT_2: 112;

            then

             A19: (S2 . (n + 1)) in (X \ {x}) by A7, A18, XBOOLE_0:def 5;

            ( dist ((S2 . (n + 1)),x)) < r by A8, A17;

            then (S2 . (n + 1)) in ( Ball (x,r)) by METRIC_1: 11;

            hence ( Ball (x,r)) meets (X \ {x}) by A19, XBOOLE_0:def 4;

          end;

        end;

      end;

      

       A20: for A be Subset of ( TopSpaceMetr M) st A is infinite holds ( Der A) is non empty

      proof

        let A be Subset of ( TopSpaceMetr M);

        assume

         A21: A is infinite;

        reconsider X = A as Subset of M;

        consider x be Element of M such that

         A22: for r be Real st 0 < r holds ( Ball (x,r)) meets (X \ {x}) by A2, A21;

        reconsider y = x as Point of ( TopSpaceMetr M);

        y is_an_accumulation_point_of A by A22, Th7;

        hence ( Der A) is non empty by TOPGEN_1: 16;

      end;

      ( TopSpaceMetr M) is T_2 by PCOMPS_1: 34;

      hence ( TopSpaceMetr M) is countably_compact by A20, COMPL_SP: 28;

    end;

    

     Th10: for M be non empty MetrSpace st M is sequentially_compact holds M is totally_bounded complete

    proof

      let M be non empty MetrSpace;

      assume M is sequentially_compact;

      then

       A1: ( [#] M) is sequentially_compact;

      thus M is totally_bounded

      proof

        assume not M is totally_bounded;

        then

        consider r be Real such that

         A2: r > 0 & not (ex G be Subset-Family of M st G is finite & the carrier of M = ( union G) & for C be Subset of M st C in G holds ex w be Element of M st C = ( Ball (w,r)));

        set S0 = the Element of M;

        set G0 = {} ;

        set ABL = { GX where GX be Subset-Family of M : GX is finite & for C be Subset of M st C in GX holds ex w be Element of M st C = ( Ball (w,r)) };

        

         A3: G0 is Subset of ( bool ( [#] M)) by XBOOLE_1: 2;

        for C be Subset of M st C in G0 holds ex w be Element of M st C = ( Ball (w,r));

        then

         A4: G0 in ABL by A3;

        then

        reconsider ABL as non empty set;

        reconsider G0 as Element of ABL by A4;

        defpred P[ Nat, Element of M, set, Element of M, set] means $5 = ($3 \/ {( Ball ($2,r))}) & not $4 in ( union $5);

        

         A5: for n be Nat, x be Element of M, y be Element of ABL holds ex x1 be Element of M, y1 be Element of ABL st P[n, x, y, x1, y1]

        proof

          let n be Nat, x be Element of M, y be Element of ABL;

          y in ABL;

          then

          consider GX be Subset-Family of M such that

           A6: y = GX & GX is finite & for C be Subset of M st C in GX holds ex w be Element of M st C = ( Ball (w,r));

          set y1 = (y \/ {( Ball (x,r))});

          ( Ball (x,r)) in ( bool ( [#] M)) by ZFMISC_1:def 1;

          then {( Ball (x,r))} c= ( bool ( [#] M)) by ZFMISC_1: 31;

          then

          reconsider y1 as Subset-Family of M by A6, XBOOLE_1: 8;

          

           A7: for C be Subset of M st C in y1 holds ex w be Element of M st C = ( Ball (w,r))

          proof

            let C be Subset of M;

            assume C in y1;

            per cases by XBOOLE_0:def 3;

              suppose C in y;

              hence ex w be Element of M st C = ( Ball (w,r)) by A6;

            end;

              suppose C in {( Ball (x,r))};

              then C = ( Ball (x,r)) by TARSKI:def 1;

              hence ex w be Element of M st C = ( Ball (w,r));

            end;

          end;

          then

           A8: y1 in ABL by A6;

           not the carrier of M = ( union y1) by A2, A6, A7;

          then

          consider x1 be object such that

           A9: x1 in the carrier of M & not x1 in ( union y1) by TARSKI:def 3;

          reconsider x1 as Element of M by A9;

          reconsider y1 as Element of ABL by A8;

          take x1, y1;

          thus thesis by A9;

        end;

        consider S1 be sequence of M, Y be sequence of ABL such that

         A10: (S1 . 0 ) = S0 & (Y . 0 ) = G0 & for n be Nat holds P[n, (S1 . n), (Y . n), (S1 . (n + 1)), (Y . (n + 1))] from RECDEF_2:sch 3( A5);

        ( rng S1) c= ( [#] M);

        then

        consider S2 be sequence of M such that

         A11: (ex N be increasing sequence of NAT st S2 = (S1 * N)) & S2 is convergent & ( lim S2) in ( [#] M) by A1;

        defpred Q[ Nat] means for k be Nat st k <= $1 holds ( Ball ((S1 . k),r)) c= ( union (Y . ($1 + 1)));

        

         A12: Q[ 0 ]

        proof

          let k be Nat;

          assume

           A13: k <= 0 ;

          (Y . ( 0 + 1)) = ( {} \/ {( Ball ((S1 . 0 ),r))}) by A10

          .= {( Ball ((S1 . 0 ),r))};

          hence thesis by A13;

        end;

        

         A14: for n be Nat st Q[n] holds Q[(n + 1)]

        proof

          let n be Nat;

          assume

           A15: Q[n];

          

           A16: (Y . ((n + 1) + 1)) = ((Y . (n + 1)) \/ {( Ball ((S1 . (n + 1)),r))}) by A10;

          then

           A17: ( union (Y . (n + 1))) c= ( union (Y . ((n + 1) + 1))) by XBOOLE_1: 7, ZFMISC_1: 77;

          ( Ball ((S1 . (n + 1)),r)) in {( Ball ((S1 . (n + 1)),r))} by TARSKI:def 1;

          then

           A18: ( Ball ((S1 . (n + 1)),r)) in (Y . ((n + 1) + 1)) by A16, TARSKI:def 3, XBOOLE_1: 7;

          let k be Nat;

          assume k <= (n + 1);

          per cases by NAT_1: 8;

            suppose k <= n;

            then ( Ball ((S1 . k),r)) c= ( union (Y . (n + 1))) by A15;

            hence ( Ball ((S1 . k),r)) c= ( union (Y . ((n + 1) + 1))) by A17, XBOOLE_1: 1;

          end;

            suppose k = (n + 1);

            hence ( Ball ((S1 . k),r)) c= ( union (Y . ((n + 1) + 1))) by A18, ZFMISC_1: 74;

          end;

        end;

        

         A19: for n be Nat holds Q[n] from NAT_1:sch 2( A12, A14);

        

         A20: for n,k be Nat st k <= n holds r <= ( dist ((S1 . (n + 1)),(S1 . k)))

        proof

          let n,k be Nat;

          assume k <= n;

          then ( Ball ((S1 . k),r)) c= ( union (Y . (n + 1))) by A19;

          then not (S1 . (n + 1)) in ( Ball ((S1 . k),r)) by A10;

          hence thesis by METRIC_1: 11;

        end;

        

         A21: for n,k be Nat st k < n holds r <= ( dist ((S1 . n),(S1 . k)))

        proof

          let n,k be Nat;

          assume

           A22: k < n;

          then (k + 1) <= n by NAT_1: 13;

          then

           A23: ((k + 1) - 1) <= (n - 1) by XREAL_1: 9;

          reconsider n1 = (n - 1) as Nat by A22;

          r <= ( dist ((S1 . (n1 + 1)),(S1 . k))) by A20, A23;

          hence r <= ( dist ((S1 . n),(S1 . k)));

        end;

         not S2 is convergent

        proof

          assume S2 is convergent;

          then S2 is Cauchy;

          then

          consider p be Nat such that

           A24: for n,m be Nat st p <= n & p <= m holds ( dist ((S2 . n),(S2 . m))) < r by A2;

          consider N be increasing sequence of NAT such that

           A25: S2 = (S1 * N) by A11;

          set q = (p + 1);

          

           A26: p < q by NAT_1: 16;

          

           A27: (S2 . p) = (S1 . (N . p)) & (S2 . q) = (S1 . (N . q)) by A25, FUNCT_2: 15, ORDINAL1:def 12;

          p in NAT & q in NAT by ORDINAL1:def 12;

          then p in ( dom N) & q in ( dom N) by FUNCT_2:def 1;

          then (N . p) < (N . q) by NAT_1: 16, SEQM_3:def 1;

          then r <= ( dist ((S1 . (N . q)),(S1 . (N . p)))) by A21;

          hence contradiction by A24, A26, A27;

        end;

        hence contradiction by A11;

      end;

      now

        let S be sequence of M such that

         A28: S is Cauchy;

        thus S is convergent

        proof

          reconsider S1 = S as sequence of ( [#] M);

          ( rng S1) c= ( [#] M);

          then

          consider S2 be sequence of M such that

           A29: (ex N be increasing sequence of NAT st S2 = (S1 * N)) & S2 is convergent & ( lim S2) in ( [#] M) by A1;

          consider N be increasing sequence of NAT such that

           A30: S2 = (S1 * N) by A29;

          take x = ( lim S2);

          let r be Real;

          assume

           A31: 0 < r;

          then

          consider p be Nat such that

           A32: for n,m be Nat st p <= n & p <= m holds ( dist ((S . n),(S . m))) < (r / 2) by A28;

          consider q be Nat such that

           A33: for m be Nat st m >= q holds ( dist ((S2 . m),( lim S2))) < (r / 2) by A29, A31, TBSP_1:def 3;

          reconsider l = ( max (p,q)) as Nat by XXREAL_0: 16;

          take l;

          let m be Nat;

          assume

           A34: l <= m;

          p <= l by XXREAL_0: 25;

          then

           A35: p <= m by A34, XXREAL_0: 2;

          m <= (N . m) by SEQM_3: 14;

          then p <= (N . m) by A35, XXREAL_0: 2;

          then ( dist ((S . m),(S . (N . m)))) < (r / 2) by A32, A35;

          then

           A36: ( dist ((S . m),(S2 . m))) < (r / 2) by A30, FUNCT_2: 15, ORDINAL1:def 12;

          q <= l by XXREAL_0: 25;

          then q <= m by A34, XXREAL_0: 2;

          then ( dist ((S2 . m),( lim S2))) < (r / 2) by A33;

          then

           A37: (( dist ((S . m),(S2 . m))) + ( dist ((S2 . m),( lim S2)))) < ((r / 2) + (r / 2)) by A36, XREAL_1: 8;

          ( dist ((S . m),x)) <= (( dist ((S . m),(S2 . m))) + ( dist ((S2 . m),x))) by METRIC_1: 4;

          hence thesis by A37, XXREAL_0: 2;

        end;

      end;

      hence M is complete;

    end;

    theorem :: TOPMETR4:11

    

     Th11: for M be non empty MetrSpace holds ( TopSpaceMetr M) is compact iff M is sequentially_compact

    proof

      let M be non empty MetrSpace;

      thus ( TopSpaceMetr M) is compact implies M is sequentially_compact by Th8, COMPL_SP: 35;

      assume M is sequentially_compact;

      then M is totally_bounded complete by Th10;

      hence ( TopSpaceMetr M) is compact by COMPL_SP: 37;

    end;

    theorem :: TOPMETR4:12

    

     Th12: for M be non empty MetrSpace holds M is totally_bounded complete iff M is sequentially_compact

    proof

      let M be non empty MetrSpace;

      M is totally_bounded complete iff ( TopSpaceMetr M) is compact by COMPL_SP: 37;

      hence thesis by Th11;

    end;

    theorem :: TOPMETR4:13

    

     Th14: for M be non empty MetrSpace, S be non empty Subset of M holds S is sequentially_compact iff (M | S) is sequentially_compact

    proof

      let M be non empty MetrSpace, S be non empty Subset of M;

      

       A1: the carrier of (M | S) = S by TOPMETR:def 2;

      set X = ( [#] (M | S));

      hereby

        assume

         A2: S is sequentially_compact;

        for S1 be sequence of (M | S) st ( rng S1) c= X holds ex S2 be sequence of (M | S) st (ex N be increasing sequence of NAT st S2 = (S1 * N)) & S2 is convergent & ( lim S2) in X

        proof

          let S1 be sequence of (M | S);

          assume ( rng S1) c= X;

          

           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 be sequence of M such that

           A4: (ex N be increasing sequence of NAT st SS2 = (SS1 * N)) & SS2 is convergent & ( lim SS2) in S by A2, A3;

          consider N be 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;

          thus ex N be increasing sequence of NAT st S2 = (S1 * N) by A5;

          reconsider x = ( lim SS2) as Element of (M | S) by A4, TOPMETR:def 2;

          now

            let r be Real;

            assume 0 < r;

            then

            consider n be Nat such that

             A6: for m be Nat st n <= m holds ( dist ((SS2 . m),( lim SS2))) < r by A4, TBSP_1:def 3;

            take n;

            thus for m be Nat st n <= m holds ( dist ((S2 . m),x)) < r

            proof

              let m be Nat;

              assume n <= m;

              then ( dist ((SS2 . m),( lim SS2))) < r by A6;

              hence ( dist ((S2 . m),x)) < r by TOPMETR:def 1;

            end;

          end;

          hence S2 is convergent;

          thus ( lim S2) in X;

        end;

        then X is sequentially_compact;

        hence (M | S) is sequentially_compact;

      end;

      assume

       A7: (M | S) is sequentially_compact;

      for S1 be sequence of M st ( rng S1) c= S holds ex S2 be sequence of M st (ex N be increasing sequence of NAT st S2 = (S1 * N)) & S2 is convergent & ( lim S2) in S

      proof

        let S1 be sequence of M;

        assume ( rng S1) c= 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 be sequence of (M | S) such that

         A9: (ex N be increasing sequence of NAT st SS2 = (SS1 * N)) & SS2 is convergent & ( lim SS2) in X by A7, A8, Def1;

        consider N be 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;

        thus ex N be increasing sequence of NAT st S2 = (S1 * N) by A10;

        reconsider x = ( lim SS2) as Element of M by A1, A9;

         A11:

        now

          let r be Real;

          assume 0 < r;

          then

          consider n be Nat such that

           A12: for m be Nat st n <= m holds ( dist ((SS2 . m),( lim SS2))) < r by A9, TBSP_1:def 3;

          take n;

          thus for m be Nat st n <= m holds ( dist ((S2 . m),x)) < r

          proof

            let m be Nat;

            assume n <= m;

            then ( dist ((SS2 . m),( lim SS2))) < r by A12;

            hence ( dist ((S2 . m),x)) < r by TOPMETR:def 1;

          end;

        end;

        hence S2 is convergent;

        then ( lim S2) = x by A11, TBSP_1:def 3;

        hence ( lim S2) in S by A1;

      end;

      hence S is sequentially_compact;

    end;

    theorem :: TOPMETR4:14

    for M be non empty MetrSpace, S be non empty Subset of M holds S is sequentially_compact iff (M | S) is compact

    proof

      let M be non empty MetrSpace, S be non empty Subset of M;

      (M | S) is sequentially_compact iff (M | S) is compact by Th11;

      hence thesis by Th14;

    end;

    theorem :: TOPMETR4:15

    

     Th16: for M be non empty MetrSpace, S be Subset of M, T be Subset of ( TopSpaceMetr M) st T = S holds T is compact iff S is sequentially_compact

    proof

      let M be non empty MetrSpace, S0 be Subset of M, T0 be Subset of ( TopSpaceMetr M);

      assume

       A1: T0 = S0;

      per cases ;

        suppose T0 = {} ;

        hence thesis by A1;

      end;

        suppose

         A2: T0 <> {} ;

        then

        reconsider T = T0 as non empty Subset of ( TopSpaceMetr M);

        reconsider S = T0 as non empty Subset of M by A2;

        hereby

          assume T0 is compact;

          then (( TopSpaceMetr M) | T) is compact;

          then ( TopSpaceMetr (M | S)) is compact by HAUSDORF: 16;

          then (M | S) is sequentially_compact by Th11;

          hence S0 is sequentially_compact by A1, Th14;

        end;

        assume S0 is sequentially_compact;

        then (M | S) is sequentially_compact by A1, Th14;

        then ( TopSpaceMetr (M | S)) is compact by Th11;

        then (( TopSpaceMetr M) | T) is compact by HAUSDORF: 16;

        hence T0 is compact by COMPTS_1: 3;

      end;

    end;

    theorem :: TOPMETR4:16

    for M be non empty MetrSpace, S be non empty Subset of M, T be non empty Subset of ( TopSpaceMetr M) st T = S holds (( TopSpaceMetr M) | T) is countably_compact iff S is sequentially_compact

    proof

      let M be non empty MetrSpace, S be non empty Subset of M, T be non empty Subset of ( TopSpaceMetr M);

      assume

       A1: T = S;

      hereby

        assume (( TopSpaceMetr M) | T) is countably_compact;

        then ( TopSpaceMetr (M | S)) is countably_compact by A1, HAUSDORF: 16;

        then (M | S) is sequentially_compact by Th11, COMPL_SP: 35;

        hence S is sequentially_compact by Th14;

      end;

      assume S is sequentially_compact;

      then (M | S) is sequentially_compact by Th14;

      then ( TopSpaceMetr (M | S)) is countably_compact by Th11, COMPL_SP: 35;

      hence (( TopSpaceMetr M) | T) is countably_compact by A1, HAUSDORF: 16;

    end;

    theorem :: TOPMETR4:17

    for M be non empty MetrSpace, S be non empty Subset of M holds ((M | S) is totally_bounded complete) iff S is sequentially_compact

    proof

      let M be non empty MetrSpace, S be non empty Subset of M;

      hereby

        assume (M | S) is totally_bounded complete;

        then (M | S) is sequentially_compact by Th12;

        hence S is sequentially_compact by Th14;

      end;

      assume S is sequentially_compact;

      then (M | S) is sequentially_compact by Th14;

      hence (M | S) is totally_bounded complete by Th12;

    end;

    begin

    theorem :: TOPMETR4:18

    

     Th19: for NrSp be RealNormSpace, S be Subset of NrSp, T be Subset of ( MetricSpaceNorm NrSp) st S = T holds S is compact iff T is sequentially_compact

    proof

      let NrSp be RealNormSpace, S be Subset of NrSp, T be Subset of ( MetricSpaceNorm NrSp);

      assume

       A1: S = T;

      hereby

        assume

         A2: S is compact;

        now

          let S1 be sequence of ( MetricSpaceNorm NrSp);

          assume

           A3: ( rng S1) c= T;

          reconsider s1 = S1 as sequence of NrSp;

          consider s2 be sequence of NrSp such that

           A4: s2 is subsequence of s1 & s2 is convergent & ( lim s2) in S by A1, A2, A3;

          consider N be increasing sequence of NAT such that

           A5: s2 = (s1 * N) by A4, VALUED_0:def 17;

          reconsider S2 = s2 as sequence of ( MetricSpaceNorm NrSp);

          take S2;

          thus ex N be increasing sequence of NAT st S2 = (S1 * N) by A5;

          thus S2 is convergent by A4, NORMSP_2: 5;

          hence ( lim S2) in T by A1, A4, NORMSP_2: 6;

        end;

        hence T is sequentially_compact;

      end;

      assume

       A6: T is sequentially_compact;

      now

        let s1 be sequence of NrSp;

        assume

         A7: ( rng s1) c= S;

        reconsider S1 = s1 as sequence of ( MetricSpaceNorm NrSp);

        consider S2 be sequence of ( MetricSpaceNorm NrSp) such that

         A8: (ex N be increasing sequence of NAT st S2 = (S1 * N)) & S2 is convergent & ( lim S2) in T by A1, A6, A7;

        consider N be increasing sequence of NAT such that

         A9: S2 = (S1 * N) by A8;

        reconsider s2 = S2 as sequence of NrSp;

        take s2;

        thus s2 is subsequence of s1 by A9;

        thus s2 is convergent by A8, NORMSP_2: 5;

        thus ( lim s2) in S by A1, A8, NORMSP_2: 6;

      end;

      hence S is compact;

    end;

    theorem :: TOPMETR4:19

    for NrSp be RealNormSpace, S be Subset of NrSp, T be Subset of ( TopSpaceNorm NrSp) st S = T holds S is compact iff T is compact

    proof

      let NrSp be RealNormSpace, S be Subset of NrSp, T be Subset of ( TopSpaceNorm NrSp);

      assume

       A1: S = T;

      reconsider W = S as Subset of ( MetricSpaceNorm NrSp);

      W is sequentially_compact iff T is compact by A1, Th16;

      hence thesis by Th19;

    end;

    begin

    theorem :: TOPMETR4:20

    

     Th23: for S1 be sequence of RealSpace , seq be Real_Sequence, g be Real, g1 be Element of RealSpace st S1 = seq & g = g1 holds (for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - g).| < p) iff (for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds ( dist ((S1 . m),g1)) < p)

    proof

      let S1 be sequence of RealSpace , seq be Real_Sequence, g be Real, g1 be Element of RealSpace ;

      assume

       A1: S1 = seq & g = g1;

      hereby

        assume

         A2: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - g).| < p;

        thus for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds ( dist ((S1 . m),g1)) < p

        proof

          let p be Real;

          assume 0 < p;

          then

          consider n be Nat such that

           A3: for m be Nat st n <= m holds |.((seq . m) - g).| < p by A2;

          

           A4: for m be Nat st n <= m holds ( dist ((S1 . m),g1)) < p

          proof

            let m be Nat;

            assume

             C5: n <= m;

            set s = (seq . m);

            set s1 = (S1 . m);

            ( dist (s1,g1)) = |.(s - g).| by A1, TOPMETR: 11;

            hence thesis by A3, C5;

          end;

          take n;

          thus thesis by A4;

        end;

      end;

      assume

       A5: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds ( dist ((S1 . m),g1)) < p;

      thus for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - g).| < p

      proof

        let p be Real;

        assume 0 < p;

        then

        consider n be Nat such that

         A6: for m be Nat st n <= m holds ( dist ((S1 . m),g1)) < p by A5;

        

         A7: for m be Nat st n <= m holds |.((seq . m) - g).| < p

        proof

          let m be Nat;

          assume

           A8: n <= m;

          set s = (seq . m);

          set s1 = (S1 . m);

          ( dist (s1,g1)) = |.(s - g).| by A1, TOPMETR: 11;

          hence thesis by A6, A8;

        end;

        take n;

        thus thesis by A7;

      end;

    end;

    theorem :: TOPMETR4:21

    for S1 be sequence of RealSpace , seq be Real_Sequence, g be Real, g1 be Element of RealSpace st S1 = seq & g = g1 holds (seq is convergent & ( lim seq) = g) iff (S1 is convergent & ( lim S1) = g1)

    proof

      let S1 be sequence of RealSpace , seq be Real_Sequence, g be Real, g1 be Element of RealSpace ;

      assume

       AS: S1 = seq & g = g1;

      hereby

        assume seq is convergent & ( lim seq) = g;

        then for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - g).| < p by SEQ_2:def 7;

        then

         A1: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds ( dist ((S1 . m),g1)) < p by AS, Th23;

        hence S1 is convergent;

        hence ( lim S1) = g1 by A1, TBSP_1:def 3;

      end;

      assume S1 is convergent & ( lim S1) = g1;

      then for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds ( dist ((S1 . m),g1)) < p by TBSP_1:def 3;

      then

       A2: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - g).| < p by AS, Th23;

      hence seq is convergent by SEQ_2:def 6;

      hence ( lim seq) = g by A2, SEQ_2:def 7;

    end;

    theorem :: TOPMETR4:22

    for S1 be sequence of RealSpace , seq be Real_Sequence st S1 = seq & seq is convergent holds S1 is convergent & ( lim S1) = ( lim seq)

    proof

      let S1 be sequence of RealSpace , seq be Real_Sequence;

      assume

       A1: S1 = seq & seq is convergent;

      reconsider g1 = ( lim seq) as Point of RealSpace by XREAL_0:def 1;

      for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - ( lim seq)).| < p by A1, SEQ_2:def 7;

      then

       A2: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds ( dist ((S1 . m),g1)) < p by A1, Th23;

      hence S1 is convergent;

      hence ( lim S1) = ( lim seq) by A2, TBSP_1:def 3;

    end;

    begin

    theorem :: TOPMETR4:23

    

     Th27: for N be Subset of REAL , M be Subset of R^1 st N = M holds (for F be Subset-Family of REAL st F is Cover of N & (for P be Subset of REAL st P in F holds P is open) holds ex G be Subset-Family of REAL st G c= F & G is Cover of N & G is finite) iff (for F1 be Subset-Family of R^1 st F1 is Cover of M & F1 is open holds ex G1 be Subset-Family of R^1 st G1 c= F1 & G1 is Cover of M & G1 is finite)

    proof

      let N be Subset of REAL , M be Subset of R^1 ;

      assume

       A1: N = M;

      hereby

        assume

         A2: for F be Subset-Family of REAL st F is Cover of N & (for P be Subset of REAL st P in F holds P is open) holds ex G be Subset-Family of REAL st G c= F & G is Cover of N & G is finite;

        thus for F1 be Subset-Family of R^1 st F1 is Cover of M & F1 is open holds ex G1 be Subset-Family of R^1 st G1 c= F1 & G1 is Cover of M & G1 is finite

        proof

          let F1 be Subset-Family of R^1 ;

          assume

           A3: F1 is Cover of M & F1 is open;

          reconsider F = F1 as Subset-Family of REAL ;

          for P be Subset of REAL st P in F holds P is open

          proof

            let P be Subset of REAL ;

            assume

             A4: P in F;

            reconsider P1 = P as Subset of R^1 ;

            P1 is open by A3, A4;

            hence P is open by BORSUK_5: 39;

          end;

          then

          consider G be Subset-Family of REAL such that

           A5: G c= F & G is Cover of N & G is finite by A1, A2, A3;

          reconsider G1 = G as Subset-Family of R^1 ;

          take G1;

          thus thesis by A1, A5;

        end;

      end;

      assume

       A6: for F1 be Subset-Family of R^1 st F1 is Cover of M & F1 is open holds ex G1 be Subset-Family of R^1 st G1 c= F1 & G1 is Cover of M & G1 is finite;

      let F be Subset-Family of REAL ;

      assume that

       A7: F is Cover of N and

       A8: for P be Subset of REAL st P in F holds P is open;

      reconsider F1 = F as Subset-Family of R^1 ;

      for P1 be Subset of R^1 st P1 in F1 holds P1 is open

      proof

        let P1 be Subset of R^1 ;

        assume

         A9: P1 in F1;

        reconsider P = P1 as Subset of REAL ;

        P is open by A8, A9;

        hence P1 is open by BORSUK_5: 39;

      end;

      then F1 is open;

      then

      consider G1 be Subset-Family of R^1 such that

       A10: G1 c= F1 & G1 is Cover of M & G1 is finite by A1, A6, A7;

      reconsider G = G1 as Subset-Family of REAL ;

      take G;

      thus thesis by A1, A10;

    end;

    theorem :: TOPMETR4:24

    for N be Subset of REAL holds N is compact iff (for F be Subset-Family of REAL st F is Cover of N & (for P be Subset of REAL st P in F holds P is open) holds ex G be Subset-Family of REAL st G c= F & G is Cover of N & G is finite)

    proof

      let N be Subset of REAL ;

      reconsider M = N as Subset of R^1 ;

      M is compact iff (for F be Subset-Family of REAL st F is Cover of N & for P be Subset of REAL st P in F holds P is open holds ex G be Subset-Family of REAL st G c= F & G is Cover of N & G is finite) by Th27;

      hence thesis by JORDAN5A: 25;

    end;