frechet.miz



    begin

    

     Lm1: for r be Real st r > 0 holds ex n be Nat st (1 / n) < r & n > 0

    proof

      let r be Real;

      assume

       A1: r > 0 ;

      consider n be Nat such that

       A2: (1 / r) < n by SEQ_4: 3;

      take n;

      (1 / (1 / r)) > (1 / n) by A1, A2, XREAL_1: 88;

      hence (1 / n) < r;

      thus thesis by A1, A2;

    end;

    theorem :: FRECHET:1

    for T be non empty 1-sorted, S be sequence of T holds ( rng S) is Subset of T;

    theorem :: FRECHET:2

    

     Th2: for T1 be non empty 1-sorted, T2 be 1-sorted, S be sequence of T1 st ( rng S) c= the carrier of T2 holds S is sequence of T2

    proof

      let T1 be non empty 1-sorted, T2 be 1-sorted, S be sequence of T1;

      

       A1: ( dom S) = NAT by FUNCT_2:def 1;

      assume ( rng S) c= the carrier of T2;

      hence thesis by A1, FUNCT_2: 2;

    end;

    theorem :: FRECHET:3

    

     Th3: for T be non empty TopSpace, x be Point of T, B be Basis of x holds B <> {}

    proof

      let T be non empty TopSpace, x be Point of T, B be Basis of x;

      

       A1: the carrier of T in the topology of T by PRE_TOPC:def 1;

      set U1 = ( [#] T);

      reconsider T as non empty TopStruct;

      U1 is open by A1, PRE_TOPC:def 2;

      then ex U2 be Subset of T st U2 in B & U2 c= U1 by YELLOW_8: 13;

      hence thesis;

    end;

    registration

      let T be non empty TopSpace;

      let x be Point of T;

      cluster -> non empty for Basis of x;

      coherence by Th3;

    end

    

     Lm2: for T be TopStruct, A be Subset of T holds A is open iff (( [#] T) \ A) is closed

    proof

      let T be TopStruct, A be Subset of T;

      thus A is open implies (( [#] T) \ A) is closed

      proof

        assume A is open;

        then (( [#] T) \ (( [#] T) \ A)) is open by PRE_TOPC: 3;

        hence thesis by PRE_TOPC:def 3;

      end;

      assume (( [#] T) \ A) is closed;

      then (( [#] T) \ (( [#] T) \ A)) is open by PRE_TOPC:def 3;

      hence thesis by PRE_TOPC: 3;

    end;

    theorem :: FRECHET:4

    

     Th4: for T be TopSpace, A,B be Subset of T st A is open & B is closed holds (A \ B) is open

    proof

      let T be TopSpace, A,B be Subset of T;

      assume that

       A1: A is open and

       A2: B is closed;

      (( [#] T) \ B) is open by A2, PRE_TOPC:def 3;

      then (A /\ (( [#] T) \ B)) is open by A1, TOPS_1: 11;

      then

       A3: ((A /\ ( [#] T)) \ (A /\ B)) is open by XBOOLE_1: 50;

      (A /\ ( [#] T)) = A by XBOOLE_1: 28;

      hence thesis by A3, XBOOLE_1: 47;

    end;

    theorem :: FRECHET:5

    

     Th5: for T be TopStruct st ( {} T) is closed & ( [#] T) is closed & (for A,B be Subset of T st A is closed & B is closed holds (A \/ B) is closed) & for F be Subset-Family of T st F is closed holds ( meet F) is closed holds T is TopSpace

    proof

      let T be TopStruct;

      assume that

       A1: ( {} T) is closed and

       A2: ( [#] T) is closed and

       A3: for A,B be Subset of T st A is closed & B is closed holds (A \/ B) is closed and

       A4: for F be Subset-Family of T st F is closed holds ( meet F) is closed;

      

       A5: for A,B be Subset of T st A in the topology of T & B in the topology of T holds (A /\ B) in the topology of T

      proof

        let A,B be Subset of T;

        assume that

         A6: A in the topology of T and

         A7: B in the topology of T;

        reconsider A, B as Subset of T;

        B is open by A7, PRE_TOPC:def 2;

        then

         A8: (( [#] T) \ B) is closed by Lm2;

        A is open by A6, PRE_TOPC:def 2;

        then (( [#] T) \ A) is closed by Lm2;

        then ((( [#] T) \ A) \/ (( [#] T) \ B)) is closed by A3, A8;

        then (( [#] T) \ (A /\ B)) is closed by XBOOLE_1: 54;

        then (A /\ B) is open by Lm2;

        hence thesis by PRE_TOPC:def 2;

      end;

      

       A9: for G be Subset-Family of T st G c= the topology of T holds ( union G) in the topology of T

      proof

        let G be Subset-Family of T;

        reconsider G9 = G as Subset-Family of T;

        assume

         A10: G c= the topology of T;

        per cases ;

          suppose

           A11: G = {} ;

          (( [#] T) \ ( {} T)) = ( [#] T);

          then ( {} T) is open by A2, Lm2;

          hence thesis by A11, PRE_TOPC:def 2, ZFMISC_1: 2;

        end;

          suppose

           A12: G <> {} ;

          reconsider CG = ( COMPLEMENT G) as Subset-Family of T;

          

           A13: for A be Subset of T holds A in G implies (( [#] T) \ A) is closed by A10, Lm2, PRE_TOPC:def 2;

          ( COMPLEMENT G) is closed

          proof

            let A be Subset of T;

            assume A in ( COMPLEMENT G);

            then (A ` ) in G9 by SETFAM_1:def 7;

            then (( [#] T) \ (A ` )) is closed by A13;

            hence thesis by PRE_TOPC: 3;

          end;

          then ( meet CG) is closed by A4;

          then (( union G9) ` ) is closed by A12, TOPS_2: 6;

          then (( [#] T) \ ( union G)) is closed;

          then ( union G) is open by Lm2;

          hence thesis by PRE_TOPC:def 2;

        end;

      end;

      (( [#] T) \ ( {} T)) is open by A1, PRE_TOPC:def 3;

      then the carrier of T in the topology of T by PRE_TOPC:def 2;

      hence thesis by A9, A5, PRE_TOPC:def 1;

    end;

    theorem :: FRECHET:6

    

     Th6: for T be TopSpace, S be non empty TopStruct, f be Function of T, S st for A be Subset of S holds A is closed iff (f " A) is closed holds S is TopSpace

    proof

      let T be TopSpace, S be non empty TopStruct, f be Function of T, S;

      assume

       A1: for A be Subset of S holds A is closed iff (f " A) is closed;

      

       A2: for A,B be Subset of S st A is closed & B is closed holds (A \/ B) is closed

      proof

        let A,B be Subset of S;

        assume A is closed & B is closed;

        then (f " A) is closed & (f " B) is closed by A1;

        then ((f " A) \/ (f " B)) is closed by TOPS_1: 9;

        then (f " (A \/ B)) is closed by RELAT_1: 140;

        hence thesis by A1;

      end;

      ( {} T) is closed & (f " {} ) = {} ;

      then

       A3: ( {} S) is closed by A1;

      

       A4: for F be Subset-Family of S st F is closed holds ( meet F) is closed

      proof

        let F be Subset-Family of S;

        assume

         A5: F is closed;

        per cases ;

          suppose F = ( {} S);

          hence thesis by A3, SETFAM_1:def 1;

        end;

          suppose

           A6: F <> {} ;

          set F1 = { (f " A) where A be Subset of S : A in F };

          ex A be set st A in F

          proof

            set A = the Element of F;

            take A;

            thus thesis by A6;

          end;

          then

          consider A be Subset of S such that

           A7: A in F;

          reconsider A as Subset of S;

          

           A8: (f " A) in F1 by A7;

          F1 c= ( bool the carrier of T)

          proof

            let B be object;

            assume B in F1;

            then ex A be Subset of S st B = (f " A) & A in F;

            hence thesis;

          end;

          then

          reconsider F1 as Subset-Family of T;

          

           A9: ( meet F1) c= (f " ( meet F))

          proof

            let x be object;

            assume

             A10: x in ( meet F1);

            for A be set st A in F holds (f . x) in A

            proof

              let A be set;

              assume

               A11: A in F;

              then

              reconsider A as Subset of S;

              (f " A) in F1 by A11;

              then x in (f " A) by A10, SETFAM_1:def 1;

              hence thesis by FUNCT_1:def 7;

            end;

            then

             A12: (f . x) in ( meet F) by A6, SETFAM_1:def 1;

            x in the carrier of T by A10;

            then x in ( dom f) by FUNCT_2:def 1;

            hence thesis by A12, FUNCT_1:def 7;

          end;

          F1 is closed

          proof

            let B be Subset of T;

            assume B in F1;

            then

            consider A be Subset of S such that

             A13: (f " A) = B and

             A14: A in F;

            A is closed by A5, A14;

            hence thesis by A1, A13;

          end;

          then

           A15: ( meet F1) is closed by TOPS_2: 22;

          (f " ( meet F)) c= ( meet F1)

          proof

            let x be object;

            assume

             A16: x in (f " ( meet F));

            then

             A17: (f . x) in ( meet F) by FUNCT_1:def 7;

            

             A18: x in ( dom f) by A16, FUNCT_1:def 7;

            for B be set st B in F1 holds x in B

            proof

              let B be set;

              assume B in F1;

              then

              consider A be Subset of S such that

               A19: B = (f " A) and

               A20: A in F;

              (f . x) in A by A17, A20, SETFAM_1:def 1;

              hence thesis by A18, A19, FUNCT_1:def 7;

            end;

            hence thesis by A8, SETFAM_1:def 1;

          end;

          then ( meet F1) = (f " ( meet F)) by A9;

          hence thesis by A1, A15;

        end;

      end;

      (f " ( [#] S)) = ( [#] T) by TOPS_2: 41;

      then ( [#] S) is closed by A1;

      hence thesis by A3, A2, A4, Th5;

    end;

    theorem :: FRECHET:7

    

     Th7: for x be Point of RealSpace , r be Real holds ( Ball (x,r)) = ].(x - r), (x + r).[

    proof

      let x be Point of RealSpace , r be Real;

      reconsider x2 = x as Element of REAL by METRIC_1:def 13;

      thus ( Ball (x,r)) c= ].(x - r), (x + r).[

      proof

        let y be object;

        assume

         A1: y in ( Ball (x,r));

        then

        reconsider y1 = y as Element of RealSpace ;

        reconsider y2 = y1 as Element of REAL by METRIC_1:def 13;

        

         A2: ( dist (x,y1)) = ( real_dist . (x2,y2)) by METRIC_1:def 1, METRIC_1:def 13

        .= |.(x2 - y2).| by METRIC_1:def 12

        .= |.( - (y2 - x2)).|

        .= |.(y2 - x2).| by COMPLEX1: 52;

        ( dist (x,y1)) < r by A1, METRIC_1: 11;

        hence thesis by A2, RCOMP_1: 1;

      end;

      let y be object;

      assume

       A3: y in ].(x - r), (x + r).[;

      then

      reconsider y2 = y as Element of REAL ;

      reconsider x1 = x, y1 = y2 as Element of RealSpace by METRIC_1:def 13;

       |.(y2 - x).| = |.( - (y2 - x)).| by COMPLEX1: 52

      .= |.(x - y2).|

      .= ( real_dist . (x2,y2)) by METRIC_1:def 12;

      then

       A4: ( real_dist . (x2,y2)) < r by A3, RCOMP_1: 1;

      ( dist (x1,y1)) = ( real_dist . (x2,y2)) by METRIC_1:def 1, METRIC_1:def 13;

      hence thesis by A4, METRIC_1: 11;

    end;

    theorem :: FRECHET:8

    for A be Subset of R^1 holds A is open iff for x be Real st x in A holds ex r be Real st r > 0 & ].(x - r), (x + r).[ c= A

    proof

      let A be Subset of R^1 ;

      reconsider A1 = A as Subset of RealSpace by TOPMETR: 12;

      thus A is open implies for x be Real st x in A holds ex r be Real st r > 0 & ].(x - r), (x + r).[ c= A

      proof

        reconsider A1 = A as Subset of R^1 ;

        

         A1: the topology of R^1 = ( Family_open_set RealSpace ) by TOPMETR: 12;

        assume A is open;

        then

         A2: A1 in the topology of R^1 by PRE_TOPC:def 2;

        let x be Real;

        reconsider x1 = x as Element of REAL by XREAL_0:def 1;

        reconsider x1 as Element of RealSpace by METRIC_1:def 13;

        assume x in A;

        then

        consider r be Real such that

         A3: r > 0 and

         A4: ( Ball (x1,r)) c= A1 by A2, A1, PCOMPS_1:def 4;

         ].(x - r), (x + r).[ c= A1 by A4, Th7;

        hence thesis by A3;

      end;

      assume

       A5: for x be Real st x in A holds ex r be Real st r > 0 & ].(x - r), (x + r).[ c= A;

      for x be Element of RealSpace st x in A1 holds ex r be Real st r > 0 & ( Ball (x,r)) c= A1

      proof

        let x be Element of RealSpace ;

        reconsider x1 = x as Real;

        assume x in A1;

        then

        consider r be Real such that

         A6: r > 0 and

         A7: ].(x1 - r), (x1 + r).[ c= A1 by A5;

        ( Ball (x,r)) c= A1 by A7, Th7;

        hence thesis by A6;

      end;

      then

       A8: A1 in ( Family_open_set RealSpace ) by PCOMPS_1:def 4;

      the topology of R^1 = ( Family_open_set RealSpace ) by TOPMETR: 12;

      hence thesis by A8, PRE_TOPC:def 2;

    end;

    theorem :: FRECHET:9

    

     Th9: for S be sequence of R^1 st (for n be Element of NAT holds (S . n) in ].(n - (1 / 4)), (n + (1 / 4)).[) holds ( rng S) is closed

    proof

      let S be sequence of R^1 ;

      reconsider B = ( rng S) as Subset of R^1 ;

      assume

       A1: for n be Element of NAT holds (S . n) in ].(n - (1 / 4)), (n + (1 / 4)).[;

      for x be Point of RealSpace st x in (B ` ) holds ex r be Real st r > 0 & ( Ball (x,r)) c= (B ` )

      proof

        let x be Point of RealSpace ;

        assume

         A2: x in (B ` );

        reconsider x1 = x as Real;

        per cases ;

          suppose

           A3: ( ].(x1 - (1 / 4)), (x1 + (1 / 4)).[ /\ B) = {} ;

          reconsider C = ( Ball (x,(1 / 4))) as Subset of R^1 by TOPMETR: 12;

          (( Ball (x,(1 / 4))) /\ ((B ` ) ` )) = {} by A3, Th7;

          then C misses ((B ` ) ` );

          then ( Ball (x,(1 / 4))) c= (B ` ) by SUBSET_1: 24;

          hence thesis;

        end;

          suppose

           A4: ( ].(x1 - (1 / 4)), (x1 + (1 / 4)).[ /\ B) <> {} ;

          set y = the Element of ( ].(x1 - (1 / 4)), (x1 + (1 / 4)).[ /\ B);

          

           A5: y in ].(x1 - (1 / 4)), (x1 + (1 / 4)).[ by A4, XBOOLE_0:def 4;

          

           A6: y in B by A4, XBOOLE_0:def 4;

          reconsider y as Real;

          consider n1 be object such that

           A7: n1 in ( dom S) and

           A8: y = (S . n1) by A6, FUNCT_1:def 3;

          reconsider n1 as Element of NAT by A7;

          set r = |.(x1 - y).|;

          reconsider C = ( Ball (x,r)) as Subset of R^1 by TOPMETR: 12;

           |.(y - x1).| < (1 / 4) by A5, RCOMP_1: 1;

          then |.( - (x1 - y)).| < (1 / 4);

          then

           A9: r <= (1 / 4) by COMPLEX1: 52;

          ( Ball (x,r)) misses ( rng S)

          proof

            assume ( Ball (x,r)) meets ( rng S);

            then

            consider z be object such that

             A10: z in ( Ball (x,r)) and

             A11: z in ( rng S) by XBOOLE_0: 3;

            consider n2 be object such that

             A12: n2 in ( dom S) and

             A13: z = (S . n2) by A11, FUNCT_1:def 3;

            reconsider n2 as Element of NAT by A12;

            reconsider z as Real by A10;

            per cases by XXREAL_0: 1;

              suppose

               A14: n1 = n2;

              

               A15: r = |.( 0 + ( - (y - x1))).|

              .= |.(y - x1).| by COMPLEX1: 52;

              y in ].(x1 - r), (x1 + r).[ by A8, A10, A13, A14, Th7;

              hence contradiction by A15, RCOMP_1: 1;

            end;

              suppose

               A16: n1 > n2;

              (S . n1) in ].(n1 - (1 / 4)), (n1 + (1 / 4)).[ by A1;

              then (S . n1) in { a where a be Real : (n1 - (1 / 4)) < a & a < (n1 + (1 / 4)) } by RCOMP_1:def 2;

              then ex a1 be Real st (S . n1) = a1 & (n1 - (1 / 4)) < a1 & a1 < (n1 + (1 / 4));

              then

               A17: n1 < (y + (1 / 4)) by A8, XREAL_1: 19;

              (S . n2) in ].(n2 - (1 / 4)), (n2 + (1 / 4)).[ by A1;

              then (S . n2) in { a where a be Real : (n2 - (1 / 4)) < a & a < (n2 + (1 / 4)) } by RCOMP_1:def 2;

              then ex a2 be Real st (S . n2) = a2 & (n2 - (1 / 4)) < a2 & a2 < (n2 + (1 / 4));

              then (z - (1 / 4)) < n2 by A13, XREAL_1: 19;

              then

               A18: (n2 + 1) > ((z - (1 / 4)) + 1) by XREAL_1: 6;

              (n2 + 1) <= n1 by A16, NAT_1: 13;

              then (n2 + 1) < (y + (1 / 4)) by A17, XXREAL_0: 2;

              then (z + (( - (1 / 4)) + 1)) < (y + (1 / 4)) by A18, XXREAL_0: 2;

              then

               A19: z < ((y + (1 / 4)) - (( - (1 / 4)) + 1)) by XREAL_1: 20;

              ( Ball (x,r)) c= ( Ball (x,(1 / 4))) by A9, PCOMPS_1: 1;

              then z in ( Ball (x,(1 / 4))) by A10;

              then z in ].(x1 - (1 / 4)), (x1 + (1 / 4)).[ by Th7;

              then z in { a where a be Real : (x1 - (1 / 4)) < a & a < (x1 + (1 / 4)) } by RCOMP_1:def 2;

              then ex a1 be Real st a1 = z & (x1 - (1 / 4)) < a1 & a1 < (x1 + (1 / 4));

              then

               A20: (z + (1 / 4)) > x1 by XREAL_1: 19;

              y in { a where a be Real : (x1 - (1 / 4)) < a & a < (x1 + (1 / 4)) } by A5, RCOMP_1:def 2;

              then ex a1 be Real st y = a1 & (x1 - (1 / 4)) < a1 & a1 < (x1 + (1 / 4));

              then (y - (1 / 4)) < ((x1 + (1 / 4)) - (1 / 4)) by XREAL_1: 9;

              then (z + (1 / 4)) > (y - (1 / 4)) by A20, XXREAL_0: 2;

              then ((z + (1 / 4)) + ( - (1 / 4))) > ((y - (1 / 4)) + ( - (1 / 4))) by XREAL_1: 6;

              hence contradiction by A19;

            end;

              suppose

               A21: n1 < n2;

              (S . n2) in ].(n2 - (1 / 4)), (n2 + (1 / 4)).[ by A1;

              then (S . n2) in { a where a be Real : (n2 - (1 / 4)) < a & a < (n2 + (1 / 4)) } by RCOMP_1:def 2;

              then ex a2 be Real st (S . n2) = a2 & (n2 - (1 / 4)) < a2 & a2 < (n2 + (1 / 4));

              then

               A22: (z + (1 / 4)) > ((n2 + ( - (1 / 4))) + (1 / 4)) by A13, XREAL_1: 6;

              (S . n1) in ].(n1 - (1 / 4)), (n1 + (1 / 4)).[ by A1;

              then (S . n1) in { a where a be Real : (n1 - (1 / 4)) < a & a < (n1 + (1 / 4)) } by RCOMP_1:def 2;

              then ex a1 be Real st (S . n1) = a1 & (n1 - (1 / 4)) < a1 & a1 < (n1 + (1 / 4));

              then ((n1 + (1 / 4)) - (1 / 4)) > (y - (1 / 4)) by A8, XREAL_1: 9;

              then

               A23: (n1 + 1) > ((y - (1 / 4)) + 1) by XREAL_1: 6;

              (n1 + 1) <= n2 by A21, NAT_1: 13;

              then (z + (1 / 4)) > (n1 + 1) by A22, XXREAL_0: 2;

              then ((y + ( - (1 / 4))) + 1) < (z + (1 / 4)) by A23, XXREAL_0: 2;

              then

               A24: ((y + (( - (1 / 4)) + 1)) - (( - (1 / 4)) + 1)) < ((z + (1 / 4)) - (( - (1 / 4)) + 1)) by XREAL_1: 9;

              ( Ball (x,r)) c= ( Ball (x,(1 / 4))) by A9, PCOMPS_1: 1;

              then z in ( Ball (x,(1 / 4))) by A10;

              then z in ].(x1 - (1 / 4)), (x1 + (1 / 4)).[ by Th7;

              then z in { a where a be Real : (x1 - (1 / 4)) < a & a < (x1 + (1 / 4)) } by RCOMP_1:def 2;

              then ex a1 be Real st a1 = z & (x1 - (1 / 4)) < a1 & a1 < (x1 + (1 / 4));

              then

               A25: (z - (1 / 4)) < x1 by XREAL_1: 19;

              y in { a where a be Real : (x1 - (1 / 4)) < a & a < (x1 + (1 / 4)) } by A5, RCOMP_1:def 2;

              then ex a1 be Real st y = a1 & (x1 - (1 / 4)) < a1 & a1 < (x1 + (1 / 4));

              then ((x1 + ( - (1 / 4))) + (1 / 4)) < (y + (1 / 4)) by XREAL_1: 6;

              then (z - (1 / 4)) < (y + (1 / 4)) by A25, XXREAL_0: 2;

              then ((z - (1 / 4)) + (1 / 4)) < ((y + (1 / 4)) + (1 / 4)) by XREAL_1: 6;

              then (z - (1 / 2)) < ((y + (1 / 2)) - (1 / 2)) by XREAL_1: 9;

              hence contradiction by A24;

            end;

          end;

          then C misses ((B ` ) ` );

          then

           A26: C c= (B ` ) by SUBSET_1: 24;

          x1 <> y

          proof

            assume x1 = y;

            then y in (B /\ (B ` )) by A2, A6, XBOOLE_0:def 4;

            then B meets (B ` );

            hence contradiction by SUBSET_1: 24;

          end;

          then (x1 + ( - y)) <> (y + ( - y));

          then |.(x1 - y).| > 0 by COMPLEX1: 47;

          hence thesis by A26;

        end;

      end;

      then (( [#] R^1 ) \ ( rng S)) is open by TOPMETR: 15;

      hence thesis by PRE_TOPC:def 3;

    end;

    theorem :: FRECHET:10

    

     Th10: for B be Subset of R^1 holds B = NAT implies B is closed

    proof

      let B be Subset of R^1 ;

      

       A1: ( dom ( id NAT )) = NAT ;

      

       A2: ( rng ( id NAT )) = NAT ;

      then

      reconsider S = ( id NAT ) as sequence of R^1 by A1, FUNCT_2: 2, TOPMETR: 17, NUMBERS: 19;

      for n be Element of NAT holds (S . n) in ].(n - (1 / 4)), (n + (1 / 4)).[

      proof

        let n be Element of NAT ;

        reconsider x = (S . n) as Real;

        

         A3: (( - (1 / 4)) + n) < ( 0 + n) by XREAL_1: 8;

        x = n & n < (n + (1 / 4)) by XREAL_1: 29;

        then x in { r where r be Real : (n - (1 / 4)) < r & r < (n + (1 / 4)) } by A3;

        hence thesis by RCOMP_1:def 2;

      end;

      hence thesis by A2, Th9;

    end;

    definition

      let M be non empty MetrStruct, x be Point of ( TopSpaceMetr M);

      :: FRECHET:def1

      func Balls (x) -> Subset-Family of ( TopSpaceMetr M) means

      : Def1: ex y be Point of M st y = x & it = { ( Ball (y,(1 / n))) where n be Nat : n <> 0 };

      existence

      proof

        

         A1: the carrier of M = the carrier of ( TopSpaceMetr M) by TOPMETR: 12;

        then

        reconsider y = x as Point of M;

        set B = { ( Ball (y,(1 / n))) where n be Nat : n <> 0 };

        B c= ( bool the carrier of ( TopSpaceMetr M))

        proof

          let A be object;

          assume A in B;

          then ex n be Nat st A = ( Ball (y,(1 / n))) & n <> 0 ;

          hence thesis by A1;

        end;

        hence thesis;

      end;

      uniqueness ;

    end

    registration

      let M be non empty MetrSpace, x be Point of ( TopSpaceMetr M);

      cluster ( Balls x) -> openx -quasi_basis;

      coherence

      proof

        set B = ( Balls x);

        consider x9 be Point of M such that

         A1: x9 = x & B = { ( Ball (x9,(1 / n))) where n be Nat : n <> 0 } by Def1;

        

         A2: B c= the topology of ( TopSpaceMetr M)

        proof

          let A be object;

          assume A in B;

          then

          consider n be Nat such that

           A3: A = ( Ball (x9,(1 / n))) and n <> 0 by A1;

          ( Ball (x9,(1 / n))) in ( Family_open_set M) by PCOMPS_1: 29;

          hence thesis by A3, TOPMETR: 12;

        end;

        

         A4: for O be set st O in B holds x in O

        proof

          let O be set;

          assume O in B;

          then ex n be Nat st O = ( Ball (x9,(1 / n))) & n <> 0 by A1;

          hence thesis by A1, GOBOARD6: 1;

        end;

        

         A5: for O be Subset of ( TopSpaceMetr M) st O is open & x in O holds ex V be Subset of ( TopSpaceMetr M) st V in B & V c= O

        proof

          let O be Subset of ( TopSpaceMetr M);

          assume O is open & x in O;

          then

          consider r be Real such that

           A6: r > 0 and

           A7: ( Ball (x9,r)) c= O by A1, TOPMETR: 15;

          reconsider r as Real;

          consider n be Nat such that

           A8: (1 / n) < r and

           A9: n > 0 by A6, Lm1;

          reconsider Ba = ( Ball (x9,(1 / n))) as Subset of ( TopSpaceMetr M) by TOPMETR: 12;

          reconsider Ba as Subset of ( TopSpaceMetr M);

          take Ba;

          thus Ba in B by A1, A9;

          ( Ball (x9,(1 / n))) c= ( Ball (x9,r)) by A8, PCOMPS_1: 1;

          hence thesis by A7;

        end;

        

         A10: ( Ball (x9,(1 / 1))) in B by A1;

        then ( Intersect B) = ( meet B) by SETFAM_1:def 9;

        then x in ( Intersect B) by A10, A4, SETFAM_1:def 1;

        hence thesis by A2, A5, TOPS_2: 64, YELLOW_8:def 1;

      end;

    end

    registration

      let M be non empty MetrSpace, x be Point of ( TopSpaceMetr M);

      cluster ( Balls x) -> countable;

      coherence

      proof

        set B = ( Balls x);

        consider x9 be Point of M such that

         A1: x9 = x & B = { ( Ball (x9,(1 / n))) where n be Nat : n <> 0 } by Def1;

        deffunc F( Nat) = ( Ball (x9,(1 / $1)));

        defpred P[ Nat] means $1 <> 0 ;

        { F(n) where n be Nat : P[n] } is countable from CARD_4:sch 1;

        hence thesis by A1;

      end;

    end

    theorem :: FRECHET:11

    

     Th11: for M be non empty MetrSpace, x be Point of ( TopSpaceMetr M), x9 be Point of M st x = x9 holds ex f be sequence of ( Balls x) st for n be Element of NAT holds (f . n) = ( Ball (x9,(1 / (n + 1))))

    proof

      let M be non empty MetrSpace, x be Point of ( TopSpaceMetr M), x9 be Point of M;

      assume

       A1: x = x9;

      set B = ( Balls x);

      consider x9 be Point of M such that

       A2: x9 = x & B = { ( Ball (x9,(1 / n))) where n be Nat : n <> 0 } by Def1;

      defpred P[ object, object] means ex n9 be Element of NAT st $1 = n9 & $2 = ( Ball (x9,(1 / (n9 + 1))));

      

       A3: for n be object st n in NAT holds ex O be object st O in B & P[n, O]

      proof

        let n be object;

        assume n in NAT ;

        then

        reconsider n as Element of NAT ;

        take ( Ball (x9,(1 / (n + 1))));

        thus thesis by A2;

      end;

      consider f be Function such that

       A4: ( dom f) = NAT & ( rng f) c= B and

       A5: for n be object st n in NAT holds P[n, (f . n)] from FUNCT_1:sch 6( A3);

      reconsider f as sequence of B by A4, FUNCT_2: 2;

      take f;

      let n be Element of NAT ;

       P[n, (f . n)] by A5;

      hence thesis by A2, A1;

    end;

    theorem :: FRECHET:12

    

     Th12: for f,g be Function holds ( rng (f +* g)) = ((f .: (( dom f) \ ( dom g))) \/ ( rng g))

    proof

      let f,g be Function;

      thus ( rng (f +* g)) c= ((f .: (( dom f) \ ( dom g))) \/ ( rng g))

      proof

        let y be object;

        assume y in ( rng (f +* g));

        then

        consider x be object such that

         A1: x in ( dom (f +* g)) and

         A2: ((f +* g) . x) = y by FUNCT_1:def 3;

        per cases ;

          suppose

           A3: x in ( dom g);

          then y = (g . x) by A2, FUNCT_4: 13;

          then y in ( rng g) by A3, FUNCT_1:def 3;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose

           A4: not x in ( dom g);

          x in (( dom f) \/ ( dom g)) by A1, FUNCT_4:def 1;

          then x in ( dom f) by A4, XBOOLE_0:def 3;

          then

           A5: x in (( dom f) \ ( dom g)) by A4, XBOOLE_0:def 5;

          y = (f . x) by A2, A4, FUNCT_4: 11;

          then y in (f .: (( dom f) \ ( dom g))) by A5, FUNCT_1:def 6;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      let y be object;

      assume

       A6: y in ((f .: (( dom f) \ ( dom g))) \/ ( rng g));

      per cases by A6, XBOOLE_0:def 3;

        suppose y in (f .: (( dom f) \ ( dom g)));

        then

        consider x be object such that

         A7: x in ( dom f) and

         A8: x in (( dom f) \ ( dom g)) and

         A9: (f . x) = y by FUNCT_1:def 6;

         not x in ( dom g) by A8, XBOOLE_0:def 5;

        then

         A10: ((f +* g) . x) = (f . x) by FUNCT_4: 11;

        x in (( dom f) \/ ( dom g)) by A7, XBOOLE_0:def 3;

        then x in ( dom (f +* g)) by FUNCT_4:def 1;

        hence thesis by A9, A10, FUNCT_1:def 3;

      end;

        suppose

         A11: y in ( rng g);

        ( rng g) c= ( rng (f +* g)) by FUNCT_4: 18;

        hence thesis by A11;

      end;

    end;

    theorem :: FRECHET:13

    

     Th13: for A,B be set holds B c= A implies (( id A) .: B) = B

    proof

      let A,B be set;

      assume

       A1: B c= A;

      thus (( id A) .: B) c= B

      proof

        let y be object;

        assume y in (( id A) .: B);

        then ex x be object st x in ( dom ( id A)) & x in B & (( id A) . x) = y by FUNCT_1:def 6;

        hence thesis by FUNCT_1: 17;

      end;

      let y be object;

      assume

       A2: y in B;

      then ( dom ( id A)) = A & (( id A) . y) = y by A1, FUNCT_1: 17;

      hence thesis by A1, A2, FUNCT_1:def 6;

    end;

    theorem :: FRECHET:14

    

     Th14: for A,B,x be set holds ( dom (( id A) +* (B --> x))) = (A \/ B)

    proof

      let A,B,x be set;

      ( dom (( id A) +* (B --> x))) = (( dom ( id A)) \/ ( dom (B --> x))) by FUNCT_4:def 1;

      then ( dom (( id A) +* (B --> x))) = (A \/ ( dom (B --> x)));

      hence thesis by FUNCOP_1: 13;

    end;

    theorem :: FRECHET:15

    

     Th15: for A,B,x be set st B <> {} holds ( rng (( id A) +* (B --> x))) = ((A \ B) \/ {x})

    proof

      let A,B,x be set;

      set f = (( id A) +* (B --> x));

      assume B <> {} ;

      then

       A1: ( rng (B --> x)) = {x} by FUNCOP_1: 8;

      thus ( rng (( id A) +* (B --> x))) c= ((A \ B) \/ {x})

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x1 be object such that

         A2: x1 in ( dom f) and

         A3: y = (f . x1) by FUNCT_1:def 3;

        

         A4: x1 in (( dom ( id A)) \/ ( dom (B --> x))) by A2, FUNCT_4:def 1;

        per cases ;

          suppose x1 in ( dom (B --> x));

          then (f . x1) = ((B --> x) . x1) & ((B --> x) . x1) = x by A4, FUNCOP_1: 7, FUNCT_4:def 1;

          then y in {x} by A3, TARSKI:def 1;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose

           A5: not x1 in ( dom (B --> x));

          then

           A6: (f . x1) = (( id A) . x1) by A4, FUNCT_4:def 1;

          

           A7: x1 in ( dom ( id A)) by A4, A5, XBOOLE_0:def 3;

           not x1 in B by A5, FUNCOP_1: 13;

          then x1 in (A \ B) by A7, XBOOLE_0:def 5;

          then x1 in ((A \ B) \/ {x}) by XBOOLE_0:def 3;

          hence thesis by A3, A6, A7, FUNCT_1: 18;

        end;

      end;

      let y be object;

      (( id A) .: (A \ B)) = (A \ B) by Th13;

      then (( id A) .: (( dom ( id A)) \ B)) = (A \ B);

      then

       A8: (( id A) .: (( dom ( id A)) \ ( dom (B --> x)))) = (A \ B) by FUNCOP_1: 13;

      assume y in ((A \ B) \/ {x});

      hence thesis by A1, A8, Th12;

    end;

    theorem :: FRECHET:16

    

     Th16: for A,B,C,x be set holds C c= A implies ((( id A) +* (B --> x)) " (C \ {x})) = ((C \ B) \ {x})

    proof

      let A,B,C,x be set;

      assume

       A1: C c= A;

      set f = (( id A) +* (B --> x));

      thus (f " (C \ {x})) c= ((C \ B) \ {x})

      proof

        let x1 be object;

        assume

         A2: x1 in (f " (C \ {x}));

        then

         A3: (f . x1) in (C \ {x}) by FUNCT_1:def 7;

        

         A4: not x1 in B

        proof

          assume

           A5: x1 in B;

          then

           A6: x1 in ( dom (B --> x)) by FUNCOP_1: 13;

          then x1 in (( dom ( id A)) \/ ( dom (B --> x))) by XBOOLE_0:def 3;

          then (f . x1) = ((B --> x) . x1) by A6, FUNCT_4:def 1;

          then

           A7: (f . x1) = x by A5, FUNCOP_1: 7;

           not (f . x1) in {x} by A3, XBOOLE_0:def 5;

          hence contradiction by A7, TARSKI:def 1;

        end;

        then

         A8: not x1 in ( dom (B --> x));

        x1 in ( dom f) by A2, FUNCT_1:def 7;

        then x1 in (A \/ B) by Th14;

        then

         A9: x1 in A or x1 in B by XBOOLE_0:def 3;

        then x1 in ( dom ( id A)) by A4;

        then x1 in (( dom ( id A)) \/ ( dom (B --> x))) by XBOOLE_0:def 3;

        then (f . x1) = (( id A) . x1) by A8, FUNCT_4:def 1;

        then

         A10: (f . x1) = x1 by A4, A9, FUNCT_1: 17;

        then

         A11: not x1 in {x} by A3, XBOOLE_0:def 5;

        x1 in (C \ B) by A3, A4, A10, XBOOLE_0:def 5;

        hence thesis by A11, XBOOLE_0:def 5;

      end;

      let x1 be object;

      assume

       A12: x1 in ((C \ B) \ {x});

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

      then

       A13: x1 in (C \ {x}) by A12, XBOOLE_0:def 5;

      

       A14: x1 in C by A12;

      then x1 in A by A1;

      then x1 in ( dom ( id A));

      then

       A15: x1 in (( dom ( id A)) \/ ( dom (B --> x))) by XBOOLE_0:def 3;

      x1 in (C \ B) by A12, XBOOLE_0:def 5;

      then not x1 in ( dom (B --> x)) by XBOOLE_0:def 5;

      then (f . x1) = (( id A) . x1) by A15, FUNCT_4:def 1;

      then

       A16: (f . x1) = x1 by A1, A14, FUNCT_1: 17;

      x1 in ( dom f) by A15, FUNCT_4:def 1;

      hence thesis by A13, A16, FUNCT_1:def 7;

    end;

    theorem :: FRECHET:17

    

     Th17: for A,B,x be set holds not x in A implies ((( id A) +* (B --> x)) " {x}) = B

    proof

      let A,B,x be set;

      set f = (( id A) +* (B --> x));

      assume

       A1: not x in A;

      thus (f " {x}) c= B

      proof

        let y be object;

        assume

         A2: y in (f " {x});

        then

         A3: y in ( dom f) by FUNCT_1:def 7;

        

         A4: (f . y) in {x} by A2, FUNCT_1:def 7;

        per cases ;

          suppose y in ( dom (B --> x));

          hence thesis;

        end;

          suppose

           A5: not y in ( dom (B --> x));

          then

           A6: (f . y) = (( id A) . y) by FUNCT_4: 11;

          

           A7: y in ( dom (B --> x)) or y in ( dom ( id A)) by A3, FUNCT_4: 12;

          then (( id A) . y) = y by A5, FUNCT_1: 18;

          then y = x by A4, A6, TARSKI:def 1;

          hence thesis by A1, A7;

        end;

      end;

      let y be object;

      assume

       A8: y in B;

      then

       A9: y in ( dom (B --> x)) by FUNCOP_1: 13;

      then (f . y) = ((B --> x) . y) by FUNCT_4: 13;

      then (f . y) = x by A8, FUNCOP_1: 7;

      then

       A10: (f . y) in {x} by TARSKI:def 1;

      y in ( dom f) by A9, FUNCT_4: 12;

      hence thesis by A10, FUNCT_1:def 7;

    end;

    theorem :: FRECHET:18

    

     Th18: for A,B,C,x be set holds C c= A & not x in A implies ((( id A) +* (B --> x)) " (C \/ {x})) = (C \/ B)

    proof

      let A,B,C,x be set;

      assume that

       A1: C c= A and

       A2: not x in A;

      

       A3: (C \ {x}) = C

      proof

        thus (C \ {x}) c= C;

        let y be object;

        assume

         A4: y in C;

         not y in {x}

        proof

          assume y in {x};

          then y = x by TARSKI:def 1;

          hence contradiction by A1, A2, A4;

        end;

        hence thesis by A4, XBOOLE_0:def 5;

      end;

      

       A5: (((C \ B) \ {x}) \/ B) = (C \/ B)

      proof

        thus (((C \ B) \ {x}) \/ B) c= (C \/ B)

        proof

          let y be object;

          assume y in (((C \ B) \ {x}) \/ B);

          then y in ((C \ B) \ {x}) or y in B by XBOOLE_0:def 3;

          hence thesis by XBOOLE_0:def 3;

        end;

        let y be object;

        assume y in (C \/ B);

        then

         A6: y in ((C \ B) \/ B) by XBOOLE_1: 39;

        per cases by A6, XBOOLE_0:def 3;

          suppose

           A7: y in (C \ B);

          then

           A8: y in C;

           not y in {x}

          proof

            assume y in {x};

            then x in C by A8, TARSKI:def 1;

            hence contradiction by A1, A2;

          end;

          then y in ((C \ B) \ {x}) by A7, XBOOLE_0:def 5;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose y in B;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      set f = (( id A) +* (B --> x));

      (f " {x}) = B by A2, Th17;

      then (f " (C \/ {x})) = ((f " C) \/ B) by RELAT_1: 140;

      hence thesis by A1, A3, A5, Th16;

    end;

    theorem :: FRECHET:19

    

     Th19: for A,B,C,x be set holds C c= A & not x in A implies ((( id A) +* (B --> x)) " (C \ {x})) = (C \ B)

    proof

      let A,B,C,x be set;

      assume that

       A1: C c= A and

       A2: not x in A;

       not x in (C \ B) by A1, A2;

      then (C \ B) misses {x} by ZFMISC_1: 50;

      then ((C \ B) \ {x}) = (C \ B) by XBOOLE_1: 83;

      hence thesis by A1, Th16;

    end;

    begin

    definition

      let T be non empty TopStruct;

      :: FRECHET:def2

      attr T is first-countable means for x be Point of T holds ex B be Basis of x st B is countable;

    end

    theorem :: FRECHET:20

    

     Th20: for M be non empty MetrSpace holds ( TopSpaceMetr M) is first-countable

    proof

      let M be non empty MetrSpace;

      let x be Point of ( TopSpaceMetr M);

      take ( Balls x);

      thus thesis;

    end;

    theorem :: FRECHET:21

     R^1 is first-countable by Th20;

    registration

      cluster R^1 -> first-countable;

      coherence by Th20;

    end

    definition

      let T be TopStruct, S be sequence of T, x be Point of T;

      :: FRECHET:def3

      pred S is_convergent_to x means for U1 be Subset of T st U1 is open & x in U1 holds ex n be Nat st for m be Nat st n <= m holds (S . m) in U1;

    end

    theorem :: FRECHET:22

    

     Th22: for T be non empty TopStruct, x be Point of T, S be sequence of T holds S = ( NAT --> x) implies S is_convergent_to x

    proof

      let T be non empty TopStruct, x be Point of T, S be sequence of T;

      assume

       A1: S = ( NAT --> x);

      let U1 be Subset of T;

      assume that U1 is open and

       A2: x in U1;

      take 0 ;

      let m be Nat;

      m in NAT by ORDINAL1:def 12;

      hence thesis by A1, A2, FUNCOP_1: 7;

    end;

    definition

      let T be TopStruct, S be sequence of T;

      :: FRECHET:def4

      attr S is convergent means ex x be Point of T st S is_convergent_to x;

    end

    definition

      let T be non empty TopStruct, S be sequence of T;

      :: FRECHET:def5

      func Lim S -> Subset of T means

      : Def5: for x be Point of T holds x in it iff S is_convergent_to x;

      existence

      proof

        defpred P[ Element of T] means S is_convergent_to $1;

        { x where x be Element of T : P[x] } is Subset of T from DOMAIN_1:sch 7;

        then

        reconsider X = { x where x be Point of T : P[x] } as Subset of T;

        take X;

        let y be Point of T;

        y in X iff ex x be Point of T st x = y & S is_convergent_to x;

        hence thesis;

      end;

      uniqueness

      proof

        let A,B be Subset of T such that

         A1: for x be Point of T holds x in A iff S is_convergent_to x and

         A2: for x be Point of T holds x in B iff S is_convergent_to x;

        for x be Point of T holds x in A iff x in B by A1, A2;

        hence thesis by SUBSET_1: 3;

      end;

    end

    definition

      let T be non empty TopStruct;

      :: FRECHET:def6

      attr T is Frechet means

      : Def6: for A be Subset of T, x be Point of T st x in ( Cl A) holds ex S be sequence of T st ( rng S) c= A & x in ( Lim S);

    end

    definition

      let T be non empty TopStruct;

      :: FRECHET:def7

      attr T is sequential means for A be Subset of T holds A is closed iff for S be sequence of T st S is convergent & ( rng S) c= A holds ( Lim S) c= A;

    end

    theorem :: FRECHET:23

    

     Th23: for T be non empty TopSpace holds T is first-countable implies T is Frechet

    proof

      let T be non empty TopSpace;

      assume

       A1: T is first-countable;

      let A be Subset of T;

      let x be Point of T such that

       A2: x in ( Cl A);

      consider B be Basis of x such that

       A3: B is countable by A1;

      consider f be sequence of B such that

       A4: ( rng f) = B by A3, CARD_3: 96;

      defpred P[ object, object] means ex D1 be set st D1 = $1 & $2 in (A /\ ( meet (f .: ( succ D1))));

      

       A5: for n be object st n in NAT holds ex y be object st y in the carrier of T & P[n, y]

      proof

        defpred P[ Nat] means ex H be Subset of T st H = ( meet (f .: ( succ $1))) & H is open;

        let n be object;

        

         A6: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          given G be Subset of T such that

           A7: G = ( meet (f .: ( succ n))) and

           A8: G is open;

          (n + 1) in NAT ;

          then

           A9: (n + 1) in ( dom f) by FUNCT_2:def 1;

          

           A10: n in NAT by ORDINAL1:def 12;

          n in ( succ n) & ( dom f) = NAT by FUNCT_2:def 1, ORDINAL1: 6;

          then

           A11: (f . n) in (f .: ( succ n)) by FUNCT_1:def 6, A10;

          (f . (n + 1)) in B;

          then

          consider H1 be Subset of T such that

           A12: H1 = (f . (n + 1));

          

           A13: H1 is open by A12, YELLOW_8: 12;

          consider H be Subset of T such that

           A14: H = (H1 /\ G);

          take H;

          ( meet (f .: ( succ (n + 1)))) = ( meet (f .: ( {(n + 1)} \/ ( Segm (n + 1)))))

          .= ( meet (f .: ( {(n + 1)} \/ ( succ ( Segm n))))) by NAT_1: 38

          .= ( meet (( Im (f,(n + 1))) \/ (f .: ( succ n)))) by RELAT_1: 120

          .= ( meet ( {(f . (n + 1))} \/ (f .: ( succ n)))) by A9, FUNCT_1: 59

          .= (( meet {(f . (n + 1))}) /\ ( meet (f .: ( succ n)))) by A11, SETFAM_1: 9

          .= H by A7, A12, A14, SETFAM_1: 10;

          hence thesis by A8, A13, A14, TOPS_1: 11;

        end;

        assume n in NAT ;

        then

        reconsider n as Element of NAT ;

        

         A15: P[ 0 ]

        proof

          (f . 0 ) in B;

          then

          reconsider H = (f . 0 ) as Subset of T;

          take H;

           0 in NAT ;

          then 0 in ( dom f) by FUNCT_2:def 1;

          

          then ( meet ( Im (f, 0 ))) = ( meet {(f . 0 )}) by FUNCT_1: 59

          .= H by SETFAM_1: 10;

          hence thesis by YELLOW_8: 12;

        end;

        for n be Nat holds P[n] from NAT_1:sch 2( A15, A6);

        then

         A16: ex H be Subset of T st H = ( meet (f .: ( succ n))) & H is open;

        

         A17: for G be set st G in (f .: ( succ n)) holds x in G

        proof

          let G be set;

          assume G in (f .: ( succ n));

          then

          consider k be object such that

           A18: k in ( dom f) and k in ( succ n) and

           A19: G = (f . k) by FUNCT_1:def 6;

          (f . k) in B by A18, FUNCT_2: 5;

          hence thesis by A19, YELLOW_8: 12;

        end;

        n in ( succ n) & ( dom f) = NAT by FUNCT_2:def 1, ORDINAL1: 6;

        then (f . n) in (f .: ( succ n)) by FUNCT_1:def 6;

        then x in ( meet (f .: ( succ n))) by A17, SETFAM_1:def 1;

        then A meets ( meet (f .: ( succ n))) by A2, A16, PRE_TOPC:def 7;

        then

        consider y be object such that

         A20: y in (A /\ ( meet (f .: ( succ n)))) by XBOOLE_0: 4;

        take y;

        thus thesis by A20;

      end;

      consider S be Function such that

       A21: ( dom S) = NAT & ( rng S) c= the carrier of T & for n be object st n in NAT holds P[n, (S . n)] from FUNCT_1:sch 6( A5);

      

       A22: ( rng S) c= A

      proof

        let y be object;

        assume y in ( rng S);

        then

        consider a be object such that

         A23: a in ( dom S) & y = (S . a) by FUNCT_1:def 3;

        reconsider a as set by TARSKI: 1;

         P[a, (S . a)] by A21, A23;

        then y in (A /\ ( meet (f .: ( succ a)))) by A23;

        hence thesis by XBOOLE_0:def 4;

      end;

      reconsider S as sequence of T by A21, FUNCT_2:def 1, RELSET_1: 4;

      

       A24: for m,n be Nat st n <= m holds (A /\ ( meet (f .: ( succ m)))) c= (A /\ ( meet (f .: ( succ n))))

      proof

        let m,n be Nat;

        assume n <= m;

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

        then ( Segm (n + 1)) c= ( Segm (m + 1)) by NAT_1: 39;

        then ( succ ( Segm n)) c= ( Segm (m + 1)) by NAT_1: 38;

        then ( succ ( Segm n)) c= ( succ ( Segm m)) by NAT_1: 38;

        then

         A25: (f .: ( succ n)) c= (f .: ( succ m)) by RELAT_1: 123;

        

         A26: n in NAT by ORDINAL1:def 12;

        n in ( succ n) & ( dom f) = NAT by FUNCT_2:def 1, ORDINAL1: 6;

        then (f . n) in (f .: ( succ n)) by FUNCT_1:def 6, A26;

        then ( meet (f .: ( succ m))) c= ( meet (f .: ( succ n))) by A25, SETFAM_1: 6;

        hence thesis by XBOOLE_1: 26;

      end;

      S is_convergent_to x

      proof

        let U1 be Subset of T;

        assume

         A27: U1 is open & x in U1;

        reconsider U1 as Subset of T;

        consider U2 be Subset of T such that

         A28: U2 in B and

         A29: U2 c= U1 by A27, YELLOW_8: 13;

        consider n be object such that

         A30: n in ( dom f) and

         A31: U2 = (f . n) by A4, A28, FUNCT_1:def 3;

        reconsider n as Element of NAT by A30;

        for m be Nat st n <= m holds (S . m) in U1

        proof

          let m be Nat;

          

           A32: m in NAT by ORDINAL1:def 12;

          n in ( succ n) & ( dom f) = NAT by FUNCT_2:def 1, ORDINAL1: 6;

          then

           A33: (f . n) in (f .: ( succ n)) by FUNCT_1:def 6;

          assume n <= m;

          then

           A34: (A /\ ( meet (f .: ( succ m)))) c= (A /\ ( meet (f .: ( succ n)))) by A24;

           P[m, (S . m)] by A21, A32;

          then (S . m) in (A /\ ( meet (f .: ( succ m))));

          then (S . m) in ( meet (f .: ( succ n))) by A34, XBOOLE_0:def 4;

          then (S . m) in (f . n) by A33, SETFAM_1:def 1;

          hence thesis by A29, A31;

        end;

        hence thesis;

      end;

      then x in ( Lim S) by Def5;

      hence thesis by A22;

    end;

    registration

      cluster first-countable -> Frechet for non empty TopSpace;

      coherence by Th23;

    end

    theorem :: FRECHET:24

    

     Th24: for T be non empty TopSpace, A be Subset of T holds A is closed implies for S be sequence of T st ( rng S) c= A holds ( Lim S) c= A

    proof

      let T be non empty TopSpace, A be Subset of T;

      assume

       A1: A is closed;

      let S be sequence of T such that

       A2: ( rng S) c= A;

      thus ( Lim S) c= A

      proof

        reconsider A as Subset of T;

        reconsider L = ( Lim S) as Subset of T;

        L c= A

        proof

          let y be object;

          assume

           A3: y in L;

          then

          reconsider p = y as Point of T;

          

           A4: S is_convergent_to p by A3, Def5;

          for U1 be Subset of T st U1 is open holds p in U1 implies A meets U1

          proof

            let U1 be Subset of T;

            assume

             A5: U1 is open;

            reconsider U2 = U1 as Subset of T;

            assume p in U1;

            then

            consider n be Nat such that

             A6: for m be Nat st n <= m holds (S . m) in U2 by A4, A5;

            

             A7: n in NAT by ORDINAL1:def 12;

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

            then

             A8: (S . n) in ( rng S) by FUNCT_1:def 3, A7;

            (S . n) in U1 by A6;

            then (S . n) in (A /\ U1) by A2, A8, XBOOLE_0:def 4;

            hence thesis;

          end;

          then p in ( Cl A) by PRE_TOPC:def 7;

          hence thesis by A1, PRE_TOPC: 22;

        end;

        hence thesis;

      end;

    end;

    theorem :: FRECHET:25

    

     Th25: for T be non empty TopSpace holds (for A be Subset of T holds (for S be sequence of T st S is convergent & ( rng S) c= A holds ( Lim S) c= A) implies A is closed) implies T is sequential by Th24;

    theorem :: FRECHET:26

    

     Th26: for T be non empty TopSpace holds T is Frechet implies T is sequential

    proof

      let T be non empty TopSpace;

      assume

       A1: T is Frechet;

      for A be Subset of T holds (for S be sequence of T st S is convergent & ( rng S) c= A holds ( Lim S) c= A) implies A is closed

      proof

        let A be Subset of T;

        assume

         A2: for S be sequence of T st S is convergent & ( rng S) c= A holds ( Lim S) c= A;

        

         A3: ( Cl A) c= A

        proof

          let x be object;

          assume

           A4: x in ( Cl A);

          then

          reconsider p = x as Point of T;

          consider S be sequence of T such that

           A5: ( rng S) c= A and

           A6: p in ( Lim S) by A1, A4;

          S is_convergent_to p by A6, Def5;

          then S is convergent;

          then ( Lim S) c= A by A2, A5;

          hence thesis by A6;

        end;

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

        then A = ( Cl A) by A3;

        hence thesis by PRE_TOPC: 22;

      end;

      hence thesis by Th25;

    end;

    registration

      cluster Frechet -> sequential for non empty TopSpace;

      coherence by Th26;

    end

    begin

    definition

      :: FRECHET:def8

      func REAL? -> strict non empty TopSpace means

      : Def8: the carrier of it = (( REAL \ NAT ) \/ { REAL }) & ex f be Function of R^1 , it st f = (( id REAL ) +* ( NAT --> REAL )) & for A be Subset of it holds A is closed iff (f " A) is closed;

      existence

      proof

        set f = (( id REAL ) +* ( NAT --> REAL ));

        reconsider X = (( REAL \ NAT ) \/ { REAL }) as non empty set;

        

         A1: ( rng f) c= (( REAL \ NAT ) \/ { REAL }) by Th15;

        ( REAL \/ NAT ) = REAL by XBOOLE_1: 12, NUMBERS: 19;

        then ( dom f) = the carrier of R^1 by Th14, TOPMETR: 17;

        then

        reconsider f as Function of the carrier of R^1 , X by A1, FUNCT_2: 2;

        set O = { (X \ A) where A be Subset of X : ex fA be Subset of R^1 st fA = (f " A) & fA is closed };

        O c= ( bool X)

        proof

          let B be object;

          assume B in O;

          then ex A be Subset of X st B = (X \ A) & ex fA be Subset of R^1 st fA = (f " A) & fA is closed;

          hence thesis;

        end;

        then

        reconsider O as Subset-Family of X;

        set T = TopStruct (# X, O #);

        reconsider f as Function of R^1 , T;

        

         A2: for A be Subset of T holds A is closed iff (f " A) is closed

        proof

          let A be Subset of T;

          thus A is closed implies (f " A) is closed

          proof

            assume A is closed;

            then (( [#] T) \ A) is open by PRE_TOPC:def 3;

            then (( [#] T) \ A) in the topology of T by PRE_TOPC:def 2;

            then

            consider B be Subset of X such that

             A3: (X \ B) = (( [#] T) \ A) and

             A4: ex fA be Subset of R^1 st fA = (f " B) & fA is closed;

            B = (( [#] T) \ (( [#] T) \ A)) by A3, PRE_TOPC: 3;

            hence thesis by A4, PRE_TOPC: 3;

          end;

          assume (f " A) is closed;

          then (X \ A) in O;

          then (( [#] T) \ A) is open by PRE_TOPC:def 2;

          hence thesis by PRE_TOPC:def 3;

        end;

        then

        reconsider T as strict non empty TopSpace by Th6;

        take T;

        thus the carrier of T = (( REAL \ NAT ) \/ { REAL });

        reconsider f as Function of R^1 , T;

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let X,Y be strict non empty TopSpace such that

         A5: the carrier of X = (( REAL \ NAT ) \/ { REAL }) and

         A6: ex f be Function of R^1 , X st f = (( id REAL ) +* ( NAT --> REAL )) & for A be Subset of X holds A is closed iff (f " A) is closed and

         A7: the carrier of Y = (( REAL \ NAT ) \/ { REAL }) and

         A8: ex f be Function of R^1 , Y st f = (( id REAL ) +* ( NAT --> REAL )) & for A be Subset of Y holds A is closed iff (f " A) is closed;

        consider g be Function of R^1 , Y such that

         A9: g = (( id REAL ) +* ( NAT --> REAL )) and

         A10: for A be Subset of Y holds A is closed iff (g " A) is closed by A8;

        consider f be Function of R^1 , X such that

         A11: f = (( id REAL ) +* ( NAT --> REAL )) and

         A12: for A be Subset of X holds A is closed iff (f " A) is closed by A6;

        

         A13: the topology of Y c= the topology of X

        proof

          let V be object;

          assume

           A14: V in the topology of Y;

          then

          reconsider V1 = V as Subset of Y;

          reconsider V2 = V as Subset of X by A5, A7, A14;

          reconsider V1 as Subset of Y;

          reconsider V2 as Subset of X;

          V1 is open by A14, PRE_TOPC:def 2;

          then (( [#] Y) \ V1) is closed by Lm2;

          then (f " (( [#] Y) \ V1)) is closed by A11, A9, A10;

          then (( [#] X) \ V2) is closed by A5, A7, A12;

          then V2 is open by Lm2;

          hence thesis by PRE_TOPC:def 2;

        end;

        the topology of X c= the topology of Y

        proof

          let V be object;

          assume

           A15: V in the topology of X;

          then

          reconsider V1 = V as Subset of X;

          reconsider V2 = V as Subset of Y by A5, A7, A15;

          reconsider V1 as Subset of X;

          reconsider V2 as Subset of Y;

          V1 is open by A15, PRE_TOPC:def 2;

          then (( [#] X) \ V1) is closed by Lm2;

          then (g " (( [#] X) \ V1)) is closed by A11, A12, A9;

          then (( [#] Y) \ V2) is closed by A5, A7, A10;

          then V2 is open by Lm2;

          hence thesis by PRE_TOPC:def 2;

        end;

        hence thesis by A5, A7, A13, XBOOLE_0:def 10;

      end;

    end

    

     Lm3: { REAL } c= the carrier of REAL?

    proof

      let x be object;

      assume x in { REAL };

      then x in (( REAL \ NAT ) \/ { REAL }) by XBOOLE_0:def 3;

      hence thesis by Def8;

    end;

    theorem :: FRECHET:27

    

     Th27: REAL is Point of REAL?

    proof

       REAL in { REAL } by TARSKI:def 1;

      hence thesis by Lm3;

    end;

    theorem :: FRECHET:28

    

     Th28: for A be Subset of REAL? holds A is open & REAL in A iff ex O be Subset of R^1 st O is open & NAT c= O & A = ((O \ NAT ) \/ { REAL })

    proof

      let A be Subset of REAL? ;

      consider f be Function of R^1 , REAL? such that

       A1: f = (( id REAL ) +* ( NAT --> REAL )) and

       A2: for A be Subset of REAL? holds A is closed iff (f " A) is closed by Def8;

      thus A is open & REAL in A implies ex O be Subset of R^1 st O is open & NAT c= O & A = ((O \ NAT ) \/ { REAL })

      proof

        assume that

         A3: A is open and

         A4: REAL in A;

        consider O be Subset of R^1 such that

         A5: O = ((f " (A ` )) ` );

        (A ` ) is closed by A3, TOPS_1: 4;

        then (f " (A ` )) is closed by A2;

        then

         A6: ((f " (A ` )) ` ) is open by TOPS_1: 3;

        

         A7: not REAL in (( [#] REAL? ) \ A) by A4, XBOOLE_0:def 5;

        

         A8: (A ` ) c= ((A ` ) \ { REAL })

        proof

          let x be object;

          assume

           A9: x in (A ` );

          then not x in { REAL } by A7, TARSKI:def 1;

          hence thesis by A9, XBOOLE_0:def 5;

        end;

        (A ` ) c= the carrier of REAL? ;

        then

         A10: (A ` ) c= (( REAL \ NAT ) \/ { REAL }) by Def8;

        

         A11: (A ` ) c= ( REAL \ NAT )

        proof

          let x be object;

          assume

           A12: x in (A ` );

          then x in ( REAL \ NAT ) or x in { REAL } by A10, XBOOLE_0:def 3;

          hence thesis by A7, A12, TARSKI:def 1;

        end;

        ((A ` ) \ { REAL }) c= (A ` ) by XBOOLE_1: 36;

        then

         A13: (A ` ) = ((A ` ) \ { REAL }) by A8;

         not REAL in REAL ;

        then ((( id REAL ) +* ( NAT --> REAL )) " ((A ` ) \ { REAL })) = ((A ` ) \ NAT ) by A11, Th19, XBOOLE_1: 1;

        then O = ((( [#] R^1 ) \ (A ` )) \/ ( NAT /\ ( [#] R^1 ))) by A1, A5, A13, XBOOLE_1: 52;

        then

         A14: O = ((( [#] R^1 ) \ (A ` )) \/ NAT ) by TOPMETR: 17, XBOOLE_1: 28, NUMBERS: 19;

        A = ((A ` ) ` )

        .= (the carrier of REAL? \ (A ` ));

        then

         A15: A = ((( REAL \ NAT ) \/ { REAL }) \ (A ` )) by Def8;

        

         A16: A = ((( REAL \ (A ` )) \ NAT ) \/ { REAL })

        proof

          thus A c= ((( REAL \ (A ` )) \ NAT ) \/ { REAL })

          proof

            let x be object;

            assume

             A17: x in A;

            then

             A18: not x in (A ` ) by XBOOLE_0:def 5;

            x in ( REAL \ NAT ) or x in { REAL } by A15, A17, XBOOLE_0:def 3;

            then x in ( REAL \ (A ` )) & not x in NAT or x in { REAL } by A18, XBOOLE_0:def 5;

            then x in (( REAL \ (A ` )) \ NAT ) or x in { REAL } by XBOOLE_0:def 5;

            hence thesis by XBOOLE_0:def 3;

          end;

          let x be object;

          assume x in ((( REAL \ (A ` )) \ NAT ) \/ { REAL });

          then x in (( REAL \ (A ` )) \ NAT ) or x in { REAL } by XBOOLE_0:def 3;

          then

           A19: x in ( REAL \ (A ` )) & not x in NAT or x in { REAL } & not x in (A ` ) by A7, TARSKI:def 1, XBOOLE_0:def 5;

          then x in ( REAL \ NAT ) or x in { REAL } by XBOOLE_0:def 5;

          then

           A20: x in (( REAL \ NAT ) \/ { REAL }) by XBOOLE_0:def 3;

           not x in (A ` ) by A19, XBOOLE_0:def 5;

          hence thesis by A15, A20, XBOOLE_0:def 5;

        end;

         NAT c= ( REAL \ (A ` ))

        proof

          let x be object;

          assume

           A21: x in NAT ;

          then not x in (A ` ) by A11, XBOOLE_0:def 5;

          hence thesis by A21, XBOOLE_0:def 5, NUMBERS: 19;

        end;

        then O = ( REAL \ (A ` )) by A14, TOPMETR: 17, XBOOLE_1: 12;

        hence thesis by A5, A6, A14, A16, XBOOLE_1: 7;

      end;

      given O be Subset of R^1 such that

       A22: O is open and

       A23: NAT c= O and

       A24: A = ((O \ NAT ) \/ { REAL });

      consider B be Subset of R^1 such that

       A25: B = (( [#] R^1 ) \ O);

       not REAL in REAL ;

      then ((( id REAL ) +* ( NAT --> REAL )) " (( REAL \ O) \ { REAL })) = (( REAL \ O) \ NAT ) by Th19;

      then

       A26: (f " (( REAL \ O) \ { REAL })) = ( REAL \ (O \/ NAT )) by A1, XBOOLE_1: 41;

      

       A27: B is closed by A22, A25, Lm2;

      (A ` ) = ((( REAL \ NAT ) \/ { REAL }) \ ((O \ NAT ) \/ { REAL })) by A24, Def8

      .= ((( REAL \ NAT ) \ ((O \ NAT ) \/ { REAL })) \/ ( { REAL } \ ( { REAL } \/ (O \ NAT )))) by XBOOLE_1: 42

      .= ((( REAL \ NAT ) \ ((O \ NAT ) \/ { REAL })) \/ {} ) by XBOOLE_1: 46

      .= ((( REAL \ NAT ) \ (O \ NAT )) \ { REAL }) by XBOOLE_1: 41

      .= (( REAL \ ( NAT \/ (O \ NAT ))) \ { REAL }) by XBOOLE_1: 41

      .= (( REAL \ ( NAT \/ O)) \ { REAL }) by XBOOLE_1: 39

      .= (( REAL \ O) \ { REAL }) by A23, XBOOLE_1: 12;

      then (f " (A ` )) = B by A23, A25, A26, TOPMETR: 17, XBOOLE_1: 12;

      then (( [#] REAL? ) \ A) is closed by A2, A27;

      hence A is open by Lm2;

       REAL in { REAL } by TARSKI:def 1;

      hence thesis by A24, XBOOLE_0:def 3;

    end;

    theorem :: FRECHET:29

    

     Th29: for A be set holds A is Subset of REAL? & not REAL in A iff A is Subset of R^1 & ( NAT /\ A) = {}

    proof

      let A be set;

      thus A is Subset of REAL? & not REAL in A implies A is Subset of R^1 & ( NAT /\ A) = {}

      proof

        assume that

         A1: A is Subset of REAL? and

         A2: not REAL in A;

        A c= the carrier of REAL? by A1;

        then

         A3: A c= (( REAL \ NAT ) \/ { REAL }) by Def8;

        A c= REAL

        proof

          let x be object;

          assume

           A4: x in A;

          then x in ( REAL \ NAT ) or x in { REAL } by A3, XBOOLE_0:def 3;

          hence thesis by A2, A4, TARSKI:def 1;

        end;

        hence A is Subset of R^1 by TOPMETR: 17;

        thus ( NAT /\ A) = {}

        proof

          set x = the Element of ( NAT /\ A);

          assume

           A5: ( NAT /\ A) <> {} ;

          then

           A6: x in NAT by XBOOLE_0:def 4;

          

           A7: x in A by A5, XBOOLE_0:def 4;

          per cases by A3, A7, XBOOLE_0:def 3;

            suppose x in ( REAL \ NAT );

            hence contradiction by A6, XBOOLE_0:def 5;

          end;

            suppose x in { REAL };

            then x = REAL by TARSKI:def 1;

            then REAL in REAL by A6, NUMBERS: 19;

            hence contradiction;

          end;

        end;

      end;

      assume that

       A8: A is Subset of R^1 and

       A9: ( NAT /\ A) = {} ;

      

       A10: A c= ( REAL \ NAT )

      proof

        let x be object;

        assume

         A11: x in A;

        then not x in NAT by A9, XBOOLE_0:def 4;

        hence thesis by A8, A11, TOPMETR: 17, XBOOLE_0:def 5;

      end;

      ( REAL \ NAT ) c= (( REAL \ NAT ) \/ { REAL }) by XBOOLE_1: 7;

      then A c= (( REAL \ NAT ) \/ { REAL }) by A10;

      hence A is Subset of REAL? by Def8;

      thus not REAL in A

      proof

        assume REAL in A;

        then REAL in REAL by A8, TOPMETR: 17;

        hence contradiction;

      end;

    end;

    theorem :: FRECHET:30

    

     Th30: for A be Subset of R^1 , B be Subset of REAL? st A = B holds ( NAT /\ A) = {} & A is open iff not REAL in B & B is open

    proof

      let A be Subset of R^1 , B be Subset of REAL? ;

      consider f be Function of R^1 , REAL? such that

       A1: f = (( id REAL ) +* ( NAT --> REAL )) and

       A2: for A be Subset of REAL? holds A is closed iff (f " A) is closed by Def8;

      assume

       A3: A = B;

      

       A4: ( NAT /\ A) = {} & not REAL in B implies (f " (B ` )) = (A ` )

      proof

        assume that

         A5: ( NAT /\ A) = {} and

         A6: not REAL in B;

        

         A7: ( REAL \ A) = ((((( REAL \ NAT ) \/ { REAL }) \ A) \ { REAL }) \/ NAT )

        proof

          thus ( REAL \ A) c= ((((( REAL \ NAT ) \/ { REAL }) \ A) \ { REAL }) \/ NAT )

          proof

            let x be object;

            assume

             A8: x in ( REAL \ A);

            then

             A9: not x in A by XBOOLE_0:def 5;

            

             A10: x in REAL by A8;

            

             A11: not x in { REAL }

            proof

              assume x in { REAL };

              then

               A: x = REAL by TARSKI:def 1;

              reconsider xx = x as set by TARSKI: 1;

               not xx in xx;

              hence contradiction by A, A10;

            end;

            per cases ;

              suppose x in NAT ;

              hence thesis by XBOOLE_0:def 3;

            end;

              suppose not x in NAT ;

              then x in ( REAL \ NAT ) by A8, XBOOLE_0:def 5;

              then x in (( REAL \ NAT ) \/ { REAL }) by XBOOLE_0:def 3;

              then x in ((( REAL \ NAT ) \/ { REAL }) \ A) by A9, XBOOLE_0:def 5;

              then x in (((( REAL \ NAT ) \/ { REAL }) \ A) \ { REAL }) by A11, XBOOLE_0:def 5;

              hence thesis by XBOOLE_0:def 3;

            end;

          end;

          let x be object;

          assume

           A12: x in ((((( REAL \ NAT ) \/ { REAL }) \ A) \ { REAL }) \/ NAT );

          per cases by A12, XBOOLE_0:def 3;

            suppose

             A13: x in NAT ;

            then not x in A by A5, XBOOLE_0:def 4;

            hence thesis by A13, XBOOLE_0:def 5, NUMBERS: 19;

          end;

            suppose

             A14: x in (((( REAL \ NAT ) \/ { REAL }) \ A) \ { REAL });

            then x in ((( REAL \ NAT ) \/ { REAL }) \ A) by XBOOLE_0:def 5;

            then

             A15: not x in A by XBOOLE_0:def 5;

            x in ( REAL \ NAT ) or x in { REAL } by A14, XBOOLE_0:def 3;

            hence thesis by A14, A15, XBOOLE_0:def 5;

          end;

        end;

        (B ` ) c= the carrier of REAL? ;

        then

         A16: (B ` ) c= (( REAL \ NAT ) \/ { REAL }) by Def8;

        

         A17: ((B ` ) \ { REAL }) c= REAL

        proof

          let x be object;

          assume

           A18: x in ((B ` ) \ { REAL });

          then x in (B ` ) by XBOOLE_0:def 5;

          then x in ( REAL \ NAT ) or x in { REAL } by A16, XBOOLE_0:def 3;

          hence thesis by A18, XBOOLE_0:def 5;

        end;

        

         A19: REAL in (( [#] REAL? ) \ B) by A6, Th27, XBOOLE_0:def 5;

         { REAL } c= (B ` ) by A19, TARSKI:def 1;

        then ( not REAL in REAL ) & (B ` ) = (((B ` ) \ { REAL }) \/ { REAL }) by XBOOLE_1: 45;

        

        then ((( id REAL ) +* ( NAT --> REAL )) " (B ` )) = (((( [#] REAL? ) \ B) \ { REAL }) \/ NAT ) by A17, Th18

        .= ((((( REAL \ NAT ) \/ { REAL }) \ A) \ { REAL }) \/ NAT ) by A3, Def8;

        hence thesis by A1, A7, TOPMETR: 17;

      end;

      thus ( NAT /\ A) = {} & A is open implies not REAL in B & B is open

      proof

        assume that

         A20: ( NAT /\ A) = {} and

         A21: A is open;

        thus not REAL in B by A3, A20, Th29;

        (A ` ) is closed by A21, TOPS_1: 4;

        then (B ` ) is closed by A3, A2, A4, A20, Th29;

        hence thesis by TOPS_1: 4;

      end;

      assume that

       A22: not REAL in B and

       A23: B is open;

      thus ( NAT /\ A) = {} by A3, A22, Th29;

      (B ` ) is closed by A23, TOPS_1: 4;

      then (A ` ) is closed by A3, A2, A4, A22, Th29;

      hence thesis by TOPS_1: 4;

    end;

    theorem :: FRECHET:31

    

     Th31: for A be Subset of REAL? st A = { REAL } holds A is closed

    proof

      reconsider B = ( REAL \ NAT ) as Subset of R^1 by TOPMETR: 17;

      let A be Subset of REAL? ;

      reconsider B as Subset of R^1 ;

      

       A1: ( REAL \ NAT ) = ((( REAL \ NAT ) \/ { REAL }) \ { REAL })

      proof

        thus ( REAL \ NAT ) c= ((( REAL \ NAT ) \/ { REAL }) \ { REAL })

        proof

          let x be object;

          assume

           A2: x in ( REAL \ NAT );

          then

           A3: x in REAL ;

          

           A4: not x in { REAL }

          proof

            assume x in { REAL };

            then

             A: x = REAL by TARSKI:def 1;

            reconsider xx = x as set by TARSKI: 1;

             not xx in xx;

            hence contradiction by A, A3;

          end;

          x in (( REAL \ NAT ) \/ { REAL }) by A2, XBOOLE_0:def 3;

          hence thesis by A4, XBOOLE_0:def 5;

        end;

        let x be object;

        assume

         A5: x in ((( REAL \ NAT ) \/ { REAL }) \ { REAL });

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

        hence thesis by A5, XBOOLE_0:def 3;

      end;

      B misses NAT by XBOOLE_1: 79;

      then

       A6: (B /\ NAT ) = {} ;

      then

      reconsider C = B as Subset of REAL? by Th29;

      assume A = { REAL };

      then

       A7: C = (A ` ) by A1, Def8;

      B is open

      proof

        reconsider N = NAT as Subset of R^1 by TOPMETR: 17, NUMBERS: 19;

        reconsider N as Subset of R^1 ;

        N is closed & (N ` ) = B by Th10, TOPMETR: 17;

        hence thesis by TOPS_1: 3;

      end;

      then C is open by A6, Th30;

      hence thesis by A7, TOPS_1: 3;

    end;

    theorem :: FRECHET:32

    

     Th32: not REAL? is first-countable

    proof

      reconsider y = REAL as Point of REAL? by Th27;

      assume REAL? is first-countable;

      then

      consider B be Basis of y such that

       A1: B is countable;

      consider h be sequence of B such that

       A2: ( rng h) = B by A1, CARD_3: 96;

      defpred P[ object, object] means ex m be Element of NAT st m = $1 & $2 in ((h . $1) /\ ].(m - (1 / 4)), (m + (1 / 4)).[);

      

       A3: for n be object st n in NAT holds ex x be object st x in ( REAL \ NAT ) & P[n, x]

      proof

        let n be object;

        assume

         A4: n in NAT ;

        then

        reconsider m = n as Element of NAT ;

        n in ( dom h) by A4, FUNCT_2:def 1;

        then

         A5: (h . n) in ( rng h) by FUNCT_1:def 3;

        then

        reconsider Bn = (h . n) as Subset of REAL? by A2;

        m in REAL by XREAL_0:def 1;

        then

        reconsider m9 = m as Point of RealSpace by METRIC_1:def 13;

        reconsider Kn = ( Ball (m9,(1 / 4))) as Subset of R^1 by TOPMETR: 12;

        reconsider Bn as Subset of REAL? ;

        Bn is open & y in Bn by A5, YELLOW_8: 12;

        then

        consider An be Subset of R^1 such that

         A6: An is open and

         A7: NAT c= An and

         A8: Bn = ((An \ NAT ) \/ { REAL }) by Th28;

        reconsider An9 = An as Subset of R^1 ;

        Kn is open by TOPMETR: 14;

        then

         A9: (An9 /\ Kn) is open by A6, TOPS_1: 11;

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

        then m9 in ( Ball (m9,(1 / 4))) by METRIC_1: 11;

        then n in (An /\ ( Ball (m9,(1 / 4)))) by A4, A7, XBOOLE_0:def 4;

        then

        consider r be Real such that

         A10: r > 0 and

         A11: ( Ball (m9,r)) c= (An /\ Kn) by A9, TOPMETR: 15;

        reconsider r as Real;

        m < (m + r) by A10, XREAL_1: 29;

        then (m - r) < m by XREAL_1: 19;

        then

        consider x be Real such that

         A12: (m - r) < x and

         A13: x < m by XREAL_1: 5;

        reconsider x as Element of REAL by XREAL_0:def 1;

        take x;

        

         A14: r < 1

        proof

          assume r >= 1;

          then (1 / 2) < r by XXREAL_0: 2;

          then ( - r) < ( - (1 / 2)) by XREAL_1: 24;

          then

           A15: (( - r) + m) < (( - (1 / 2)) + m) by XREAL_1: 6;

          (( - (1 / 2)) + m) < (r + m) by A10, XREAL_1: 6;

          then (m - (1 / 2)) in { a where a be Real : (m - r) < a & a < (m + r) } by A15;

          then (m - (1 / 2)) in ].(m - r), (m + r).[ by RCOMP_1:def 2;

          then (m - (1 / 2)) in ( Ball (m9,r)) by Th7;

          then (m - (1 / 2)) in Kn by A11, XBOOLE_0:def 4;

          then (m - (1 / 2)) in ].(m - (1 / 4)), (m + (1 / 4)).[ by Th7;

          then (m - (1 / 2)) in { a where a be Real : (m - (1 / 4)) < a & a < (m + (1 / 4)) } by RCOMP_1:def 2;

          then ex a be Real st a = (m - (1 / 2)) & (m - (1 / 4)) < a & a < (m + (1 / 4));

          hence contradiction by XREAL_1: 6;

        end;

        

         A16: not x in NAT

        proof

          assume x in NAT ;

          then

          reconsider x as Element of NAT ;

          per cases by XXREAL_0: 1;

            suppose x = m;

            hence contradiction by A13;

          end;

            suppose x > m;

            hence contradiction by A13;

          end;

            suppose

             A17: x < m;

            m < (x + r) by A12, XREAL_1: 19;

            then (m - x) < r by XREAL_1: 19;

            then

             A18: (m - x) < 1 by A14, XXREAL_0: 2;

            m >= (x + 1) by A17, NAT_1: 13;

            hence contradiction by A18, XREAL_1: 19;

          end;

        end;

        hence x in ( REAL \ NAT ) by XBOOLE_0:def 5;

        (x + 0 ) < (m + r) by A10, A13, XREAL_1: 8;

        then x in { a where a be Real : (m - r) < a & a < (m + r) } by A12;

        then x in ].(m - r), (m + r).[ by RCOMP_1:def 2;

        then

         A19: x in ( Ball (m9,r)) by Th7;

        then x in An by A11, XBOOLE_0:def 4;

        then x in (An \ NAT ) by A16, XBOOLE_0:def 5;

        then

         A20: x in Bn by A8, XBOOLE_0:def 3;

        take m;

        ( Ball (m9,(1 / 4))) = ].(m - (1 / 4)), (m + (1 / 4)).[ by Th7;

        then x in ].(m - (1 / 4)), (m + (1 / 4)).[ by A11, A19, XBOOLE_0:def 4;

        hence thesis by A20, XBOOLE_0:def 4;

      end;

      consider S be Function such that

       A21: ( dom S) = NAT and

       A22: ( rng S) c= ( REAL \ NAT ) and

       A23: for n be object st n in NAT holds P[n, (S . n)] from FUNCT_1:sch 6( A3);

      reconsider S as sequence of R^1 by A21, A22, FUNCT_2: 2, TOPMETR: 17, XBOOLE_1: 1;

      reconsider O = ( rng S) as Subset of R^1 ;

      for n be Element of NAT holds (S . n) in ].(n - (1 / 4)), (n + (1 / 4)).[

      proof

        let n be Element of NAT ;

        ex m be Element of NAT st m = n & (S . n) in ((h . n) /\ ].(m - (1 / 4)), (m + (1 / 4)).[) by A23;

        hence thesis by XBOOLE_0:def 4;

      end;

      then O is closed by Th9;

      then

       A24: (( [#] R^1 ) \ O) is open by PRE_TOPC:def 3;

      set A = (((O ` ) \ NAT ) \/ { REAL });

      A c= (( REAL \ NAT ) \/ { REAL })

      proof

        let x be object;

        assume x in A;

        then x in ((O ` ) \ NAT ) or x in { REAL } by XBOOLE_0:def 3;

        then x in (O ` ) & not x in NAT or x in { REAL } by XBOOLE_0:def 5;

        then x in ( REAL \ NAT ) or x in { REAL } by TOPMETR: 17, XBOOLE_0:def 5;

        hence thesis by XBOOLE_0:def 3;

      end;

      then

      reconsider A as Subset of REAL? by Def8;

      reconsider A as Subset of REAL? ;

       NAT c= (O ` )

      proof

        let x be object;

        assume

         A25: x in NAT ;

        then not x in ( rng S) by A22, XBOOLE_0:def 5;

        hence thesis by A25, TOPMETR: 17, XBOOLE_0:def 5, NUMBERS: 19;

      end;

      then A is open & REAL in A by A24, Th28;

      then

      consider V be Subset of REAL? such that

       A26: V in B and

       A27: V c= A by YELLOW_8: 13;

      consider n1 be object such that

       A28: n1 in ( dom h) and

       A29: V = (h . n1) by A2, A26, FUNCT_1:def 3;

      reconsider n = n1 as Element of NAT by A28;

      for n be Element of NAT holds ex x be set st x in (h . n) & not x in A

      proof

        let n be Element of NAT ;

        consider xn be set such that

         A30: xn = (S . n);

        take xn;

        

         A31: (S . n) in ( rng S) by A21, FUNCT_1:def 3;

        then not xn in (( [#] R^1 ) \ O) by A30, XBOOLE_0:def 5;

        then

         A32: not xn in ((O ` ) \ NAT ) by XBOOLE_0:def 5;

         not xn = REAL

        proof

          assume xn = REAL ;

          then REAL in REAL by A22, A30, A31, XBOOLE_0:def 5;

          hence contradiction;

        end;

        then

         A33: not xn in { REAL } by TARSKI:def 1;

        ex m be Element of NAT st m = n & (S . n) in ((h . n) /\ ].(m - (1 / 4)), (m + (1 / 4)).[) by A23;

        hence thesis by A30, A32, A33, XBOOLE_0:def 3, XBOOLE_0:def 4;

      end;

      then ex x be set st x in (h . n) & not x in A;

      hence contradiction by A27, A29;

    end;

    theorem :: FRECHET:33

    

     Th33: REAL? is Frechet

    proof

      let A be Subset of REAL? , x be Point of REAL? ;

      assume

       A1: x in ( Cl A);

      x in the carrier of REAL? ;

      then x in (( REAL \ NAT ) \/ { REAL }) by Def8;

      then

       A2: x in ( REAL \ NAT ) or x in { REAL } by XBOOLE_0:def 3;

      per cases by A2, TARSKI:def 1;

        suppose

         A3: x in ( REAL \ NAT );

        then

         A4: x in REAL ;

        A c= the carrier of REAL? ;

        then

         A5: A c= (( REAL \ NAT ) \/ { REAL }) by Def8;

        (A \ { REAL }) c= REAL

        proof

          let a be object;

          assume

           A6: a in (A \ { REAL });

          then a in A by XBOOLE_0:def 5;

          then a in ( REAL \ NAT ) or a in { REAL } by A5, XBOOLE_0:def 3;

          hence thesis by A6, XBOOLE_0:def 5;

        end;

        then

        reconsider A9 = (A \ { REAL }) as Subset of R^1 by TOPMETR: 17;

        reconsider x9 = x as Point of R^1 by A3, TOPMETR: 17;

        reconsider A9 as Subset of R^1 ;

        for B9 be Subset of R^1 st B9 is open holds x9 in B9 implies A9 meets B9

        proof

          reconsider C = NAT as Subset of R^1 by TOPMETR: 17, NUMBERS: 19;

          let B9 be Subset of R^1 ;

          reconsider B1 = B9 as Subset of R^1 ;

          reconsider C as Subset of R^1 ;

          

           A7: not x9 in NAT by A3, XBOOLE_0:def 5;

          (B9 \ NAT ) misses NAT by XBOOLE_1: 79;

          then

           A8: ((B9 \ NAT ) /\ NAT ) = {} ;

          then

          reconsider D = (B1 \ C) as Subset of REAL? by Th29;

          assume B9 is open;

          then (B1 \ C) is open by Th4, Th10;

          then

           A9: D is open by A8, Th30;

          reconsider D as Subset of REAL? ;

          assume x9 in B9;

          then x9 in (B9 \ NAT ) by A7, XBOOLE_0:def 5;

          then A meets D by A1, A9, PRE_TOPC:def 7;

          then

           A10: (A /\ D) <> {} ;

          (A9 /\ B9) <> {}

          proof

            set a = the Element of (A /\ D);

            

             A11: a in D by A10, XBOOLE_0:def 4;

            then

             A12: a in B9 by XBOOLE_0:def 5;

            

             A13: a in REAL by A11, TOPMETR: 17;

            

             A14: not a in { REAL }

            proof

              assume a in { REAL };

              then a = REAL by TARSKI:def 1;

              hence contradiction by A13;

            end;

            a in A by A10, XBOOLE_0:def 4;

            then a in (A \ { REAL }) by A14, XBOOLE_0:def 5;

            hence thesis by A12, XBOOLE_0:def 4;

          end;

          hence thesis;

        end;

        then x9 in ( Cl A9) by PRE_TOPC:def 7;

        then

        consider S9 be sequence of R^1 such that

         A15: ( rng S9) c= A9 and

         A16: x9 in ( Lim S9) by Def6;

        

         A17: ( rng S9) c= A by A15, XBOOLE_0:def 5;

        then

        reconsider S = S9 as sequence of REAL? by Th2, XBOOLE_1: 1;

        take S;

        thus ( rng S) c= A by A17;

        

         A18: S9 is_convergent_to x9 by A16, Def5;

        S is_convergent_to x

        proof

          reconsider C = { REAL } as Subset of REAL? by Lm3;

          let V be Subset of REAL? ;

          assume that

           A19: V is open and

           A20: x in V;

          reconsider C as Subset of REAL? ;

           REAL in { REAL } by TARSKI:def 1;

          then

           A21: not REAL in (V \ { REAL }) by XBOOLE_0:def 5;

          then

          reconsider V9 = (V \ C) as Subset of R^1 by Th29;

          (V \ C) is open by A19, Th4, Th31;

          then

           A22: V9 is open by A21, Th30;

           not x in C

          proof

            assume x in C;

            then x = REAL by TARSKI:def 1;

            hence contradiction by A4;

          end;

          then x in (V \ C) by A20, XBOOLE_0:def 5;

          then

          consider n be Nat such that

           A23: for m be Nat st n <= m holds (S9 . m) in V9 by A18, A22;

          take n;

          let m be Nat;

          assume n <= m;

          then (S9 . m) in V9 by A23;

          hence thesis by XBOOLE_0:def 5;

        end;

        hence thesis by Def5;

      end;

        suppose

         A24: x = REAL & x in A;

        reconsider S = ( NAT --> x) as sequence of REAL? ;

        take S;

         {x} c= A by A24, ZFMISC_1: 31;

        hence ( rng S) c= A by FUNCOP_1: 8;

        S is_convergent_to x by Th22;

        hence thesis by Def5;

      end;

        suppose

         A25: x = REAL & not x in A;

        then

        reconsider A9 = A as Subset of R^1 by Th29;

        ex k be Point of R^1 st k in NAT & ex S9 be sequence of R^1 st ( rng S9) c= A9 & S9 is_convergent_to k

        proof

          defpred P[ object, object] means ex D2 be set st D2 = $2 & $1 in D2 & $2 in the topology of R^1 & (D2 /\ A9) = {} ;

          assume

           A26: not (ex k be Point of R^1 st k in NAT & ex S9 be sequence of R^1 st ( rng S9) c= A9 & S9 is_convergent_to k);

          

           A27: for k be object st k in NAT holds ex U1 be object st P[k, U1]

          proof

            given k be object such that

             A28: k in NAT and

             A29: for U1 be object holds not P[k, U1];

            reconsider k as Point of R^1 by A28, TOPMETR: 17, NUMBERS: 19;

            reconsider k99 = k as Point of ( TopSpaceMetr RealSpace );

            reconsider k9 = k99 as Point of RealSpace by TOPMETR: 12;

            set Bs = ( Balls k99);

            consider h be sequence of Bs such that

             A30: for n be Element of NAT holds (h . n) = ( Ball (k9,(1 / (n + 1)))) by Th11;

            defpred P[ object, object] means $2 in ((h . $1) /\ A9);

            

             A31: for n be object st n in NAT holds ex z be object st z in the carrier of R^1 & P[n, z]

            proof

              let n be object;

              assume n in NAT ;

              then

              reconsider n as Element of NAT ;

              

               A32: (h . n) in Bs;

              then

              reconsider H = (h . n) as Subset of R^1 ;

              take z = the Element of (H /\ A9);

              Bs c= the topology of R^1 by TOPS_2: 64;

              then

               A33: (H /\ A9) <> {} by A29, A32, YELLOW_8: 12;

              then z in H by XBOOLE_0:def 4;

              hence thesis by A33;

            end;

            consider S9 be Function such that

             A34: ( dom S9) = NAT & ( rng S9) c= the carrier of R^1 and

             A35: for n be object st n in NAT holds P[n, (S9 . n)] from FUNCT_1:sch 6( A31);

            reconsider S9 as sequence of the carrier of R^1 by A34, FUNCT_2: 2;

            

             A36: S9 is_convergent_to k

            proof

              let U1 be Subset of R^1 ;

              assume U1 is open & k in U1;

              then

              consider r be Real such that

               A37: r > 0 and

               A38: ( Ball (k9,r)) c= U1 by TOPMETR: 15;

              reconsider r as Real;

              consider n be Nat such that

               A39: (1 / n) < r and

               A40: n > 0 by A37, Lm1;

              reconsider n as Element of NAT by ORDINAL1:def 12;

              take n;

              let m be Nat;

              

               A41: m in NAT by ORDINAL1:def 12;

              (S9 . m) in ((h . m) /\ A9) by A35, A41;

              then

               A42: (S9 . m) in (h . m) by XBOOLE_0:def 4;

              assume n <= m;

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

              then (1 / (m + 1)) < (1 / n) by A40, XREAL_1: 88;

              then ( Ball (k9,(1 / (m + 1)))) c= ( Ball (k9,r)) by A39, PCOMPS_1: 1, XXREAL_0: 2;

              then

               A43: ( Ball (k9,(1 / (m + 1)))) c= U1 by A38;

              (h . m) = ( Ball (k9,(1 / (m + 1)))) by A30, A41;

              hence thesis by A43, A42;

            end;

            ( rng S9) c= A9

            proof

              let z be object;

              assume z in ( rng S9);

              then

              consider z9 be object such that

               A44: z9 in ( dom S9) and

               A45: z = (S9 . z9) by FUNCT_1:def 3;

              (S9 . z9) in ((h . z9) /\ A9) by A35, A44;

              hence thesis by A45, XBOOLE_0:def 4;

            end;

            hence contradiction by A26, A28, A36;

          end;

          consider g be Function such that

           A46: ( dom g) = NAT & for k be object st k in NAT holds P[k, (g . k)] from CLASSES1:sch 1( A27);

          ( rng g) c= ( bool the carrier of R^1 )

          proof

            let z be object;

            assume z in ( rng g);

            then

            consider k be object such that

             A47: k in ( dom g) and

             A48: z = (g . k) by FUNCT_1:def 3;

             P[k, (g . k)] by A46, A47;

            then (g . k) in the topology of R^1 ;

            hence thesis by A48;

          end;

          then

          reconsider F = ( rng g) as Subset-Family of R^1 ;

          F is open

          proof

            let O be Subset of R^1 ;

            assume O in F;

            then

            consider k be object such that

             A49: k in ( dom g) and

             A50: O = (g . k) by FUNCT_1:def 3;

             P[k, (g . k)] by A46, A49;

            then (g . k) in the topology of R^1 ;

            hence thesis by A50, PRE_TOPC:def 2;

          end;

          then

           A51: ( union F) is open by TOPS_2: 19;

          (( union F) \ NAT ) c= ( REAL \ NAT ) by TOPMETR: 17, XBOOLE_1: 33;

          then ((( union F) \ NAT ) \/ { REAL }) c= (( REAL \ NAT ) \/ { REAL }) by XBOOLE_1: 9;

          then

          reconsider B = ((( union F) \ NAT ) \/ { REAL }) as Subset of REAL? by Def8;

          reconsider B as Subset of REAL? ;

          

           A52: (B /\ A) = {}

          proof

            set z = the Element of (B /\ A);

            assume

             A53: (B /\ A) <> {} ;

            then

             A54: z in B by XBOOLE_0:def 4;

            

             A55: z in A by A53, XBOOLE_0:def 4;

            per cases by A54, XBOOLE_0:def 3;

              suppose z in (( union F) \ NAT );

              then z in ( union F) by XBOOLE_0:def 5;

              then

              consider C be set such that

               A56: z in C and

               A57: C in F by TARSKI:def 4;

              consider l be object such that

               A58: l in ( dom g) and

               A59: C = (g . l) by A57, FUNCT_1:def 3;

               P[l, (g . l)] by A46, A58;

              then ((g . l) /\ A) = {} ;

              hence contradiction by A55, A56, A59, XBOOLE_0:def 4;

            end;

              suppose z in { REAL };

              then z = REAL by TARSKI:def 1;

              hence contradiction by A25, A53, XBOOLE_0:def 4;

            end;

          end;

           NAT c= ( union F)

          proof

            let k be object;

            assume

             A60: k in NAT ;

            then P[k, (g . k)] by A46;

            then k in (g . k) & (g . k) in ( rng g) by A46, FUNCT_1:def 3, A60;

            hence thesis by TARSKI:def 4;

          end;

          then B is open & REAL in B by A51, Th28;

          then A meets B by A1, A25, PRE_TOPC:def 7;

          hence contradiction by A52;

        end;

        then

        consider k be Point of R^1 such that

         A61: k in NAT and

         A62: ex S9 be sequence of R^1 st ( rng S9) c= A9 & S9 is_convergent_to k;

        consider S9 be sequence of R^1 such that

         A63: ( rng S9) c= A9 and

         A64: S9 is_convergent_to k by A62;

        reconsider S = S9 as sequence of REAL? by A63, Th2, XBOOLE_1: 1;

        take S;

        thus ( rng S) c= A by A63;

        S is_convergent_to x

        proof

          let U1 be Subset of REAL? ;

          assume U1 is open & x in U1;

          then

          consider O be Subset of R^1 such that

           A65: O is open & NAT c= O and

           A66: U1 = ((O \ NAT ) \/ { REAL }) by A25, Th28;

          consider n be Nat such that

           A67: for m be Nat st n <= m holds (S9 . m) in O by A61, A64, A65;

          take n;

          let m be Nat;

          assume n <= m;

          then

           A68: (S9 . m) in O by A67;

          

           A69: m in NAT by ORDINAL1:def 12;

          then m in ( dom S9) by NORMSP_1: 12;

          then (S9 . m) in ( rng S9) by FUNCT_1:def 3;

          then (S9 . m) in A9 by A63;

          then (S9 . m) in the carrier of REAL? ;

          then (S9 . m) in (( REAL \ NAT ) \/ { REAL }) by Def8;

          then

           A70: (S9 . m) in ( REAL \ NAT ) or (S9 . m) in { REAL } by XBOOLE_0:def 3;

          reconsider m as Element of NAT by A69;

          (S9 . m) <> REAL

          proof

            

             A71: (S9 . m) in REAL by TOPMETR: 17;

            assume (S9 . m) = REAL ;

            hence contradiction by A71;

          end;

          then not (S9 . m) in NAT by A70, TARSKI:def 1, XBOOLE_0:def 5;

          then (S9 . m) in (O \ NAT ) by A68, XBOOLE_0:def 5;

          hence thesis by A66, XBOOLE_0:def 3;

        end;

        hence thesis by Def5;

      end;

    end;

    theorem :: FRECHET:34

     not (for T be non empty TopSpace holds T is Frechet implies T is first-countable) by Th32, Th33;

    begin

    theorem :: FRECHET:35

    for f,g be Function st f tolerates g holds ( rng (f +* g)) = (( rng f) \/ ( rng g))

    proof

      let f,g be Function such that

       A1: f tolerates g;

      thus ( rng (f +* g)) c= (( rng f) \/ ( rng g)) by FUNCT_4: 17;

      let x be object;

      assume

       A2: x in (( rng f) \/ ( rng g));

      

       A3: ( rng (f +* g)) = ((f .: (( dom f) \ ( dom g))) \/ ( rng g)) by Th12;

      

       A4: ( rng g) c= ( rng (f +* g)) by FUNCT_4: 18;

      per cases ;

        suppose x in ( rng g);

        hence thesis by A4;

      end;

        suppose

         A5: not x in ( rng g);

        then x in ( rng f) by A2, XBOOLE_0:def 3;

        then

        consider a be object such that

         A6: a in ( dom f) and

         A7: x = (f . a) by FUNCT_1:def 3;

        now

          assume

           A8: a in ( dom g);

          x = ((f +* g) . a) by A1, A6, A7, FUNCT_4: 15

          .= (g . a) by A8, FUNCT_4: 13;

          hence contradiction by A5, A8, FUNCT_1:def 3;

        end;

        then a in (( dom f) \ ( dom g)) by A6, XBOOLE_0:def 5;

        then x in (f .: (( dom f) \ ( dom g))) by A7, FUNCT_1:def 6;

        hence thesis by A3, XBOOLE_0:def 3;

      end;

    end;

    theorem :: FRECHET:36

    for r be Real st r > 0 holds ex n be Nat st (1 / n) < r & n > 0 by Lm1;