nagata_1.miz



    begin

    reserve T,T1 for non empty TopSpace;

    

     Lm1: for r,s,t be Real st r >= 0 & s >= 0 & (r + s) < t holds r < t & s < t

    proof

      let r,s,t be Real such that

       A1: r >= 0 & s >= 0 and

       A2: (r + s) < t;

      assume r >= t or s >= t;

      then (r + s) >= (t + 0 ) or (s + r) >= (t + 0 ) by A1, XREAL_1: 7;

      hence thesis by A2;

    end;

    

     Lm2: for r1,r2,r3,r4 be Real holds |.(r1 - r4).| <= (( |.(r1 - r2).| + |.(r2 - r3).|) + |.(r3 - r4).|)

    proof

      let r1,r2,r3,r4 be Real;

      (r2 - r4) = ((r2 - r3) + (r3 - r4));

      then |.(r2 - r4).| <= ( |.(r2 - r3).| + |.(r3 - r4).|) by COMPLEX1: 56;

      then

       A1: ( |.(r1 - r2).| + |.(r2 - r4).|) <= ( |.(r1 - r2).| + ( |.(r2 - r3).| + |.(r3 - r4).|)) by XREAL_1: 7;

      (r1 - r4) = ((r1 - r2) + (r2 - r4));

      then |.(r1 - r4).| <= ( |.(r1 - r2).| + |.(r2 - r4).|) by COMPLEX1: 56;

      hence thesis by A1, XXREAL_0: 2;

    end;

    definition

      let T be TopSpace;

      let F be Subset-Family of T;

      :: NAGATA_1:def1

      attr F is discrete means

      : Def1: for p be Point of T holds ex O be open Subset of T st p in O & for A,B be Subset of T st A in F & B in F holds O meets A & O meets B implies A = B;

    end

    registration

      let T be non empty TopSpace;

      cluster discrete for Subset-Family of T;

      existence

      proof

        set F = { {} , the carrier of T};

        F c= ( bool the carrier of T)

        proof

          let f be object;

          reconsider ff = f as set by TARSKI: 1;

          assume f in F;

          then f = {} or f = the carrier of T by TARSKI:def 2;

          then ff c= the carrier of T;

          hence thesis;

        end;

        then

        reconsider F as Subset-Family of T;

        take F;

        let p be Point of T;

        take O = ( [#] T);

        thus p in O;

        now

          let A,B be Subset of T;

          assume that

           A1: A in F and

           A2: B in F;

          

           A3: B = {} or B = the carrier of T by A2, TARSKI:def 2;

          assume O meets A & O meets B;

          then

           A4: (O /\ A) <> {} & (O /\ B) <> {} by XBOOLE_0:def 7;

          A = {} or A = the carrier of T by A1, TARSKI:def 2;

          hence A = B by A3, A4;

        end;

        hence thesis;

      end;

    end

    registration

      let T;

      cluster empty discrete for Subset-Family of T;

      existence

      proof

        reconsider F = {} as Subset-Family of T by XBOOLE_1: 2;

        take F;

        thus F is empty;

        let p be Point of T;

        take ( [#] T);

        thus thesis;

      end;

    end

    reserve F,G,H for Subset-Family of T,

A,B,C,D for Subset of T,

O,U for open Subset of T,

p,q for Point of T,

x,y,X for set;

    theorem :: NAGATA_1:1

    

     Th1: for F st (ex A st F = {A}) holds F is discrete

    proof

      let F;

      assume ex A st F = {A};

      then

      consider A such that

       A1: F = {A};

      now

        let p;

        take O = ( [#] T);

        thus p in O;

        now

          let B, C;

          assume that

           A2: B in F and

           A3: C in F;

           {B} c= {A} by A1, A2, ZFMISC_1: 31;

          then

           A4: B = A by ZFMISC_1: 3;

           {C} c= {A} by A1, A3, ZFMISC_1: 31;

          hence B = C by A4, ZFMISC_1: 3;

        end;

        hence for B, C st B in F & C in F holds O meets B & O meets C implies B = C;

      end;

      hence thesis;

    end;

    theorem :: NAGATA_1:2

    

     Th2: for F, G st F c= G & G is discrete holds F is discrete

    proof

      let F,G be Subset-Family of T;

      assume that

       A1: F c= G and

       A2: G is discrete;

      now

        let p;

        thus ex O st p in O & for C, D st C in F & D in F holds O meets C & O meets D implies C = D

        proof

          consider U such that

           A3: p in U & for C, D st C in G & D in G holds U meets C & U meets D implies C = D by A2;

          take O = U;

          thus thesis by A1, A3;

        end;

        hence ex O st p in O & for C, D st C in F & D in F holds O meets C & O meets D implies C = D;

      end;

      hence thesis;

    end;

    theorem :: NAGATA_1:3

    for F, G st F is discrete holds (F /\ G) is discrete by Th2, XBOOLE_1: 17;

    theorem :: NAGATA_1:4

    for F, G st F is discrete holds (F \ G) is discrete by Th2, XBOOLE_1: 36;

    theorem :: NAGATA_1:5

    for F, G, H st F is discrete & G is discrete & ( INTERSECTION (F,G)) = H holds H is discrete

    proof

      let F, G, H;

      assume that

       A1: F is discrete and

       A2: G is discrete and

       A3: ( INTERSECTION (F,G)) = H;

      now

        let p;

        consider O such that

         A4: p in O and

         A5: for A,B be Subset of T st A in F & B in F holds O meets A & O meets B implies A = B by A1;

        consider U such that

         A6: p in U and

         A7: for A,B be Subset of T st A in G & B in G holds U meets A & U meets B implies A = B by A2;

         A8:

        now

          let A, B;

          assume that

           A9: A in ( INTERSECTION (F,G)) and

           A10: B in ( INTERSECTION (F,G));

          consider af,ag be set such that

           A11: af in F and

           A12: ag in G and

           A13: A = (af /\ ag) by A9, SETFAM_1:def 5;

          assume that

           A14: (O /\ U) meets A and

           A15: (O /\ U) meets B;

          consider bf,bg be set such that

           A16: bf in F and

           A17: bg in G and

           A18: B = (bf /\ bg) by A10, SETFAM_1:def 5;

          ((O /\ U) /\ (bf /\ bg)) <> {} by A18, A15, XBOOLE_0:def 7;

          then (((O /\ U) /\ bf) /\ bg) <> {} by XBOOLE_1: 16;

          then

           A19: (((O /\ bf) /\ U) /\ bg) <> {} by XBOOLE_1: 16;

          then (O /\ bf) <> {} ;

          then

           A20: O meets bf by XBOOLE_0:def 7;

          ((O /\ U) /\ (af /\ ag)) <> {} by A13, A14, XBOOLE_0:def 7;

          then (((O /\ U) /\ af) /\ ag) <> {} by XBOOLE_1: 16;

          then

           A21: (((O /\ af) /\ U) /\ ag) <> {} by XBOOLE_1: 16;

          then ((O /\ af) /\ (U /\ ag)) <> {} by XBOOLE_1: 16;

          then (U /\ ag) <> {} ;

          then

           A22: U meets ag by XBOOLE_0:def 7;

          ((O /\ bf) /\ (U /\ bg)) <> {} by A19, XBOOLE_1: 16;

          then (U /\ bg) <> {} ;

          then

           A23: U meets bg by XBOOLE_0:def 7;

          (O /\ af) <> {} by A21;

          then O meets af by XBOOLE_0:def 7;

          then af = bf by A5, A11, A16, A20;

          hence A = B by A7, A12, A13, A17, A18, A22, A23;

        end;

        set Q = (O /\ U);

        p in Q by A4, A6, XBOOLE_0:def 4;

        hence ex Q be open Subset of T st p in Q & for A,B be Subset of T st A in H & B in H holds Q meets A & Q meets B implies A = B by A3, A8;

      end;

      hence thesis;

    end;

    theorem :: NAGATA_1:6

    

     Th6: for F, A, B st F is discrete & A in F & B in F holds A = B or A misses B

    proof

      let F, A, B;

      assume that

       A1: F is discrete and

       A2: A in F & B in F;

      assume that

       A3: A <> B and

       A4: A meets B;

      (A /\ B) <> ( {} T) by A4, XBOOLE_0:def 7;

      then

      consider p such that

       A5: p in (A /\ B) by PRE_TOPC: 12;

      consider O such that

       A6: p in O and

       A7: for C, D st C in F & D in F holds O meets C & O meets D implies C = D by A1;

      

       A8: {p} c= O by A6, ZFMISC_1: 31;

      p in B by A5, XBOOLE_0:def 4;

      then {p} c= B by ZFMISC_1: 31;

      then {p} c= (O /\ B) by A8, XBOOLE_1: 19;

      then

       A9: p in (O /\ B) by ZFMISC_1: 31;

      p in A by A5, XBOOLE_0:def 4;

      then {p} c= A by ZFMISC_1: 31;

      then {p} c= (O /\ A) by A8, XBOOLE_1: 19;

      then

       A10: p in (O /\ A) by ZFMISC_1: 31;

      O meets A & O meets B implies A = B by A2, A7;

      hence contradiction by A3, A10, A9, XBOOLE_0: 4;

    end;

    theorem :: NAGATA_1:7

    

     Th7: F is discrete implies for p holds ex O st p in O & (( INTERSECTION ( {O},F)) \ { {} }) is trivial

    proof

      assume

       A1: F is discrete;

      let p;

      consider O such that

       A2: p in O and

       A3: for C, D st C in F & D in F holds O meets C & O meets D implies C = D by A1;

      set I = ( INTERSECTION ( {O},F));

      

       A4: for f,g be set st f in I & g in I holds f = g or f = {} or g = {}

      proof

        let f,g be set;

        assume that

         A5: f in I and

         A6: g in I;

        consider o1,f1 be set such that

         A7: o1 in {O} and

         A8: f1 in F and

         A9: f = (o1 /\ f1) by A5, SETFAM_1:def 5;

        consider o2,g1 be set such that

         A10: o2 in {O} and

         A11: g1 in F and

         A12: g = (o2 /\ g1) by A6, SETFAM_1:def 5;

         {o2} c= {O} by A10, ZFMISC_1: 31;

        then

         A13: o2 = O by ZFMISC_1: 3;

         {o1} c= {O} by A7, ZFMISC_1: 31;

        then

         A14: o1 = O by ZFMISC_1: 3;

        then O meets f1 & O meets g1 or f = {} or g = {} by A9, A12, A13, XBOOLE_0:def 7;

        hence thesis by A3, A8, A9, A11, A12, A14, A13;

      end;

      

       A15: for f be set st f <> {} & f in I holds I c= { {} , f}

      proof

        let f be set;

        assume

         A16: f <> {} & f in I;

        now

          let g be object;

          assume g in I;

          then f = g or g = {} by A4, A16;

          hence g in { {} , f} by TARSKI:def 2;

        end;

        hence thesis;

      end;

      now

        per cases ;

          suppose (I \ { {} }) <> {} ;

          then

          consider f be object such that

           A17: f in (I \ { {} }) by XBOOLE_0:def 1;

          f <> {} by A17, ZFMISC_1: 56;

          then

           A18: I c= { {} , f} by A15, A17;

          now

            let g be object;

            assume g in I;

            then {g} c= { {} , f} by A18, ZFMISC_1: 31;

            then g = {} or g = f by ZFMISC_1: 19;

            then g in { {} } or g in {f} by ZFMISC_1: 31;

            hence g in ( { {} } \/ {f}) by XBOOLE_0:def 3;

          end;

          then I c= ( { {} } \/ {f});

          then (I \ { {} }) c= {f} by XBOOLE_1: 43;

          then (I \ { {} }) = {} or (I \ { {} }) = {f} by ZFMISC_1: 33;

          hence (I \ { {} }) is trivial;

        end;

          suppose (I \ { {} }) = {} ;

          hence (I \ { {} }) is trivial;

        end;

      end;

      hence thesis by A2;

    end;

    theorem :: NAGATA_1:8

    F is discrete iff (for p holds ex O st p in O & (( INTERSECTION ( {O},F)) \ { {} }) is trivial) & for A, B st A in F & B in F holds A = B or A misses B

    proof

      now

        let F;

        (for p holds ex O st p in O & (( INTERSECTION ( {O},F)) \ { {} }) is trivial) & (for A, B st A in F & B in F holds A = B or A misses B) implies F is discrete

        proof

          assume that

           A1: for p holds ex O st p in O & (( INTERSECTION ( {O},F)) \ { {} }) is trivial and

           A2: for A, B st A in F & B in F holds A = B or A misses B;

          assume not F is discrete;

          then

          consider p such that

           A3: for O holds not p in O or not (for A, B st A in F & B in F holds O meets A & O meets B implies A = B);

          consider O such that

           A4: p in O and

           A5: (( INTERSECTION ( {O},F)) \ { {} }) is trivial by A1;

          consider A, B such that

           A6: A in F and

           A7: B in F and

           A8: O meets A and

           A9: O meets B and

           A10: A <> B by A3, A4;

          

           A11: (O /\ B) <> {} by A9, XBOOLE_0:def 7;

          set I = ( INTERSECTION ( {O},F));

          consider a be object such that

           A12: (I \ { {} }) = {} or (I \ { {} }) = {a} by A5, ZFMISC_1: 131;

          

           A13: O in {O} by ZFMISC_1: 31;

          then (O /\ B) in I by A7, SETFAM_1:def 5;

          then (O /\ B) in (I \ { {} }) by A11, ZFMISC_1: 56;

          then {(O /\ B)} c= {a} by A12, ZFMISC_1: 31;

          then

           A14: (O /\ B) = a by ZFMISC_1: 3;

          

           A15: (O /\ A) <> {} by A8, XBOOLE_0:def 7;

          then

          consider f be object such that

           A16: f in (O /\ A) by XBOOLE_0:def 1;

          

           A17: f in A by A16, XBOOLE_0:def 4;

          (O /\ A) in I by A6, A13, SETFAM_1:def 5;

          then (O /\ A) in (I \ { {} }) by A15, ZFMISC_1: 56;

          then {(O /\ A)} c= {a} by A12, ZFMISC_1: 31;

          then (O /\ A) = a by ZFMISC_1: 3;

          then f in B by A14, A16, XBOOLE_0:def 4;

          then

           A18: f in (A /\ B) by A17, XBOOLE_0:def 4;

          A misses B by A2, A6, A7, A10;

          hence thesis by A18, XBOOLE_0:def 7;

        end;

        hence F is discrete iff (for p holds ex O st p in O & (( INTERSECTION ( {O},F)) \ { {} }) is trivial) & for A, B st A in F & B in F holds A = B or A misses B by Th6, Th7;

      end;

      hence thesis;

    end;

    

     Lm3: for O, A holds O meets ( Cl A) implies O meets A

    proof

      let O, A;

      O misses A implies O misses ( Cl A)

      proof

        assume O misses A;

        then A c= (O ` ) by SUBSET_1: 23;

        then ( Cl A) c= (O ` ) by TOPS_1: 5;

        hence thesis by SUBSET_1: 23;

      end;

      hence thesis;

    end;

    registration

      let T;

      let F be discrete Subset-Family of T;

      cluster ( clf F) -> discrete;

      coherence

      proof

        thus ( clf F) is discrete

        proof

          let p;

          consider O such that

           A1: p in O and

           A2: for A, B st A in F & B in F holds O meets A & O meets B implies A = B by Def1;

          now

            let A, B;

            assume that

             A3: A in ( clf F) and

             A4: B in ( clf F);

            consider C such that

             A5: A = ( Cl C) and

             A6: C in F by A3, PCOMPS_1:def 2;

            assume that

             A7: O meets A and

             A8: O meets B;

            consider D such that

             A9: B = ( Cl D) and

             A10: D in F by A4, PCOMPS_1:def 2;

            

             A11: O meets D by A9, A8, Lm3;

            O meets C by A5, A7, Lm3;

            hence A = B by A2, A5, A6, A9, A10, A11;

          end;

          hence thesis by A1;

        end;

      end;

    end

    

     Lm4: for F holds for A st A in F holds ( Cl A) c= ( Cl ( union F))

    proof

      let F;

      let A;

      assume A in F;

      then for f be object st f in A holds f in ( union F) by TARSKI:def 4;

      then A c= ( union F);

      hence thesis by PRE_TOPC: 19;

    end;

    theorem :: NAGATA_1:9

    for F st F is discrete holds for A, B st A in F & B in F holds ( Cl (A /\ B)) = (( Cl A) /\ ( Cl B))

    proof

      let F such that

       A1: F is discrete;

      let A, B such that

       A2: A in F & B in F;

      now

        per cases by A1, A2, Th6;

          suppose A misses B;

          then

           A3: (A /\ B) = ( {} T) by XBOOLE_0:def 7;

          (( Cl A) /\ ( Cl B)) = {}

          proof

            assume (( Cl A) /\ ( Cl B)) <> {} ;

            then

            consider x be object such that

             A4: x in (( Cl A) /\ ( Cl B)) by XBOOLE_0:def 1;

            consider O such that

             A5: x in O and

             A6: for A, B st A in F & B in F holds O meets A & O meets B implies A = B by A1, A4;

            x in ( Cl A) by A4, XBOOLE_0:def 4;

            then

             A7: O meets A by A5, PRE_TOPC:def 7;

            x in ( Cl B) by A4, XBOOLE_0:def 4;

            then O meets B by A5, PRE_TOPC:def 7;

            then A = B by A2, A6, A7;

            hence thesis by A3, A7, XBOOLE_1: 65;

          end;

          hence thesis by A3, PRE_TOPC: 22;

        end;

          suppose A = B;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: NAGATA_1:10

    for F st F is discrete holds ( Cl ( union F)) = ( union ( clf F))

    proof

      let F;

      assume

       A1: F is discrete;

      

       A2: ( Cl ( union F)) c= ( union ( clf F))

      proof

        let x be object;

        assume

         A3: x in ( Cl ( union F));

        then

        consider O such that

         A4: x in O and

         A5: for A, B st A in F & B in F holds O meets A & O meets B implies A = B by A1;

         not O misses ( union F) by A3, A4, PRE_TOPC:def 7;

        then

        consider f be object such that

         A6: f in O and

         A7: f in ( union F) by XBOOLE_0: 3;

        consider AF be set such that

         A8: f in AF and

         A9: AF in F by A7, TARSKI:def 4;

        reconsider AF as Subset of T by A9;

        

         A10: O meets AF by A6, A8, XBOOLE_0: 3;

        for D st D is open & x in D holds not D misses AF

        proof

          assume ex D st D is open & x in D & D misses AF;

          then

          consider D such that

           A11: D is open and

           A12: x in D and

           A13: D misses AF;

          x in (D /\ O) by A4, A12, XBOOLE_0:def 4;

          then (D /\ O) meets ( union F) by A3, A11, PRE_TOPC:def 7;

          then

          consider y be object such that

           A14: y in (D /\ O) and

           A15: y in ( union F) by XBOOLE_0: 3;

          consider BF be set such that

           A16: y in BF and

           A17: BF in F by A15, TARSKI:def 4;

          y in D by A14, XBOOLE_0:def 4;

          then y in (D /\ BF) by A16, XBOOLE_0:def 4;

          then

           A18: D meets BF by XBOOLE_0:def 7;

          y in O by A14, XBOOLE_0:def 4;

          then y in (O /\ BF) by A16, XBOOLE_0:def 4;

          then O meets BF by XBOOLE_0:def 7;

          hence contradiction by A5, A9, A10, A13, A17, A18;

        end;

        then

         A19: x in ( Cl AF) by A3, PRE_TOPC:def 7;

        ( Cl AF) in ( clf F) by A9, PCOMPS_1:def 2;

        hence thesis by A19, TARSKI:def 4;

      end;

      ( union ( clf F)) c= ( Cl ( union F))

      proof

        let f be object;

        assume f in ( union ( clf F));

        then

        consider Af be set such that

         A20: f in Af and

         A21: Af in ( clf F) by TARSKI:def 4;

        reconsider Af as Subset of T by A21;

        ex A st ( Cl A) = Af & A in F by A21, PCOMPS_1:def 2;

        then Af c= ( Cl ( union F)) by Lm4;

        hence thesis by A20;

      end;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: NAGATA_1:11

    

     Th11: for F st F is discrete holds F is locally_finite

    proof

      let F;

      assume

       A1: F is discrete;

      for p holds ex A st p in A & A is open & { D : D in F & D meets A } is finite

      proof

        let p;

        consider U such that

         A2: p in U and

         A3: for A, B st A in F & B in F holds U meets A & U meets B implies A = B by A1;

        set SF = { D : D in F & D meets U };

        take O = U;

        SF <> {} implies ex A st SF = {A}

        proof

          assume SF <> {} ;

          then

          consider a be object such that

           A4: a in SF by XBOOLE_0:def 1;

          consider D such that

           A5: a = D and

           A6: D in F & D meets O by A4;

          now

            let b be object;

            assume b in SF;

            then ex C st b = C & C in F & C meets O;

            then b = D by A3, A6;

            hence b in {D} by TARSKI:def 1;

          end;

          then

           A7: SF c= {D};

           {D} c= SF by A4, A5, ZFMISC_1: 31;

          then SF = {D} by A7, XBOOLE_0:def 10;

          hence thesis;

        end;

        hence thesis by A2;

      end;

      hence thesis;

    end;

    definition

      let T be TopSpace;

      mode FamilySequence of T is sequence of ( bool ( bool the carrier of T)) qua non empty set;

    end

    reserve Un for FamilySequence of T,

r,r1,r2 for Real,

n for Element of NAT ;

    definition

      let T, Un, n;

      :: original: .

      redefine

      func Un . n -> Subset-Family of T ;

      coherence

      proof

        (Un . n) c= ( bool the carrier of T);

        hence thesis;

      end;

    end

    definition

      let T, Un;

      :: original: Union

      redefine

      func Union Un -> Subset-Family of T ;

      coherence

      proof

        ( Union Un) c= ( bool the carrier of T);

        hence thesis;

      end;

    end

    definition

      let T be non empty TopSpace;

      let Un be FamilySequence of T;

      :: NAGATA_1:def2

      attr Un is sigma_discrete means

      : Def2: for n be Element of NAT holds (Un . n) is discrete;

    end

    

     Lm5: ex Un be FamilySequence of T st Un is sigma_discrete

    proof

      set C = {the carrier of T};

      the carrier of T in ( bool the carrier of T) by ZFMISC_1:def 1;

      then C c= ( bool the carrier of T) by ZFMISC_1: 31;

      then

      reconsider f = ( NAT --> C) as sequence of ( bool ( bool the carrier of T)) by FUNCOP_1: 45;

      take f;

      now

        let n;

        the carrier of T is Subset of T by ZFMISC_1:def 1;

        hence (f . n) is discrete by Th1, FUNCOP_1: 7;

      end;

      hence thesis;

    end;

    registration

      let T be non empty TopSpace;

      cluster sigma_discrete for FamilySequence of T;

      existence by Lm5;

    end

    definition

      let T be non empty TopSpace;

      let Un be FamilySequence of T;

      :: NAGATA_1:def3

      attr Un is sigma_locally_finite means for n be Element of NAT holds (Un . n) is locally_finite;

    end

    definition

      let T;

      let F be Subset-Family of T;

      :: NAGATA_1:def4

      attr F is sigma_discrete means ex f be sigma_discrete FamilySequence of T st F = ( Union f);

    end

    registration

      let T be non empty TopSpace;

      cluster sigma_locally_finite for FamilySequence of T;

      existence

      proof

        thus ex Un be FamilySequence of T st Un is sigma_locally_finite

        proof

          consider Un be FamilySequence of T such that

           A1: Un is sigma_discrete by Lm5;

          take Un;

          for n holds (Un . n) is locally_finite by Th11, A1;

          hence thesis;

        end;

      end;

    end

    theorem :: NAGATA_1:12

    for Un st Un is sigma_discrete holds Un is sigma_locally_finite by Th11;

    theorem :: NAGATA_1:13

    for A be uncountable set holds ex F be Subset-Family of ( 1TopSp [:A, A:]) st F is locally_finite & not F is sigma_discrete

    proof

      let A be uncountable set;

      set TS = ( 1TopSp [:A, A:]);

      set F = { ( [: {a}, A:] \/ [:A, {a}:]) where a be Element of A : a in A };

      F c= ( bool [:A, A:])

      proof

        let f be object;

        assume f in F;

        then

        consider a be Element of A such that

         A1: f = ( [: {a}, A:] \/ [:A, {a}:]) and a in A;

         [: {a}, A:] c= [:A, A:] & [:A, {a}:] c= [:A, A:] by ZFMISC_1: 96;

        then ( [: {a}, A:] \/ [:A, {a}:]) c= [:A, A:] by XBOOLE_1: 8;

        hence thesis by A1;

      end;

      then

      reconsider F as Subset-Family of TS;

      take F;

      for z be Point of TS holds ex Z be Subset of TS st z in Z & Z is open & { O where O be Subset of TS : O in F & O meets Z } is finite

      proof

        let z be Point of TS;

        set Z = {z};

        reconsider Z as Subset of TS;

        consider x,y be object such that x in A and y in A and

         A2: z = [x, y] by ZFMISC_1:def 2;

        set yAAy = {( [: {y}, A:] \/ [:A, {y}:])};

        set xAAx = {( [: {x}, A:] \/ [:A, {x}:])};

        set UZ = { O where O be Subset of TS : O in F & O meets Z };

        

         A3: UZ c= (xAAx \/ yAAy)

        proof

          let U be object;

          assume U in UZ;

          then

          consider O be Subset of TS such that

           A4: U = O and

           A5: O in F and

           A6: O meets Z;

          consider u be object such that

           A7: u in O and

           A8: u in Z by A6, XBOOLE_0: 3;

          consider a be Element of A such that

           A9: O = ( [: {a}, A:] \/ [:A, {a}:]) and a in A by A5;

          now

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

              suppose u in [: {a}, A:];

              then [x, y] in [: {a}, A:] by A2, A8, TARSKI:def 1;

              then x in {a} by ZFMISC_1: 87;

              then x = a by TARSKI:def 1;

              then O in xAAx by A9, TARSKI:def 1;

              hence O in (xAAx \/ yAAy) by XBOOLE_0:def 3;

            end;

              suppose u in [:A, {a}:];

              then [x, y] in [:A, {a}:] by A2, A8, TARSKI:def 1;

              then y in {a} by ZFMISC_1: 87;

              then y = a by TARSKI:def 1;

              then O in yAAy by A9, TARSKI:def 1;

              hence O in (xAAx \/ yAAy) by XBOOLE_0:def 3;

            end;

          end;

          hence thesis by A4;

        end;

        z in Z & Z is open by PRE_TOPC:def 2, ZFMISC_1: 31;

        hence thesis by A3;

      end;

      hence F is locally_finite;

       not F is sigma_discrete

      proof

        consider a be object such that

         A10: a in A by XBOOLE_0:def 1;

        reconsider a as Element of A by A10;

        set aAAa = ( [: {a}, A:] \/ [:A, {a}:]);

        

         A11: ( card A) c= ( card F)

        proof

          deffunc D( object) = ( [: {$1}, A:] \/ [:A, {$1}:]);

          consider d be Function such that

           A12: ( dom d) = A & for x be object st x in A holds (d . x) = D(x) from FUNCT_1:sch 3;

          for a1,a2 be object st a1 in ( dom d) & a2 in ( dom d) & (d . a1) = (d . a2) holds a1 = a2

          proof

            let a1,a2 be object;

            assume that

             A13: a1 in ( dom d) and

             A14: a2 in ( dom d) and

             A15: (d . a1) = (d . a2);

            a1 in {a1} by ZFMISC_1: 31;

            then

             A16: [a1, a1] in [: {a1}, A:] by A12, A13, ZFMISC_1: 87;

             D(a1) = (d . a1) & D(a2) = (d . a2) by A12, A13, A14;

            then [a1, a1] in ( [: {a2}, A:] \/ [:A, {a2}:]) by A15, A16, XBOOLE_0:def 3;

            then [a1, a1] in [: {a2}, A:] or [a1, a1] in [:A, {a2}:] by XBOOLE_0:def 3;

            then

             A17: a1 in {a2} by ZFMISC_1: 87;

            assume a1 <> a2;

            hence thesis by A17, TARSKI:def 1;

          end;

          then

           A18: d is one-to-one by FUNCT_1:def 4;

          ( rng d) c= F

          proof

            let AA be object;

            assume AA in ( rng d);

            then

            consider a be object such that

             A19: a in ( dom d) and

             A20: AA = (d . a) by FUNCT_1:def 3;

            reconsider a as Element of A by A12, A19;

            AA = ( [: {a}, A:] \/ [:A, {a}:]) by A12, A20;

            hence thesis;

          end;

          hence thesis by A12, A18, CARD_1: 10;

        end;

        assume F is sigma_discrete;

        then

        consider f be sigma_discrete FamilySequence of TS such that

         A21: F = ( Union f);

        defpred F1[ object, object] means ($2 in (f . $1) & (f . $1) is non empty) or ($2 = aAAa & (f . $1) is empty);

        

         A22: for k be object st k in NAT holds ex f be object st f in F & F1[k, f]

        proof

          let k be object;

          assume k in NAT ;

          then

          reconsider k as Element of NAT ;

          now

            per cases ;

              suppose

               A23: (f . k) is empty;

              aAAa in F;

              hence ex A be set st A in F & F1[k, A] by A23;

            end;

              suppose (f . k) is non empty;

              then

              consider A be object such that

               A24: A in (f . k) by XBOOLE_0:def 1;

              A in F by A21, A24, PROB_1: 12;

              hence ex A be set st A in F & F1[k, A] by A24;

            end;

          end;

          hence thesis;

        end;

        consider Df be sequence of F such that

         A25: for k be object st k in NAT holds F1[k, (Df . k)] from FUNCT_2:sch 1( A22);

        

         A26: for n be Element of NAT , AD,BD be Element of F st F1[n, AD] & F1[n, BD] holds AD = BD

        proof

          let n be Element of NAT , AD,BD be Element of F;

          assume that

           A27: F1[n, AD] and

           A28: F1[n, BD];

          now

            

             A29: (f . n) is discrete by Def2;

            BD in F by A21, A28, PROB_1: 12;

            then

            consider b be Element of A such that

             A30: BD = ( [: {b}, A:] \/ [:A, {b}:]) and b in A;

            AD in F by A21, A27, PROB_1: 12;

            then

            consider a be Element of A such that

             A31: AD = ( [: {a}, A:] \/ [:A, {a}:]) and a in A;

            b in {b} by TARSKI:def 1;

            then [a, b] in [:A, {b}:] by ZFMISC_1: 87;

            then

             A32: [a, b] in BD by A30, XBOOLE_0:def 3;

            a in {a} by TARSKI:def 1;

            then [a, b] in [: {a}, A:] by ZFMISC_1: 87;

            then [a, b] in AD by A31, XBOOLE_0:def 3;

            then AD meets BD by A32, XBOOLE_0: 3;

            hence thesis by A27, A28, A29, Th6;

          end;

          hence thesis;

        end;

        

         A33: F c= (Df .: NAT )

        proof

          let cAAc be object;

          assume

           A34: cAAc in F;

          then

          consider k be Nat such that

           A35: cAAc in (f . k) by A21, PROB_1: 12;

          

           A36: k in NAT by ORDINAL1:def 12;

           F1[k, (Df . k)] by A25, A36;

          then

           A37: cAAc = (Df . k) by A26, A34, A35, A36;

          ( dom Df) = NAT by A34, FUNCT_2:def 1;

          hence thesis by A37, FUNCT_1:def 6, A36;

        end;

        

         A38: not ( card A) c= omega by CARD_3:def 14;

        then ( card NAT ) in ( card A) by CARD_1: 4, CARD_1: 47;

        then ( card NAT ) c= ( card F) by A11, CARD_1: 3;

        then ( card NAT ) c< ( card F) by A11, A38, CARD_1: 47, XBOOLE_0:def 8;

        then

         A39: ( card (Df .: NAT )) c< ( card F) by CARD_1: 67, XBOOLE_1: 59;

        then ( card (Df .: NAT )) c= ( card F) by XBOOLE_0:def 8;

        then ( card (Df .: NAT )) in ( card F) by A39, CARD_1: 3;

        then (F \ (Df .: NAT )) <> {} by CARD_1: 68;

        hence contradiction by A33, XBOOLE_1: 37;

      end;

      hence thesis;

    end;

    definition

      let T be non empty TopSpace;

      let Un be FamilySequence of T;

      :: NAGATA_1:def5

      attr Un is Basis_sigma_discrete means Un is sigma_discrete & ( Union Un) is Basis of T;

    end

    definition

      let T be non empty TopSpace;

      let Un be FamilySequence of T;

      :: NAGATA_1:def6

      attr Un is Basis_sigma_locally_finite means Un is sigma_locally_finite & ( Union Un) is Basis of T;

    end

    theorem :: NAGATA_1:14

    

     Th14: for r be Real, PM be non empty MetrSpace holds for x be Element of PM holds (( [#] PM) \ ( cl_Ball (x,r))) in ( Family_open_set PM)

    proof

      let r be Real;

      reconsider r9 = r as Real;

      let PM be non empty MetrSpace;

      let x be Element of PM;

      now

        let y be Element of PM;

        set r1 = (( dist (x,y)) - r9);

        

         A1: ( Ball (y,r1)) c= (( [#] PM) \ ( cl_Ball (x,r)))

        proof

          assume not ( Ball (y,r1)) c= (( [#] PM) \ ( cl_Ball (x,r)));

          then

          consider z be object such that

           A2: z in ( Ball (y,r1)) and

           A3: not z in (( [#] PM) \ ( cl_Ball (x,r)));

          reconsider z as Element of PM by A2;

           not (z in ( [#] PM) & not z in ( cl_Ball (x,r))) by A3, XBOOLE_0:def 5;

          then

           A4: ( dist (x,z)) <= r9 by METRIC_1: 12;

          ( dist (y,z)) < r1 by A2, METRIC_1: 11;

          then (( dist (y,z)) + ( dist (x,z))) < (r1 + r9) by A4, XREAL_1: 8;

          then (( dist (x,z)) + ( dist (z,y))) < (r1 + r9);

          hence thesis by METRIC_1: 4;

        end;

        assume y in (( [#] PM) \ ( cl_Ball (x,r)));

        then not y in ( cl_Ball (x,r)) by XBOOLE_0:def 5;

        then (r9 + 0 ) < (r9 + r1) by METRIC_1: 12;

        then (r9 - r9) < (r1 - 0 ) by XREAL_1: 21;

        hence ex r2 st r2 > 0 & ( Ball (y,r2)) c= (( [#] PM) \ ( cl_Ball (x,r))) by A1;

      end;

      hence thesis by PCOMPS_1:def 4;

    end;

    theorem :: NAGATA_1:15

    for T st T is metrizable holds T is regular & T is T_1

    proof

      let T;

      assume T is metrizable;

      then

      consider metr be Function of [:the carrier of T, the carrier of T:], REAL such that

       A1: metr is_metric_of the carrier of T and

       A2: ( Family_open_set ( SpaceMetr (the carrier of T,metr))) = the topology of T;

      set PM = ( SpaceMetr (the carrier of T,metr));

      reconsider PM as non empty MetrSpace by A1, PCOMPS_1: 36;

      set TPM = ( TopSpaceMetr PM);

      

       A3: for p be Element of T holds for D be Subset of T st D <> {} & D is closed & p in (D ` ) holds ex A,B be Subset of T st A is open & B is open & p in A & D c= B & A misses B

      proof

        let p be Element of T;

        let D be Subset of T;

        assume that D <> {} and

         A4: D is closed and

         A5: p in (D ` );

        

         A6: (( [#] T) \ D) in the topology of T by A4, A5, PRE_TOPC:def 2;

        reconsider p as Element of PM by A1, PCOMPS_2: 4;

        

         A7: D misses (D ` ) by XBOOLE_1: 79;

        reconsider D as Subset of TPM by A1, PCOMPS_2: 4;

        (( [#] TPM) \ D) in ( Family_open_set PM) by A1, A2, A6, PCOMPS_2: 4;

        then (( [#] TPM) \ D) is open by PRE_TOPC:def 2;

        then

         A8: D is closed by PRE_TOPC:def 3;

        

         A9: not p in D by A5, A7, XBOOLE_0: 3;

        ex r1 st r1 > 0 & ( Ball (p,r1)) misses D

        proof

          assume

           A10: for r1 st r1 > 0 holds ( Ball (p,r1)) meets D;

          now

            let A be Subset of TPM;

            assume that

             A11: A is open and

             A12: p in A;

            A in ( Family_open_set PM) by A11, PRE_TOPC:def 2;

            then

            consider r2 such that

             A13: r2 > 0 and

             A14: ( Ball (p,r2)) c= A by A12, PCOMPS_1:def 4;

            ( Ball (p,r2)) meets D by A10, A13;

            then ex x be object st x in ( Ball (p,r2)) & x in D by XBOOLE_0: 3;

            hence A meets D by A14, XBOOLE_0: 3;

          end;

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

          hence thesis by A8, A9, PRE_TOPC: 22;

        end;

        then

        consider r1 such that

         A15: r1 > 0 and

         A16: ( Ball (p,r1)) misses D;

        set r2 = (r1 / 2);

        

         A17: r2 < (r2 + r2) by A15, XREAL_1: 29;

        

         A18: D c= (( [#] PM) \ ( cl_Ball (p,r2)))

        proof

          assume not D c= (( [#] PM) \ ( cl_Ball (p,r2)));

          then

          consider x be object such that

           A19: x in D and

           A20: not x in (( [#] PM) \ ( cl_Ball (p,r2)));

          reconsider x as Element of PM by A19;

          x in ( cl_Ball (p,r2)) by A20, XBOOLE_0:def 5;

          then ( dist (p,x)) <= r2 by METRIC_1: 12;

          then ( dist (p,x)) < r1 by A17, XXREAL_0: 2;

          then x in ( Ball (p,r1)) by METRIC_1: 11;

          hence thesis by A16, A19, XBOOLE_0: 3;

        end;

        set r4 = (r2 / 2);

        

         A21: r2 > 0 by A15, XREAL_1: 139;

        then

         A22: r4 < (r4 + r4) by XREAL_1: 29;

        

         A23: ( Ball (p,r4)) misses (( [#] PM) \ ( cl_Ball (p,r2)))

        proof

          assume ( Ball (p,r4)) meets (( [#] PM) \ ( cl_Ball (p,r2)));

          then

          consider x be object such that

           A24: x in ( Ball (p,r4)) and

           A25: x in (( [#] PM) \ ( cl_Ball (p,r2))) by XBOOLE_0: 3;

          reconsider x as Element of PM by A24;

           not x in ( cl_Ball (p,r2)) by A25, XBOOLE_0:def 5;

          then

           A26: ( dist (p,x)) > r2 by METRIC_1: 12;

          ( dist (p,x)) < r4 by A24, METRIC_1: 11;

          hence thesis by A22, A26, XXREAL_0: 2;

        end;

        set A = ( Ball (p,r4));

        set B = (( [#] PM) \ ( cl_Ball (p,r2)));

        

         A27: B in ( Family_open_set PM) & A in ( Family_open_set PM) by Th14, PCOMPS_1: 29;

        then

        reconsider A, B as Subset of T by A2;

        take A, B;

        r4 > 0 by A21, XREAL_1: 139;

        then ( dist (p,p)) < r4 by METRIC_1: 1;

        hence thesis by A2, A18, A23, A27, METRIC_1: 11, PRE_TOPC:def 2;

      end;

      for p,q be Point of T st not p = q holds ex A,B be Subset of T st A is open & B is open & p in A & not q in A & q in B & not p in B

      proof

        let p,q be Point of T;

        assume

         A28: not p = q;

        reconsider p, q as Element of TPM by A1, PCOMPS_2: 4;

        TPM is T_2 by PCOMPS_1: 34;

        then

        consider A,B be Subset of TPM such that

         A29: A is open and

         A30: B is open and

         A31: p in A & q in B and

         A32: A misses B by A28, PRE_TOPC:def 10;

        reconsider A, B as Subset of T by A1, PCOMPS_2: 4;

        A in the topology of T by A2, A29, PRE_TOPC:def 2;

        then

         A33: A is open by PRE_TOPC:def 2;

        B in the topology of T by A2, A30, PRE_TOPC:def 2;

        then

         A34: B is open by PRE_TOPC:def 2;

        ( not q in A) & not p in B by A31, A32, XBOOLE_0: 3;

        hence thesis by A31, A33, A34;

      end;

      hence thesis by A3, URYSOHN1:def 7;

    end;

    theorem :: NAGATA_1:16

    for T st T is metrizable holds ex Un be FamilySequence of T st Un is Basis_sigma_locally_finite

    proof

      let T;

      assume

       A1: T is metrizable;

      then

      consider metr be Function of [:the carrier of T, the carrier of T:], REAL such that

       A2: metr is_metric_of the carrier of T and

       A3: ( Family_open_set ( SpaceMetr (the carrier of T,metr))) = the topology of T;

      set PM = ( SpaceMetr (the carrier of T,metr));

      reconsider PM as non empty MetrSpace by A2, PCOMPS_1: 36;

      deffunc BALL( Element of NAT ) = { ( Ball (x,(1 / (2 |^ $1)))) where x be Element of PM : x is Element of PM };

      defpred E[ Element of NAT , set] means $2 = BALL($1);

      

       A4: for k be Element of NAT holds ex y be Subset-Family of T st E[k, y]

      proof

        let k be Element of NAT ;

        set Ak = BALL(k);

        Ak c= ( bool the carrier of T)

        proof

          let B be object;

          assume B in Ak;

          then ex x be Element of PM st B = ( Ball (x,(1 / (2 |^ k)))) & x is Element of PM;

          then B in ( Family_open_set PM) by PCOMPS_1: 29;

          hence thesis by A3;

        end;

        hence thesis;

      end;

      consider FB be sequence of ( bool ( bool the carrier of T)) such that

       A5: for k be Element of NAT holds E[k, (FB . k)] from FUNCT_2:sch 3( A4);

      defpred P[ object, object] means ex W be Subset-Family of T st W = $2 & W is open & W is Cover of T & W is_finer_than (FB . $1) & W is locally_finite;

      set TPM = ( TopSpaceMetr PM);

      

       A6: ( [#] T) = ( [#] TPM) by A2, PCOMPS_2: 4;

      

       A7: for n holds ex PP be Subset-Family of T st PP is_finer_than (FB . n) & PP is Cover of T & PP is open & PP is locally_finite

      proof

        let n;

        ( [#] TPM) c= ( union (FB . n))

        proof

          let x be object;

          assume x in ( [#] TPM);

          then

          reconsider x9 = x as Element of PM;

          ( dist (x9,x9)) = 0 & (2 |^ n) > 0 by METRIC_1: 1, NEWTON: 83;

          then ( dist (x9,x9)) < (1 / (2 |^ n)) by XREAL_1: 139;

          then

           A8: x9 in ( Ball (x9,(1 / (2 |^ n)))) by METRIC_1: 11;

          ( Ball (x9,(1 / (2 |^ n)))) in BALL(n);

          then ( Ball (x9,(1 / (2 |^ n)))) in (FB . n) by A5;

          hence thesis by A8, TARSKI:def 4;

        end;

        then

         A9: (FB . n) is Cover of T by A6, SETFAM_1:def 11;

        for U be Subset of T holds U in (FB . n) implies U is open

        proof

          let U be Subset of T;

          assume U in (FB . n);

          then U in BALL(n) by A5;

          then ex x be Element of PM st U = ( Ball (x,(1 / (2 |^ n)))) & x is Element of PM;

          then U in the topology of T by A3, PCOMPS_1: 29;

          hence thesis by PRE_TOPC:def 2;

        end;

        then (FB . n) is open by TOPS_2:def 1;

        then ex PP be Subset-Family of T st PP is open & PP is Cover of T & PP is_finer_than (FB . n) & PP is locally_finite by A1, A9, PCOMPS_2: 6;

        hence thesis;

      end;

      

       A10: for k be object st k in NAT holds ex y be object st y in ( bool ( bool the carrier of T)) & P[k, y]

      proof

        let k be object;

        assume k in NAT ;

        then

        reconsider k as Element of NAT ;

        ex PP be Subset-Family of T st PP is_finer_than (FB . k) & PP is Cover of T & PP is open & PP is locally_finite by A7;

        hence thesis;

      end;

      consider UC be FamilySequence of T such that

       A11: for x be object st x in NAT holds P[x, (UC . x)] from FUNCT_2:sch 1( A10);

      

       A12: for A be Subset of T st A is open holds for p be Point of T st p in A holds ex B be Subset of T st B in ( Union UC) & p in B & B c= A

      proof

        let A;

        assume A is open;

        then

         A13: A in ( Family_open_set PM) by A3, PRE_TOPC:def 2;

        let p;

        assume

         A14: p in A;

        then

        reconsider p as Element of PM by A13;

        consider r1 such that

         A15: r1 > 0 and

         A16: ( Ball (p,r1)) c= A by A14, A13, PCOMPS_1:def 4;

        consider n be Nat such that

         A17: (1 / (2 |^ n)) <= r1 by A15, PREPOWER: 92;

        

         A18: P[(n + 1), (UC . (n + 1))] by A11;

        then ( union (UC . (n + 1))) = the carrier of T by SETFAM_1: 45;

        then

        consider B be set such that

         A19: p in B and

         A20: B in (UC . (n + 1)) by TARSKI:def 4;

        reconsider B as Subset of PM by A2, A20, PCOMPS_2: 4;

        consider B1 be set such that

         A21: B1 in (FB . (n + 1)) and

         A22: B c= B1 by A18, A20, SETFAM_1:def 2;

        B1 in BALL(+) by A5, A21;

        then

        consider q be Element of PM such that

         A23: B1 = ( Ball (q,(1 / (2 |^ (n + 1))))) and q is Element of PM;

        

         A24: ( dist (q,p)) < (1 / (2 |^ (n + 1))) by A19, A22, A23, METRIC_1: 11;

        now

          let r be Element of PM;

          assume r in B;

          then ( dist (q,r)) < (1 / (2 |^ (n + 1))) by A22, A23, METRIC_1: 11;

          then ( dist (p,r)) <= (( dist (q,p)) + ( dist (q,r))) & (( dist (q,p)) + ( dist (q,r))) < ((1 / (2 |^ (n + 1))) + (1 / (2 |^ (n + 1)))) by A24, METRIC_1: 4, XREAL_1: 8;

          then ( dist (p,r)) < (2 * (1 / (2 |^ (n + 1)))) by XXREAL_0: 2;

          then ( dist (p,r)) < ((1 / ((2 |^ n) * 2)) * 2) by NEWTON: 6;

          then ( dist (p,r)) < (1 / (2 |^ n)) by XCMPLX_1: 92;

          then ( dist (p,r)) < r1 by A17, XXREAL_0: 2;

          hence r in ( Ball (p,r1)) by METRIC_1: 11;

        end;

        then

         A25: B c= ( Ball (p,r1));

        B in ( Union UC) by A20, PROB_1: 12;

        hence thesis by A16, A19, A25, XBOOLE_1: 1;

      end;

      for n holds (UC . n) is locally_finite

      proof

        let n;

         P[n, (UC . n)] by A11;

        hence thesis;

      end;

      then

       A26: UC is sigma_locally_finite;

      ( Union UC) c= the topology of T

      proof

        let u be object;

        assume u in ( Union UC);

        then

        consider k be Nat such that

         A27: u in (UC . k) by PROB_1: 12;

        

         A28: k in NAT by ORDINAL1:def 12;

        reconsider u9 = u as Subset of T by A27;

         P[k, (UC . k)] by A11, A28;

        then u9 is open by A27, TOPS_2:def 1;

        hence thesis by PRE_TOPC:def 2;

      end;

      then ( Union UC) is Basis of T by A12, YELLOW_9: 32;

      then UC is Basis_sigma_locally_finite by A26;

      hence thesis;

    end;

    

     Lm6: for U, A st A is closed holds (U \ A) is open

    proof

      let U, A;

      

       A1: (U /\ (( [#] T) \ A)) = (U /\ (A ` ));

      assume A is closed;

      hence thesis by A1, SUBSET_1: 13;

    end;

    theorem :: NAGATA_1:17

    

     Th17: for U be sequence of ( bool the carrier of T) st (for n holds (U . n) is open) holds ( Union U) is open

    proof

      let U be sequence of ( bool the carrier of T);

      assume

       A1: for n holds (U . n) is open;

      ( rng U) c= the topology of T

      proof

        let u be object;

        assume u in ( rng U);

        then

        consider k be object such that

         A2: k in ( dom U) and

         A3: u = (U . k) by FUNCT_1:def 3;

        reconsider k as Element of NAT by A2;

        (U . k) is open by A1;

        hence thesis by A3, PRE_TOPC:def 2;

      end;

      then ( union ( rng U)) in the topology of T by PRE_TOPC:def 1;

      then ( Union U) in the topology of T by CARD_3:def 4;

      hence thesis by PRE_TOPC:def 2;

    end;

    theorem :: NAGATA_1:18

    

     Th18: (for A, U st A is closed & U is open & A c= U holds ex W be sequence of ( bool the carrier of T) st A c= ( Union W) & ( Union W) c= U & (for n holds ( Cl (W . n)) c= U & (W . n) is open)) implies T is normal

    proof

      assume

       A1: for A, U st A is closed & U is open & A c= U holds ex W be sequence of ( bool the carrier of T) st A c= ( Union W) & ( Union W) c= U & for n holds ( Cl (W . n)) c= U & (W . n) is open;

      for A,B be Subset of T st A <> {} & B <> {} & A is closed & B is closed & A misses B holds ex UA,WB be Subset of T st UA is open & WB is open & A c= UA & B c= WB & UA misses WB

      proof

        let A,B be Subset of T;

        assume that A <> {} and B <> {} and

         A2: A is closed & B is closed and

         A3: A misses B;

        set W = (( [#] T) \ B);

        A c= (B ` ) by A3, SUBSET_1: 23;

        then

        consider Wn be sequence of ( bool the carrier of T) such that

         A4: A c= ( Union Wn) and ( Union Wn) c= W and

         A5: for n holds ( Cl (Wn . n)) c= W & (Wn . n) is open by A1, A2;

        set U = (( [#] T) \ A);

        B c= (A ` ) by A3, SUBSET_1: 23;

        then

        consider Un be sequence of ( bool the carrier of T) such that

         A6: B c= ( Union Un) and ( Union Un) c= U and

         A7: for n holds ( Cl (Un . n)) c= U & (Un . n) is open by A1, A2;

        deffunc UW( Nat) = ((Un . $1) \ ( union { ( Cl (Wn . k)) where k be Element of NAT : k in (( Seg $1) \/ { 0 }) }));

        defpred E2[ Element of NAT , set] means $2 = UW($1);

        

         A8: for k be Element of NAT holds ex y be Subset of T st E2[k, y];

        consider FUW be sequence of ( bool the carrier of T) such that

         A9: for k be Element of NAT holds E2[k, (FUW . k)] from FUNCT_2:sch 3( A8);

        for n holds (FUW . n) is open

        proof

          let n;

          set CLn = { ( Cl (Wn . k)) where k be Element of NAT : k in (( Seg n) \/ { 0 }) };

          now

            let C be object;

            assume C in CLn;

            then ex k be Element of NAT st C = ( Cl (Wn . k)) & k in (( Seg n) \/ { 0 });

            hence C in ( bool the carrier of T);

          end;

          then

          reconsider CLn as Subset-Family of T by TARSKI:def 3;

          deffunc CL( Element of NAT ) = ( Cl (Wn . $1));

          

           A10: (( Seg n) \/ { 0 }) is finite;

          

           A11: { CL(k) where k be Element of NAT : k in (( Seg n) \/ { 0 }) } is finite from FRAENKEL:sch 21( A10);

          now

            let A;

            assume A in CLn;

            then ex k be Element of NAT st A = ( Cl (Wn . k)) & k in (( Seg n) \/ { 0 });

            hence A is closed;

          end;

          then

           A12: CLn is closed by TOPS_2:def 2;

          (Un . n) is open by A7;

          then ((Un . n) \ ( union CLn)) is open by A11, A12, Lm6, TOPS_2: 21;

          hence thesis by A9;

        end;

        then

         A13: ( Union FUW) is open by Th17;

        

         A14: for n holds B misses ( Cl (Wn . n))

        proof

          let n;

          ( Cl (Wn . n)) c= W by A5;

          hence thesis by XBOOLE_1: 63, XBOOLE_1: 79;

        end;

        now

          let b be object;

          assume that

           A15: b in B and

           A16: not b in ( Union FUW);

          consider k be Nat such that

           A17: b in (Un . k) by A6, A15, PROB_1: 12;

          

           A18: k in NAT by ORDINAL1:def 12;

           not b in ( union { ( Cl (Wn . m)) where m be Element of NAT : m in (( Seg k) \/ { 0 }) })

          proof

            assume b in ( union { ( Cl (Wn . m)) where m be Element of NAT : m in (( Seg k) \/ { 0 }) });

            then

            consider CL be set such that

             A19: b in CL and

             A20: CL in { ( Cl (Wn . m)) where m be Element of NAT : m in (( Seg k) \/ { 0 }) } by TARSKI:def 4;

            consider m be Element of NAT such that

             A21: CL = ( Cl (Wn . m)) and m in (( Seg k) \/ { 0 }) by A20;

            B meets ( Cl (Wn . m)) by A15, A19, A21, XBOOLE_0: 3;

            hence contradiction by A14;

          end;

          then b in UW(k) by A17, XBOOLE_0:def 5;

          then b in (FUW . k) by A9, A18;

          hence contradiction by A16, PROB_1: 12;

        end;

        then

         A22: B c= ( Union FUW);

        deffunc WU( Nat) = ((Wn . $1) \ ( union { ( Cl (Un . k)) where k be Element of NAT : k in (( Seg $1) \/ { 0 }) }));

        defpred E1[ Element of NAT , set] means $2 = WU($1);

        

         A23: for k be Element of NAT holds ex y be Subset of T st E1[k, y];

        consider FWU be sequence of ( bool the carrier of T) such that

         A24: for k be Element of NAT holds E1[k, (FWU . k)] from FUNCT_2:sch 3( A23);

        

         A25: ( Union FUW) misses ( Union FWU)

        proof

          assume ( Union FUW) meets ( Union FWU);

          then

          consider f be object such that

           A26: f in ( Union FUW) and

           A27: f in ( Union FWU) by XBOOLE_0: 3;

          consider n be Nat such that

           A28: f in (FUW . n) by A26, PROB_1: 12;

          consider k be Nat such that

           A29: f in (FWU . k) by A27, PROB_1: 12;

          

           A30: n >= k implies (FUW . n) misses (FWU . k)

          proof

            assume that

             A31: n >= k and

             A32: (FUW . n) meets (FWU . k);

            consider w be object such that

             A33: w in (FUW . n) and

             A34: w in (FWU . k) by A32, XBOOLE_0: 3;

            

             A35: k in NAT by ORDINAL1:def 12;

            

             A36: n in NAT by ORDINAL1:def 12;

            w in ((Wn . k) \ ( union { ( Cl (Un . l)) where l be Element of NAT : l in (( Seg k) \/ { 0 }) })) by A24, A34, A35;

            then

             A37: w in (Wn . k) by XBOOLE_0:def 5;

            k = 0 or k in ( Seg k) by FINSEQ_1: 3;

            then k in { 0 } or k in ( Seg k) & ( Seg k) c= ( Seg n) by A31, FINSEQ_1: 5, TARSKI:def 1;

            then k in (( Seg n) \/ { 0 }) by XBOOLE_0:def 3;

            then

             A38: (Wn . k) c= ( Cl (Wn . k)) & ( Cl (Wn . k)) in { ( Cl (Wn . l)) where l be Element of NAT : l in (( Seg n) \/ { 0 }) } by PRE_TOPC: 18;

            w in ((Un . n) \ ( union { ( Cl (Wn . l)) where l be Element of NAT : l in (( Seg n) \/ { 0 }) })) by A9, A33, A36;

            then not w in ( union { ( Cl (Wn . l)) where l be Element of NAT : l in (( Seg n) \/ { 0 }) }) by XBOOLE_0:def 5;

            hence contradiction by A37, A38, TARSKI:def 4;

          end;

          n <= k implies (FUW . n) misses (FWU . k)

          proof

            assume that

             A39: n <= k and

             A40: (FUW . n) meets (FWU . k);

            consider u be object such that

             A41: u in (FUW . n) and

             A42: u in (FWU . k) by A40, XBOOLE_0: 3;

            

             A43: n in NAT by ORDINAL1:def 12;

            

             A44: k in NAT by ORDINAL1:def 12;

            u in ((Un . n) \ ( union { ( Cl (Wn . l)) where l be Element of NAT : l in (( Seg n) \/ { 0 }) })) by A9, A41, A43;

            then

             A45: u in (Un . n) by XBOOLE_0:def 5;

            n = 0 or n in ( Seg n) by FINSEQ_1: 3;

            then n in { 0 } or n in ( Seg n) & ( Seg n) c= ( Seg k) by A39, FINSEQ_1: 5, TARSKI:def 1;

            then n in (( Seg k) \/ { 0 }) by XBOOLE_0:def 3;

            then

             A46: (Un . n) c= ( Cl (Un . n)) & ( Cl (Un . n)) in { ( Cl (Un . l)) where l be Element of NAT : l in (( Seg k) \/ { 0 }) } by PRE_TOPC: 18;

            u in ((Wn . k) \ ( union { ( Cl (Un . l)) where l be Element of NAT : l in (( Seg k) \/ { 0 }) })) by A24, A42, A44;

            then not u in ( union { ( Cl (Un . l)) where l be Element of NAT : l in (( Seg k) \/ { 0 }) }) by XBOOLE_0:def 5;

            hence contradiction by A45, A46, TARSKI:def 4;

          end;

          hence contradiction by A28, A29, A30, XBOOLE_0: 3;

        end;

        for n holds (FWU . n) is open

        proof

          let n;

          set CLn = { ( Cl (Un . k)) where k be Element of NAT : k in (( Seg n) \/ { 0 }) };

          now

            let C be object;

            assume C in CLn;

            then ex k be Element of NAT st C = ( Cl (Un . k)) & k in (( Seg n) \/ { 0 });

            hence C in ( bool the carrier of T);

          end;

          then

          reconsider CLn as Subset-Family of T by TARSKI:def 3;

          deffunc CL( Element of NAT ) = ( Cl (Un . $1));

          

           A47: (( Seg n) \/ { 0 }) is finite;

          

           A48: { CL(k) where k be Element of NAT : k in (( Seg n) \/ { 0 }) } is finite from FRAENKEL:sch 21( A47);

          now

            let A;

            assume A in CLn;

            then ex k be Element of NAT st A = ( Cl (Un . k)) & k in (( Seg n) \/ { 0 });

            hence A is closed;

          end;

          then

           A49: CLn is closed by TOPS_2:def 2;

          (Wn . n) is open by A5;

          then ((Wn . n) \ ( union CLn)) is open by A48, A49, Lm6, TOPS_2: 21;

          hence thesis by A24;

        end;

        then

         A50: ( Union FWU) is open by Th17;

        

         A51: for n holds A misses ( Cl (Un . n))

        proof

          let n;

          ( Cl (Un . n)) c= U by A7;

          hence thesis by XBOOLE_1: 63, XBOOLE_1: 79;

        end;

        now

          let a be object;

          assume that

           A52: a in A and

           A53: not a in ( Union FWU);

          consider k be Nat such that

           A54: a in (Wn . k) by A4, A52, PROB_1: 12;

          

           A55: k in NAT by ORDINAL1:def 12;

           not a in ( union { ( Cl (Un . m)) where m be Element of NAT : m in (( Seg k) \/ { 0 }) })

          proof

            assume a in ( union { ( Cl (Un . m)) where m be Element of NAT : m in (( Seg k) \/ { 0 }) });

            then

            consider CL be set such that

             A56: a in CL and

             A57: CL in { ( Cl (Un . m)) where m be Element of NAT : m in (( Seg k) \/ { 0 }) } by TARSKI:def 4;

            consider m be Element of NAT such that

             A58: CL = ( Cl (Un . m)) and m in (( Seg k) \/ { 0 }) by A57;

            A meets ( Cl (Un . m)) by A52, A56, A58, XBOOLE_0: 3;

            hence contradiction by A51;

          end;

          then a in WU(k) by A54, XBOOLE_0:def 5;

          then a in (FWU . k) by A24, A55;

          hence contradiction by A53, PROB_1: 12;

        end;

        then A c= ( Union FWU);

        hence thesis by A22, A25, A13, A50;

      end;

      hence thesis;

    end;

    theorem :: NAGATA_1:19

    

     Th19: for T st T is regular holds for Bn be FamilySequence of T st ( Union Bn) is Basis of T holds for U be Subset of T, p be Point of T st U is open & p in U holds ex O be Subset of T st p in O & ( Cl O) c= U & O in ( Union Bn)

    proof

      let T;

      assume

       A1: T is regular;

      let Bn be FamilySequence of T;

      assume

       A2: ( Union Bn) is Basis of T;

      for U, p st U is open & p in U holds ex O be Subset of T st p in O & ( Cl O) c= U & O in ( Union Bn)

      proof

        let U, p;

        assume that U is open and

         A3: p in U;

        now

          per cases ;

            suppose

             A4: U = the carrier of T;

            consider O be Subset of T such that

             A5: O in ( Union Bn) & p in O and O c= U by A2, A3, YELLOW_9: 31;

            take O;

            ( Cl O) c= U by A4;

            hence thesis by A5;

          end;

            suppose U <> the carrier of T;

            then U c< the carrier of T by XBOOLE_0:def 8;

            then

             A6: (U ` ) <> {} by XBOOLE_1: 105;

            p in ((U ` ) ` ) by A3;

            then

            consider W,V be Subset of T such that

             A7: W is open and

             A8: V is open and

             A9: p in W and

             A10: (U ` ) c= V and

             A11: W misses V by A1, A6;

            consider O be Subset of T such that

             A12: O in ( Union Bn) & p in O and

             A13: O c= W by A2, A7, A9, YELLOW_9: 31;

            W c= (V ` ) by A11, SUBSET_1: 23;

            then O c= (V ` ) by A13;

            then ( Cl O) c= ( Cl (V ` )) by PRE_TOPC: 19;

            then

             A14: ( Cl O) c= (V ` ) by A8, PRE_TOPC: 22;

            take O;

            (V ` ) c= U by A10, SUBSET_1: 17;

            hence thesis by A12, A14, XBOOLE_1: 1;

          end;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: NAGATA_1:20

    for T st T is regular & ex Bn be FamilySequence of T st Bn is Basis_sigma_locally_finite holds T is normal

    proof

      let T;

      assume that

       A1: T is regular and

       A2: ex Bn be FamilySequence of T st Bn is Basis_sigma_locally_finite;

      consider Bn be FamilySequence of T such that

       A3: Bn is Basis_sigma_locally_finite by A2;

      

       A4: ( Union Bn) is Basis of T by A3;

      

       A5: Bn is sigma_locally_finite by A3;

      for A, U st A is closed & U is open & A c= U holds ex W be sequence of ( bool the carrier of T) st A c= ( Union W) & ( Union W) c= U & for n holds ( Cl (W . n)) c= U & (W . n) is open

      proof

        let A, U;

        assume that A is closed and U is open and

         A6: A c= U;

        deffunc B( object) = ( union { O where O be Subset of T : O in (Bn . $1) & ( Cl O) c= U });

        

         A7: for k be object st k in NAT holds B(k) in ( bool the carrier of T)

        proof

          let k be object;

          assume k in NAT ;

          then

          reconsider k as Element of NAT ;

          now

            let bu be object;

            assume bu in B(k);

            then

            consider b be set such that

             A8: bu in b and

             A9: b in { O where O be Subset of T : O in (Bn . k) & ( Cl O) c= U } by TARSKI:def 4;

            ex O be Subset of T st b = O & O in (Bn . k) & ( Cl O) c= U by A9;

            hence bu in the carrier of T by A8;

          end;

          then B(k) c= the carrier of T;

          hence thesis;

        end;

        consider BU be sequence of ( bool the carrier of T) such that

         A10: for k be object st k in NAT holds (BU . k) = B(k) from FUNCT_2:sch 2( A7);

         A11:

        now

          let n;

          set BUn = { O where O be Subset of T : O in (Bn . n) & ( Cl O) c= U };

          BUn c= ( bool the carrier of T)

          proof

            let b be object;

            assume b in BUn;

            then ex O be Subset of T st b = O & O in (Bn . n) & ( Cl O) c= U;

            hence thesis;

          end;

          then

          reconsider BUn as Subset-Family of T;

          

           A12: BUn c= (Bn . n)

          proof

            let b be object;

            assume b in BUn;

            then ex O be Subset of T st b = O & O in (Bn . n) & ( Cl O) c= U;

            hence thesis;

          end;

          (Bn . n) is locally_finite by A5;

          then

           A13: ( Cl ( union BUn)) = ( union ( clf BUn)) by A12, PCOMPS_1: 9, PCOMPS_1: 20;

          

           A14: ( Cl ( union BUn)) c= U

          proof

            let ClBu be object;

            assume ClBu in ( Cl ( union BUn));

            then

            consider ClB be set such that

             A15: ClBu in ClB and

             A16: ClB in ( clf BUn) by A13, TARSKI:def 4;

            reconsider ClB as Subset of T by A16;

            consider B be Subset of T such that

             A17: ( Cl B) = ClB and

             A18: B in BUn by A16, PCOMPS_1:def 2;

            ex Q be Subset of T st B = Q & Q in (Bn . n) & ( Cl Q) c= U by A18;

            hence thesis by A15, A17;

          end;

          BUn c= the topology of T

          proof

            let B be object;

            assume B in BUn;

            then

            consider Q be Subset of T such that

             A19: B = Q and

             A20: Q in (Bn . n) and ( Cl Q) c= U;

            

             A21: ( Union Bn) c= the topology of T by A4, TOPS_2: 64;

            Q in ( Union Bn) by A20, PROB_1: 12;

            hence thesis by A19, A21;

          end;

          then ( union BUn) in the topology of T by PRE_TOPC:def 1;

          then ( union BUn) is open by PRE_TOPC:def 2;

          hence (BU . n) is open & ( Cl (BU . n)) c= U by A10, A14;

        end;

        

         A22: ( Union BU) c= U

        proof

          let bu be object;

          assume bu in ( Union BU);

          then

          consider k be Nat such that

           A23: bu in (BU . k) by PROB_1: 12;

          

           A24: k in NAT by ORDINAL1:def 12;

          bu in ( union { O where O be Subset of T : O in (Bn . k) & ( Cl O) c= U }) by A10, A23, A24;

          then

          consider b be set such that

           A25: bu in b and

           A26: b in { O where O be Subset of T : O in (Bn . k) & ( Cl O) c= U } by TARSKI:def 4;

          consider O be Subset of T such that

           A27: b = O and O in (Bn . k) and

           A28: ( Cl O) c= U by A26;

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

          then b c= U by A27, A28;

          hence thesis by A25;

        end;

        for a be object st a in A holds a in ( Union BU)

        proof

          let a be object;

          assume a in A;

          then

          consider Q be Subset of T such that

           A29: a in Q and

           A30: ( Cl Q) c= U and

           A31: Q in ( Union Bn) by A1, A4, A6, Th19;

          consider k be Nat such that

           A32: Q in (Bn . k) by A31, PROB_1: 12;

          

           A33: k in NAT by ORDINAL1:def 12;

          Q in { O where O be Subset of T : O in (Bn . k) & ( Cl O) c= U } by A30, A32;

          then a in B(k) by A29, TARSKI:def 4;

          then a in (BU . k) by A10, A33;

          hence thesis by PROB_1: 12;

        end;

        then A c= ( Union BU);

        hence thesis by A22, A11;

      end;

      hence thesis by Th18;

    end;

    

     Lm7: for r be Real, A be Point of RealSpace st r > 0 holds A in ( Ball (A,r))

    proof

      let r be Real, A be Point of RealSpace ;

      reconsider A9 = A as Real;

      

       A1: |.(A9 - A9).| = 0 by ABSVALUE: 2;

      assume r > 0 ;

      then ( dist (A,A)) < r by A1, TOPMETR: 11;

      hence thesis by METRIC_1: 11;

    end;

    definition

      let T;

      let F,G be RealMap of T;

      :: original: +

      redefine

      :: NAGATA_1:def7

      func F + G -> RealMap of T means

      : Def7: for t be Element of T holds (it . t) = ((F . t) + (G . t));

      coherence

      proof

        (F + G) is Function of the carrier of T, REAL ;

        hence thesis;

      end;

      compatibility

      proof

        let m be RealMap of T;

        thus m = (F + G) implies for p be Element of T holds (m . p) = ((F . p) + (G . p)) by VALUED_1: 1;

        

         A1: ( dom (F + G)) = (( dom F) /\ ( dom G)) by VALUED_1:def 1

        .= (the carrier of T /\ ( dom G)) by FUNCT_2:def 1

        .= (the carrier of T /\ the carrier of T) by FUNCT_2:def 1;

        assume

         A2: for p be Element of T holds (m . p) = ((F . p) + (G . p));

         A3:

        now

          let x be object;

          assume

           A4: x in ( dom m);

          

          hence (m . x) = ((F . x) + (G . x)) by A2

          .= ((F + G) . x) by A1, A4, VALUED_1:def 1;

        end;

        ( dom m) = the carrier of T by FUNCT_2:def 1;

        hence thesis by A1, A3, FUNCT_1: 2;

      end;

    end

    theorem :: NAGATA_1:21

    for f be RealMap of T st f is continuous holds for F be RealMap of [:T, T:] st for x,y be Element of T holds (F . (x,y)) = |.((f . x) - (f . y)).| holds F is continuous

    proof

      let f be RealMap of T such that

       A1: f is continuous;

      set TT = [:T, T:];

      set cT = the carrier of T;

      reconsider f9 = f as Function of T, R^1 by TOPMETR: 17;

      let F be RealMap of [:T, T:] such that

       A2: for x,y be Element of T holds (F . (x,y)) = |.((f . x) - (f . y)).|;

      reconsider F9 = F as Function of [:T, T:], R^1 by TOPMETR: 17;

      

       A3: f9 is continuous by A1, JORDAN5A: 27;

      now

        let tt be Point of TT;

        tt in the carrier of TT;

        then tt in [:cT, cT:] by BORSUK_1:def 2;

        then

        consider t1,t2 be object such that

         A4: t1 in cT & t2 in cT and

         A5: [t1, t2] = tt by ZFMISC_1:def 2;

        reconsider t1, t2 as Point of T by A4;

        for R be Subset of R^1 st R is open & (F9 . tt) in R holds ex H be Subset of TT st H is open & tt in H & (F9 .: H) c= R

        proof

          reconsider ft1 = (f . t1), ft2 = (f . t2) as Point of RealSpace by METRIC_1:def 13;

          reconsider Ftt = (F . tt) as Point of RealSpace by METRIC_1:def 13;

          let R be Subset of R^1 ;

          assume R is open & (F9 . tt) in R;

          then

          consider r be Real such that

           A6: r > 0 and

           A7: ( Ball (Ftt,r)) c= R by TOPMETR: 15, TOPMETR:def 6;

          reconsider r9 = r as Real;

          reconsider A = ( Ball (ft1,(r9 / 2))), B = ( Ball (ft2,(r9 / 2))) as Subset of R^1 by METRIC_1:def 13, TOPMETR: 17;

          

           A8: A is open & f9 is_continuous_at t1 by A3, TMAP_1: 50, TOPMETR: 14, TOPMETR:def 6;

          (f . t1) in A by A6, Lm7, XREAL_1: 139;

          then

          consider T1 be Subset of T such that

           A9: T1 is open and

           A10: t1 in T1 and

           A11: (f9 .: T1) c= A by A8, TMAP_1: 43;

          

           A12: B is open & f9 is_continuous_at t2 by A3, TMAP_1: 50, TOPMETR: 14, TOPMETR:def 6;

          (f . t2) in B by A6, Lm7, XREAL_1: 139;

          then

          consider T2 be Subset of T such that

           A13: T2 is open and

           A14: t2 in T2 and

           A15: (f9 .: T2) c= B by A12, TMAP_1: 43;

          (F . tt) = (F . (t1,t2)) by A5;

          then

           A16: |.((f9 . t1) - (f9 . t2)).| = (F . tt) by A2;

          

           A17: (F .: [:T1, T2:]) c= R

          proof

            let Fxy be object;

            assume Fxy in (F .: [:T1, T2:]);

            then

            consider xy be object such that xy in ( dom F) and

             A18: xy in [:T1, T2:] and

             A19: Fxy = (F . xy) by FUNCT_1:def 6;

            consider x,y be object such that

             A20: x in T1 and

             A21: y in T2 and

             A22: xy = [x, y] by A18, ZFMISC_1:def 2;

            reconsider x, y as Point of T by A20, A21;

            reconsider fx = (f . x), fy = (f . y) as Point of RealSpace by METRIC_1:def 13;

            y in cT;

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

            then (f . y) in (f .: T2) by A21, FUNCT_1:def 6;

            then

             A23: ( dist (fy,ft2)) < (r9 / 2) by A15, METRIC_1: 11;

            reconsider Fxy1 = (F . [x, y]) as Point of RealSpace by METRIC_1:def 13;

            

             A24: |.((f . x) - (f . y)).| = (F . (x,y)) by A2;

            then (F . [x, y]) <= (( |.((f . x) - (f . t1)).| + (F . tt)) + |.((f . t2) - (f . y)).|) by A16, Lm2;

            then (F . [x, y]) <= (( |.((f . x) - (f . t1)).| + (F . tt)) + ( dist (ft2,fy))) by TOPMETR: 11;

            then

             A25: ((F . [x, y]) + 0 ) <= (((F . tt) + ( dist (fx,ft1))) + ( dist (ft2,fy))) by TOPMETR: 11;

            (F . tt) <= (( |.((f . t1) - (f . x)).| + (F . [x, y])) + |.((f . y) - (f . t2)).|) by A16, A24, Lm2;

            then (F . tt) <= ((( dist (fx,ft1)) + (F . [x, y])) + |.((f . y) - (f . t2)).|) by TOPMETR: 11;

            then

             A26: (F . tt) <= (((F . [x, y]) + ( dist (fx,ft1))) + ( dist (fy,ft2))) by TOPMETR: 11;

            x in cT;

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

            then (f . x) in (f .: T1) by A20, FUNCT_1:def 6;

            then ( dist (fx,ft1)) < (r9 / 2) by A11, METRIC_1: 11;

            then

             A27: (( dist (fx,ft1)) + ( dist (fy,ft2))) < ((r9 / 2) + (r9 / 2)) by A23, XREAL_1: 8;

            then ((F . [x, y]) + (( dist (fx,ft1)) + ( dist (fy,ft2)))) < ((F . [x, y]) + r9) by XREAL_1: 8;

            then (F . tt) < ( - (( - (F . [x, y])) - r9)) by A26, XXREAL_0: 2;

            then (( - (F . tt)) - 0 ) > (( - r9) - (F . [x, y])) by XREAL_1: 26;

            then

             A28: (( - (F . tt)) + (F . [x, y])) > (( - r9) + 0 ) by XREAL_1: 21;

            ((F . tt) + (( dist (fx,ft1)) + ( dist (ft2,fy)))) < ((F . tt) + r9) by A27, XREAL_1: 8;

            then ((F . [x, y]) + 0 ) < ((F . tt) + r9) by A25, XXREAL_0: 2;

            then ((F . [x, y]) - (F . tt)) < (r9 - 0 ) by XREAL_1: 21;

            then |.((F . [x, y]) - (F . tt)).| < r9 by A28, SEQ_2: 1;

            then ( dist (Ftt,Fxy1)) < r9 by TOPMETR: 11;

            then Fxy1 in ( Ball (Ftt,r)) by METRIC_1: 11;

            hence thesis by A7, A19, A22;

          end;

          tt in [:T1, T2:] by A5, A10, A14, ZFMISC_1:def 2;

          hence thesis by A9, A13, A17, BORSUK_1: 6;

        end;

        hence F9 is_continuous_at tt by TMAP_1: 43;

      end;

      then F9 is continuous by TMAP_1: 50;

      hence thesis by JORDAN5A: 27;

    end;

    theorem :: NAGATA_1:22

    

     Th22: for F,G be RealMap of T st F is continuous & G is continuous holds (F + G) is continuous

    proof

      let F,G be RealMap of T such that

       A1: F is continuous and

       A2: G is continuous;

      reconsider F9 = F, G9 = G, FG9 = (F + G) as Function of T, R^1 by TOPMETR: 17;

      

       A3: G9 is continuous by A2, JORDAN5A: 27;

      

       A4: F9 is continuous by A1, JORDAN5A: 27;

      now

        let t be Point of T;

        for R be Subset of R^1 st R is open & (FG9 . t) in R holds ex H be Subset of T st H is open & t in H & (FG9 .: H) c= R

        proof

          reconsider Ft = (F . t), Gt = (G . t), FGt = ((F + G) . t) as Point of RealSpace by METRIC_1:def 13;

          let R be Subset of R^1 ;

          assume R is open & (FG9 . t) in R;

          then

          consider r be Real such that

           A5: r > 0 and

           A6: ( Ball (FGt,r)) c= R by TOPMETR: 15, TOPMETR:def 6;

          reconsider r9 = r as Real;

          reconsider A = ( Ball (Ft,(r9 / 2))), B = ( Ball (Gt,(r9 / 2))) as Subset of R^1 by METRIC_1:def 13, TOPMETR: 17;

          

           A7: A is open & F9 is_continuous_at t by A4, TMAP_1: 50, TOPMETR: 14, TOPMETR:def 6;

          (F9 . t) in A by A5, Lm7, XREAL_1: 139;

          then

          consider AT be Subset of T such that

           A8: AT is open and

           A9: t in AT and

           A10: (F9 .: AT) c= A by A7, TMAP_1: 43;

          

           A11: B is open & G9 is_continuous_at t by A3, TMAP_1: 50, TOPMETR: 14, TOPMETR:def 6;

          (G . t) in B by A5, Lm7, XREAL_1: 139;

          then

          consider BT be Subset of T such that

           A12: BT is open and

           A13: t in BT and

           A14: (G9 .: BT) c= B by A11, TMAP_1: 43;

          

           A15: ((F + G) .: (AT /\ BT)) c= R

          proof

            let FGx be object;

            assume FGx in ((F + G) .: (AT /\ BT));

            then

            consider x be object such that

             A16: x in ( dom (F + G)) and

             A17: x in (AT /\ BT) and

             A18: FGx = ((F + G) . x) by FUNCT_1:def 6;

            reconsider x as Point of T by A16;

            reconsider Fx = (F . x), Gx = (G . x), FGx9 = ((F + G) . x) as Point of RealSpace by METRIC_1:def 13;

            ( dom G) = the carrier of T & x in BT by A17, FUNCT_2:def 1, XBOOLE_0:def 4;

            then (G . x) in (G .: BT) by FUNCT_1:def 6;

            then ( dist (Gx,Gt)) < (r9 / 2) by A14, METRIC_1: 11;

            then

             A19: |.((G . x) - (G . t)).| < (r9 / 2) by TOPMETR: 11;

            then

             A20: ( - (r9 / 2)) < ((G . x) - (G . t)) by SEQ_2: 1;

            ( dom F) = the carrier of T & x in AT by A17, FUNCT_2:def 1, XBOOLE_0:def 4;

            then (F . x) in (F .: AT) by FUNCT_1:def 6;

            then ( dist (Fx,Ft)) < (r9 / 2) by A10, METRIC_1: 11;

            then

             A21: |.((F . x) - (F . t)).| < (r9 / 2) by TOPMETR: 11;

            then ( - (r9 / 2)) < ((F . x) - (F . t)) by SEQ_2: 1;

            then (( - (r9 / 2)) + ( - (r9 / 2))) < (((F . x) - (F . t)) + ((G . x) - (G . t))) by A20, XREAL_1: 8;

            then

             A22: ( - r9) < (((F . x) + (G . x)) - ((F . t) + (G . t)));

            

             A23: ((G . x) - (G . t)) < (r9 / 2) by A19, SEQ_2: 1;

            ((F . x) - (F . t)) < (r9 / 2) by A21, SEQ_2: 1;

            then (((F . x) - (F . t)) + ((G . x) - (G . t))) < ((r9 / 2) + (r9 / 2)) by A23, XREAL_1: 8;

            then |.(((F . x) + (G . x)) - ((F . t) + (G . t))).| < r9 by A22, SEQ_2: 1;

            then |.(((F + G) . x) - ((F . t) + (G . t))).| < r9 by Def7;

            then |.(((F + G) . x) - ((F + G) . t)).| < r9 by Def7;

            then ( dist (FGt,FGx9)) < r9 by TOPMETR: 11;

            then FGx9 in ( Ball (FGt,r)) by METRIC_1: 11;

            hence thesis by A6, A18;

          end;

          t in (AT /\ BT) by A9, A13, XBOOLE_0:def 4;

          hence thesis by A8, A12, A15;

        end;

        hence FG9 is_continuous_at t by TMAP_1: 43;

      end;

      then FG9 is continuous by TMAP_1: 50;

      hence thesis by JORDAN5A: 27;

    end;

    theorem :: NAGATA_1:23

    

     Th23: for ADD be BinOp of ( Funcs (the carrier of T, REAL )) st (for f1,f2 be RealMap of T holds (ADD . (f1,f2)) = (f1 + f2)) holds ADD is having_a_unity & ADD is commutative associative

    proof

      set F = ( Funcs (the carrier of T, REAL ));

      let ADD be BinOp of ( Funcs (the carrier of T, REAL )) such that

       A1: for f1,f2 be RealMap of T holds (ADD . (f1,f2)) = (f1 + f2);

      ex map9 be Element of F st map9 is_a_unity_wrt ADD

      proof

        reconsider map0 = (the carrier of T --> ( In ( 0 , REAL ))) as RealMap of T;

        reconsider map09 = map0 as Element of F by FUNCT_2: 8;

        take map09;

        now

          let f be Element of F;

          now

            let x be Element of T;

            ((f + map09) . x) = ((f . x) + (map09 . x)) by Def7;

            then ((f + map09) . x) = ((f . x) + 0 ) by FUNCOP_1: 7;

            hence ((f + map09) . x) = (f . x);

          end;

          then (f + map09) = f by FUNCT_2: 63;

          hence (ADD . (map0,f)) = f & (ADD . (f,map0)) = f by A1;

        end;

        hence thesis by BINOP_1: 3;

      end;

      hence ADD is having_a_unity by SETWISEO:def 2;

      thus ADD is commutative

      proof

        let f1,f2 be Element of F;

        (ADD . (f1,f2)) = (f1 + f2) by A1;

        hence thesis by A1;

      end;

      thus ADD is associative

      proof

        let f1,f2,f3 be Element of F;

        reconsider ADD12 = (ADD . (f1,f2)), ADD23 = (ADD . (f2,f3)) as RealMap of T by FUNCT_2: 66;

        

         A2: (ADD12 + f3) = (ADD . (ADD12,f3)) by A1;

        now

          let t be Element of T;

          ((f1 + (f2 + f3)) . t) = ((f1 . t) + ((f2 + f3) . t)) & ((f2 + f3) . t) = ((f2 . t) + (f3 . t)) by Def7;

          then ((f1 + (f2 + f3)) . t) = (((f1 . t) + (f2 . t)) + (f3 . t));

          then ((f1 + (f2 + f3)) . t) = (((f1 + f2) . t) + (f3 . t)) by Def7;

          hence ((f1 + (f2 + f3)) . t) = (((f1 + f2) + f3) . t) by Def7;

        end;

        then

         A3: (f1 + (f2 + f3)) = ((f1 + f2) + f3) by FUNCT_2: 63;

        (f1 + (f2 + f3)) = (f1 + ADD23) by A1;

        then (f1 + ADD23) = (ADD12 + f3) by A1, A3;

        hence thesis by A1, A2;

      end;

    end;

    theorem :: NAGATA_1:24

    

     Th24: for ADD be BinOp of ( Funcs (the carrier of T, REAL )) st (for f1,f2 be RealMap of T holds (ADD . (f1,f2)) = (f1 + f2)) holds for map9 be Element of ( Funcs (the carrier of T, REAL )) st map9 is_a_unity_wrt ADD holds map9 is continuous

    proof

      let ADD be BinOp of ( Funcs (the carrier of T, REAL )) such that

       A1: for f1,f2 be RealMap of T holds (ADD . (f1,f2)) = (f1 + f2);

      set F = ( Funcs (the carrier of T, REAL ));

      let map9 be Element of F such that

       A2: map9 is_a_unity_wrt ADD;

      

       A3: for x be Point of T holds (map9 . x) = 0

      proof

        assume ex x be Point of T st (map9 . x) <> 0 ;

        then

        consider x be Point of T such that

         A4: (map9 . x) <> 0 ;

        (ADD . (map9,map9)) = map9 by A2, BINOP_1: 3;

        then (map9 + map9) = map9 by A1;

        then ((map9 . x) + (map9 . x)) = (map9 . x) by Def7;

        hence thesis by A4;

      end;

      reconsider map99 = map9 as Function of T, R^1 by TOPMETR: 17;

      for A be Subset of T holds (map99 .: ( Cl A)) c= ( Cl (map99 .: A) qua Subset of R^1 )

      proof

        let A be Subset of T;

        let mCla be object;

        assume mCla in (map99 .: ( Cl A));

        then

         A5: ex Cla be object st Cla in ( dom map9) & Cla in ( Cl A) & mCla = (map99 . Cla) by FUNCT_1:def 6;

        then A <> ( {} T) by PRE_TOPC: 22;

        then

        consider a be object such that

         A6: a in A by XBOOLE_0:def 1;

        reconsider a as Element of T by A6;

        ( dom map9) = the carrier of T & (map9 . a) = 0 by A3, FUNCT_2:def 1;

        then 0 in (map9 .: A) by A6, FUNCT_1:def 6;

        then

         A7: mCla in (map9 .: A) by A3, A5;

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

        hence thesis by A7;

      end;

      then map99 is continuous by TOPS_2: 45;

      hence thesis by JORDAN5A: 27;

    end;

    definition

      let A,B be non empty set;

      let F be Function of A, ( Funcs (A,B));

      :: NAGATA_1:def8

      func F Toler -> Function of A, B means

      : Def8: for p be Element of A holds (it . p) = ((F . p) . p);

      existence

      proof

        deffunc IT( Element of A) = ((F . $1) . $1);

        defpred P[ Element of A, set] means $2 = IT($1);

        

         A1: for x be Element of A holds ex y be Element of B st P[x, y]

        proof

          let x be Element of A;

          reconsider Funx = (F . x) as Function of A, B by FUNCT_2: 66;

          (Funx . x) in B;

          hence thesis;

        end;

        consider F be Function of A, B such that

         A2: for x be Element of A holds P[x, (F . x)] from FUNCT_2:sch 3( A1);

        take F;

        thus thesis by A2;

      end;

      uniqueness

      proof

        now

          let IT1,IT2 be Function of A, B such that

           A3: for x be Element of A holds (IT1 . x) = ((F . x) . x) & for x be Element of A holds (IT2 . x) = ((F . x) . x);

          now

            let x be Element of A;

            (IT1 . x) = ((F . x) . x) by A3;

            hence (IT1 . x) = (IT2 . x) by A3;

          end;

          hence IT1 = IT2 by FUNCT_2: 63;

        end;

        hence thesis;

      end;

    end

    theorem :: NAGATA_1:25

    for ADD be BinOp of ( Funcs (the carrier of T, REAL )) st (for f1,f2 be RealMap of T holds (ADD . (f1,f2)) = (f1 + f2)) holds for F be FinSequence of ( Funcs (the carrier of T, REAL )) st for n st 0 <> n & n <= ( len F) holds (F . n) is continuous RealMap of T holds (ADD "**" F) is continuous RealMap of T

    proof

      let ADD be BinOp of ( Funcs (the carrier of T, REAL )) such that

       A1: for f1,f2 be RealMap of T holds (ADD . (f1,f2)) = (f1 + f2);

      set Fu = ( Funcs (the carrier of T, REAL ));

      let F be FinSequence of ( Funcs (the carrier of T, REAL )) such that

       A2: for n st 0 <> n & n <= ( len F) holds (F . n) is continuous RealMap of T;

      reconsider ADDF = (ADD "**" F) as RealMap of T by FUNCT_2: 66;

      now

        per cases ;

          suppose

           A3: ( len F) = 0 ;

          

           A4: ADD is having_a_unity by A1, Th23;

          then ex x be Element of Fu st x is_a_unity_wrt ADD by SETWISEO:def 2;

          then

           A5: ( the_unity_wrt ADD) is_a_unity_wrt ADD by BINOP_1:def 8;

          ADDF = ( the_unity_wrt ADD) by A3, A4, FINSOP_1:def 1;

          hence thesis by A1, A5, Th24;

        end;

          suppose

           A6: ( len F) <> 0 ;

          

           A7: ( len F) >= 1

          proof

            assume ( len F) < 1;

            then ( len F) < (1 + 0 );

            hence thesis by A6, NAT_1: 13;

          end;

          then

          consider f be sequence of Fu such that

           A8: (f . 1) = (F . 1) and

           A9: for n be Nat st 0 <> n & n < ( len F) holds (f . (n + 1)) = (ADD . ((f . n),(F . (n + 1)))) and

           A10: (ADD "**" F) = (f . ( len F)) by FINSOP_1: 1;

          defpred Con[ Nat] means $1 <= ( len F) implies (f . $1) is continuous RealMap of T;

          

           A11: for n be Nat st n >= 1 holds Con[n] implies Con[(n + 1)]

          proof

            let n be Nat such that

             A12: n >= 1 and

             A13: Con[n];

            assume

             A14: (n + 1) <= ( len F);

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

            

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

            then n < ( len F) by A14, XXREAL_0: 2;

            then

             A16: (f . (n + 1)) = (ADD . ((f . n),(F . (n + 1)))) by A9, A12;

            (1 + 0 ) <= (n + 1) by A12, XREAL_1: 8;

            then (n + 1) in ( Seg ( len F)) by A14, FINSEQ_1: 1;

            then (n + 1) in ( dom F) by FINSEQ_1:def 3;

            then (F . (n + 1)) in ( rng F) by FUNCT_1:def 3;

            then

            reconsider fn = (f . n), Fn1 = (F . (n + 1)) as RealMap of T by FUNCT_2: 66;

            Fn1 is continuous by A2, A14;

            then (fn + Fn1) is continuous by A13, A14, A15, Th22, XXREAL_0: 2;

            hence thesis by A1, A16;

          end;

          

           A17: Con[1] by A2, A8;

          for n be Nat st n >= 1 holds Con[n] from NAT_1:sch 8( A17, A11);

          hence thesis by A7, A10;

        end;

      end;

      hence thesis;

    end;

    theorem :: NAGATA_1:26

    for F be Function of the carrier of T, ( Funcs (the carrier of T,the carrier of T1)) st for p be Point of T holds (F . p) is continuous Function of T, T1 holds for S be Function of the carrier of T, ( bool the carrier of T) st for p be Point of T holds p in (S . p) & (S . p) is open & for p,q be Point of T st p in (S . q) holds ((F . p) . p) = ((F . q) . p) holds (F Toler ) is continuous

    proof

      let F be Function of the carrier of T, ( Funcs (the carrier of T,the carrier of T1)) such that

       A1: for p holds (F . p) is continuous Function of T, T1;

      let S be Function of the carrier of T, ( bool the carrier of T) such that

       A2: for p holds p in (S . p) & (S . p) is open & for p, q st p in (S . q) holds ((F . p) . p) = ((F . q) . p);

      now

        let t be Point of T;

        for R be Subset of T1 st R is open & ((F Toler ) . t) in R holds ex H be Subset of T st H is open & t in H & ((F Toler ) .: H) c= R

        proof

          reconsider Ft = (F . t) as Function of T, T1 by A1;

          let R be Subset of T1 such that

           A3: R is open and

           A4: ((F Toler ) . t) in R;

          Ft is continuous by A1;

          then

           A5: Ft is_continuous_at t by TMAP_1: 50;

          (Ft . t) in R by A4, Def8;

          then

          consider A be Subset of T such that

           A6: A is open & t in A and

           A7: (Ft .: A) c= R by A3, A5, TMAP_1: 43;

          set H = (A /\ (S . t));

          

           A8: ((F Toler ) .: H) c= R

          proof

            let FSh be object;

            assume FSh in ((F Toler ) .: H);

            then

            consider h be object such that

             A9: h in ( dom (F Toler )) and

             A10: h in H and

             A11: FSh = ((F Toler ) . h) by FUNCT_1:def 6;

            reconsider h9 = h as Point of T by A9;

            h9 in (S . t) & FSh = ((F . h9) . h9) by A10, A11, Def8, XBOOLE_0:def 4;

            then

             A12: FSh = (Ft . h9) by A2;

            

             A13: the carrier of T = ( dom Ft) by FUNCT_2:def 1;

            h9 in A by A10, XBOOLE_0:def 4;

            then FSh in (Ft .: A) by A12, A13, FUNCT_1:def 6;

            hence thesis by A7;

          end;

          take H;

          (S . t) is open & t in (S . t) by A2;

          hence thesis by A6, A8, XBOOLE_0:def 4;

        end;

        hence (F Toler ) is_continuous_at t by TMAP_1: 43;

      end;

      hence thesis by TMAP_1: 50;

    end;

    reserve m for Function of [:the carrier of T, the carrier of T:], REAL ;

    definition

      let X, r;

      let f be Function of X, REAL ;

      deffunc M( Element of X) = ( min (r,(f . $1)));

      :: NAGATA_1:def9

      func min (r,f) -> Function of X, REAL means

      : Def9: for x st x in X holds (it . x) = ( min (r,(f . x)));

      existence

      proof

        defpred P[ object, object] means ex a be Element of X st a = $1 & $2 = M(a);

        

         A1: for x be object st x in X holds ex y be object st y in REAL & P[x, y]

        proof

          let x be object;

          assume x in X;

          then

          reconsider x as Element of X;

          ( min (r,(f . x))) is Element of REAL by XREAL_0:def 1;

          hence thesis;

        end;

        consider Min be Function of X, REAL such that

         A2: for x be object st x in X holds P[x, (Min . x)] from FUNCT_2:sch 1( A1);

        take Min;

        let x;

        assume x in X;

        then P[x, (Min . x)] by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let M1,M2 be Function of X, REAL ;

        assume that

         A3: for x st x in X holds (M1 . x) = ( min (r,(f . x))) and

         A4: for x st x in X holds (M2 . x) = ( min (r,(f . x)));

        now

          let x be object such that

           A5: x in X;

          reconsider y = x as Element of X by A5;

          (M1 . x) = M(y) by A3, A5;

          hence (M1 . x) = (M2 . x) by A4, A5;

        end;

        hence M1 = M2 by FUNCT_2: 12;

      end;

    end

    theorem :: NAGATA_1:27

    for r be Real, f be RealMap of T st f is continuous holds ( min (r,f)) is continuous

    proof

      let r be Real, f be RealMap of T such that

       A1: f is continuous;

      reconsider f9 = f, mf9 = ( min (r,f)) as Function of T, R^1 by TOPMETR: 17;

      

       A2: f9 is continuous by A1, JORDAN5A: 27;

      now

        let t be Point of T;

        for R be Subset of R^1 st R is open & (mf9 . t) in R holds ex U be Subset of T st U is open & t in U & (mf9 .: U) c= R

        proof

          reconsider ft = (f . t) as Point of RealSpace by METRIC_1:def 13;

          let R be Subset of R^1 such that

           A3: R is open and

           A4: (mf9 . t) in R;

          now

            per cases ;

              suppose

               A5: (f . t) <= r;

              then (f . t) = ( min (r,(f . t))) by XXREAL_0:def 9;

              then ft in R by A4, Def9;

              then

              consider s be Real such that

               A6: s > 0 and

               A7: ( Ball (ft,s)) c= R by A3, TOPMETR: 15, TOPMETR:def 6;

              reconsider s9 = s as Real;

              reconsider B = ( Ball (ft,s9)) as Subset of R^1 by METRIC_1:def 13, TOPMETR: 17;

              ( dist (ft,ft)) < s9 by A6, METRIC_1: 1;

              then

               A8: ft in B by METRIC_1: 11;

              B is open & f9 is_continuous_at t by A2, TMAP_1: 50, TOPMETR: 14, TOPMETR:def 6;

              then

              consider U be Subset of T such that

               A9: U is open & t in U and

               A10: (f9 .: U) c= B by A8, TMAP_1: 43;

              (( min (r,f)) .: U) c= R

              proof

                let mfx be object;

                assume mfx in (( min (r,f)) .: U);

                then

                consider x be object such that

                 A11: x in ( dom ( min (r,f))) and

                 A12: x in U and

                 A13: mfx = (( min (r,f)) . x) by FUNCT_1:def 6;

                reconsider x as Point of T by A11;

                (f . x) in REAL & r in REAL by XREAL_0:def 1;

                then

                reconsider fx = (f . x), r9 = r as Point of RealSpace by METRIC_1:def 13;

                ( dom ( min (r,f))) = the carrier of T by FUNCT_2:def 1;

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

                then

                 A14: (f . x) in (f .: U) by A12, FUNCT_1:def 6;

                then

                 A15: (f . x) in B by A10;

                now

                  per cases ;

                    suppose (f . x) <= r;

                    then ( min (r,(f . x))) = (f . x) by XXREAL_0:def 9;

                    then mfx = (f . x) by A13, Def9;

                    hence thesis by A7, A15;

                  end;

                    suppose

                     A16: (f . x) > r;

                    ( dist (fx,ft)) < s by A10, A14, METRIC_1: 11;

                    then

                     A17: |.((f . x) - (f . t)).| < s by TOPMETR: 11;

                    

                     A18: (r - (f . t)) <= ((f . x) - (f . t)) by A16, XREAL_1: 9;

                    (f . x) >= (f . t) by A5, A16, XXREAL_0: 2;

                    then ((f . x) - (f . t)) >= 0 by XREAL_1: 48;

                    then ((f . x) - (f . t)) < s by A17, ABSVALUE:def 1;

                    then

                     A19: (r - (f . t)) < s by A18, XXREAL_0: 2;

                    (r - (f . t)) >= 0 by A5, XREAL_1: 48;

                    then |.(r - (f . t)).| < s by A19, ABSVALUE:def 1;

                    then ( dist (ft,r9)) < s by TOPMETR: 11;

                    then

                     A20: r in B by METRIC_1: 11;

                    ( min (r,(f . x))) = r by A16, XXREAL_0:def 9;

                    then mfx = r by A13, Def9;

                    hence thesis by A7, A20;

                  end;

                end;

                hence thesis;

              end;

              hence ex U be Subset of T st U is open & t in U & (( min (r,f)) .: U) c= R by A9;

            end;

              suppose

               A21: (f . t) > r;

              set s = ((f . t) - r);

              reconsider B = ( Ball (ft,s)) as Subset of R^1 by METRIC_1:def 13, TOPMETR: 17;

              s > 0 by A21, XREAL_1: 50;

              then ( dist (ft,ft)) < s by METRIC_1: 1;

              then

               A22: ft in B by METRIC_1: 11;

              B is open & f9 is_continuous_at t by A2, TMAP_1: 50, TOPMETR: 14, TOPMETR:def 6;

              then

              consider U be Subset of T such that

               A23: U is open & t in U and

               A24: (f9 .: U) c= B by A22, TMAP_1: 43;

              (( min (r,f)) .: U) c= R

              proof

                let mfx be object;

                assume mfx in (( min (r,f)) .: U);

                then

                consider x be object such that

                 A25: x in ( dom ( min (r,f))) and

                 A26: x in U and

                 A27: mfx = (( min (r,f)) . x) by FUNCT_1:def 6;

                reconsider x as Point of T by A25;

                reconsider fx = (f . x) as Point of RealSpace by METRIC_1:def 13;

                ( dom ( min (r,f))) = the carrier of T by FUNCT_2:def 1;

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

                then (f . x) in (f .: U) by A26, FUNCT_1:def 6;

                then ( dist (ft,fx)) < s by A24, METRIC_1: 11;

                then |.((f . t) - (f . x)).| < s by TOPMETR: 11;

                then ((f . t) + ( - (f . x))) <= ((f . t) + ( - r)) by ABSVALUE: 5;

                then ( - (f . x)) <= ( - r) by XREAL_1: 6;

                then r <= (f . x) by XREAL_1: 24;

                then

                 A28: ( min (r,(f . x))) = r by XXREAL_0:def 9;

                ( min (r,(f . t))) = r by A21, XXREAL_0:def 9;

                then (( min (r,f)) . t) = r by Def9;

                hence thesis by A4, A27, A28, Def9;

              end;

              hence ex U be Subset of T st U is open & t in U & (( min (r,f)) .: U) c= R by A23;

            end;

          end;

          hence thesis;

        end;

        hence mf9 is_continuous_at t by TMAP_1: 43;

      end;

      then mf9 is continuous by TMAP_1: 50;

      hence thesis by JORDAN5A: 27;

    end;

    definition

      let X be set, f be Function of [:X, X:], REAL ;

      :: NAGATA_1:def10

      pred f is_a_pseudometric_of X means f is Reflexive symmetric triangle;

    end

    

     Lm8: for f be Function of [:X, X:], REAL holds f is_a_pseudometric_of X iff for a,b,c be Element of X holds (f . (a,a)) = 0 & (f . (a,b)) = (f . (b,a)) & (f . (a,c)) <= ((f . (a,b)) + (f . (b,c))) by METRIC_1:def 2, METRIC_1:def 4, METRIC_1:def 5;

    theorem :: NAGATA_1:28

    

     Th28: for f be Function of [:X, X:], REAL holds f is_a_pseudometric_of X iff for a,b,c be Element of X holds (f . (a,a)) = 0 & (f . (a,c)) <= ((f . (a,b)) + (f . (c,b)))

    proof

      let f be Function of [:X, X:], REAL ;

      thus f is_a_pseudometric_of X implies for a,b,c be Element of X holds (f . (a,a)) = 0 & (f . (a,c)) <= ((f . (a,b)) + (f . (c,b)))

      proof

        assume

         A1: f is_a_pseudometric_of X;

        let a,b,c be Element of X;

        (f . (a,c)) <= ((f . (a,b)) + (f . (b,c))) by A1, Lm8;

        hence thesis by A1, Lm8;

      end;

      thus (for a,b,c be Element of X holds (f . (a,a)) = 0 & (f . (a,c)) <= ((f . (a,b)) + (f . (c,b)))) implies f is_a_pseudometric_of X

      proof

        assume

         A2: for a,b,c be Element of X holds (f . (a,a)) = 0 & (f . (a,c)) <= ((f . (a,b)) + (f . (c,b)));

        

         A3: for a,b be Element of X holds (f . (a,b)) = (f . (b,a))

        proof

          let a,b be Element of X;

          

           A4: (f . (b,a)) <= ((f . (b,b)) + (f . (a,b))) & (f . (b,b)) = 0 by A2;

          (f . (a,b)) <= ((f . (a,a)) + (f . (b,a))) & (f . (a,a)) = 0 by A2;

          hence thesis by A4, XXREAL_0: 1;

        end;

        for a,b,c be Element of X holds (f . (a,c)) <= ((f . (a,b)) + (f . (b,c)))

        proof

          let x,y,z be Element of X;

          (f . (x,z)) <= ((f . (x,y)) + (f . (z,y))) by A2;

          hence thesis by A3;

        end;

        then f is Reflexive symmetric triangle by A2, A3, METRIC_1:def 2, METRIC_1:def 4, METRIC_1:def 5;

        hence thesis;

      end;

    end;

    

     Lm9: for r be Real, X be non empty set, f be Function of [:X, X:], REAL holds for x,y be Element of X holds (( min (r,f)) . (x,y)) = ( min (r,(f . (x,y))))

    proof

      let r be Real, X be non empty set, f be Function of [:X, X:], REAL ;

      let x,y be Element of X;

      (( min (r,f)) . (x,y)) = ( min (r,(f . [x, y]))) by Def9;

      hence thesis;

    end;

    theorem :: NAGATA_1:29

    

     Th29: for f be Function of [:X, X:], REAL st f is_a_pseudometric_of X holds for x,y be Element of X holds (f . (x,y)) >= 0

    proof

      let f be Function of [:X, X:], REAL such that

       A1: f is_a_pseudometric_of X;

      let x,y be Element of X;

      (f . (x,x)) <= ((f . (x,y)) + (f . (y,x))) & (f . (x,x)) = 0 by A1, Lm8;

      then 0 <= (((f . (x,y)) + (f . (x,y))) / 2) by A1, Lm8;

      hence thesis;

    end;

    theorem :: NAGATA_1:30

    

     Th30: for r, m st r > 0 & m is_a_pseudometric_of the carrier of T holds ( min (r,m)) is_a_pseudometric_of the carrier of T

    proof

      let r, m such that

       A1: r > 0 and

       A2: m is_a_pseudometric_of the carrier of T;

      now

        let a,b,c be Element of T;

        (m . (a,a)) = 0 by A2, Th28;

        then ( min (r,(m . (a,a)))) = 0 by A1, XXREAL_0:def 9;

        hence (( min (r,m)) . (a,a)) = 0 by Lm9;

        thus (( min (r,m)) . (a,c)) <= ((( min (r,m)) . (a,b)) + (( min (r,m)) . (c,b)))

        proof

          now

            per cases ;

              suppose

               A3: ((( min (r,m)) . (a,b)) + (( min (r,m)) . (c,b))) >= r;

              ( min (r,(m . (a,c)))) <= r by XXREAL_0: 17;

              then (( min (r,m)) . (a,c)) <= r by Lm9;

              hence thesis by A3, XXREAL_0: 2;

            end;

              suppose

               A4: ((( min (r,m)) . (a,b)) + (( min (r,m)) . (c,b))) < r;

              (m . (c,b)) >= 0 by A2, Th29;

              then 0 <= ( min (r,(m . (c,b)))) by A1, XXREAL_0: 20;

              then

               A5: 0 <= (( min (r,m)) . (c,b)) by Lm9;

              (m . (a,b)) >= 0 by A2, Th29;

              then 0 <= ( min (r,(m . (a,b)))) by A1, XXREAL_0: 20;

              then

               A6: 0 <= (( min (r,m)) . (a,b)) by Lm9;

              then (( min (r,m)) . (a,b)) < r by A4, A5, Lm1;

              then ( min (r,(m . (a,b)))) < r by Lm9;

              then ( min (r,(m . (a,b)))) = (m . (a,b)) by XXREAL_0:def 9;

              then

               A7: (( min (r,m)) . (a,b)) = (m . (a,b)) by Lm9;

              (( min (r,m)) . (c,b)) < r by A4, A6, A5, Lm1;

              then ( min (r,(m . (c,b)))) < r by Lm9;

              then ( min (r,(m . (c,b)))) = (m . (c,b)) by XXREAL_0:def 9;

              then

               A8: (( min (r,m)) . (c,b)) = (m . (c,b)) by Lm9;

              ( min (r,(m . (a,c)))) <= (m . (a,c)) & (m . (a,c)) <= ((m . (a,b)) + (m . (c,b))) by A2, Th28, XXREAL_0: 17;

              then ( min (r,(m . (a,c)))) <= ((m . (a,b)) + (m . (c,b))) by XXREAL_0: 2;

              hence thesis by A7, A8, Lm9;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis by Th28;

    end;

    theorem :: NAGATA_1:31

    for r, m st r > 0 & m is_metric_of the carrier of T holds ( min (r,m)) is_metric_of the carrier of T

    proof

      let r, m such that

       A1: r > 0 and

       A2: m is_metric_of the carrier of T;

      let a,b,c be Element of T;

      for a,b,c be Element of T holds (m . (a,a)) = 0 & (m . (a,b)) = (m . (b,a)) & (m . (a,c)) <= ((m . (a,b)) + (m . (b,c))) by A2;

      then m is_a_pseudometric_of the carrier of T by Lm8;

      then

       A3: ( min (r,m)) is_a_pseudometric_of the carrier of T by A1, Th30;

      (( min (r,m)) . (a,b)) = 0 implies a = b

      proof

        assume (( min (r,m)) . (a,b)) = 0 ;

        then ( min (r,(m . (a,b)))) = 0 by Lm9;

        then (m . (a,b)) = 0 by A1, XXREAL_0:def 9;

        hence thesis by A2;

      end;

      hence (( min (r,m)) . (a,b)) = 0 iff a = b by A3, Lm8;

      thus thesis by A3, Lm8;

    end;