yellow14.miz

    begin

    theorem :: YELLOW14:1

    ( bool { 0 }) = { 0 , 1} by CARD_1: 49, ZFMISC_1: 24;

    theorem :: YELLOW14:2



     Th2: for X be set, Y be Subset of X holds ( rng (( id X) | Y)) = Y

    proof

      let X be set, Y be Subset of X;

      set f = ( id X);



       A1: (f | Y) is Function of Y, X by FUNCT_2: 32;

      hereby

        let y be object;

        assume y in ( rng (f | Y));

        then

        consider x be object such that

         A2: x in ( dom (f | Y)) and

         A3: y = ((f | Y) . x) by FUNCT_1:def 3;

        ((f | Y) . x) = (f . x) by A2, FUNCT_1: 47

        .= x by A2, FUNCT_1: 17;

        hence y in Y by A1, A2, A3, FUNCT_2:def 1;

      end;

      let y be object;

      X = {} implies Y = {} ;

      then

       A4: ( dom (f | Y)) = Y by A1, FUNCT_2:def 1;

      assume

       A5: y in Y;



      then ((f | Y) . y) = (f . y) by FUNCT_1: 49

      .= y by A5, FUNCT_1: 18;

      hence thesis by A4, A5, FUNCT_1:def 3;

    end;

    theorem :: YELLOW14:3

    for S be empty 1-sorted, T be 1-sorted, f be Function of S, T st ( rng f) = ( [#] T) holds T is empty;

    theorem :: YELLOW14:4

    for S be 1-sorted, T be empty 1-sorted, f be Function of S, T st ( dom f) = ( [#] S) holds S is empty;

    theorem :: YELLOW14:5

    for S be non empty 1-sorted, T be 1-sorted, f be Function of S, T st ( dom f) = ( [#] S) holds T is non empty;

    theorem :: YELLOW14:6

    for S be 1-sorted, T be non empty 1-sorted, f be Function of S, T st ( rng f) = ( [#] T) holds S is non empty;

    definition

      let S be non empty reflexive RelStr, T be non empty RelStr, f be Function of S, T;

      :: original: directed-sups-preserving

      redefine

      :: YELLOW14:def1

      attr f is directed-sups-preserving means for X be non empty directed Subset of S holds f preserves_sup_of X;

      compatibility ;

    end

    definition

      let R be 1-sorted, N be NetStr over R;

      :: YELLOW14:def2

      attr N is Function-yielding means

      : Def2: the mapping of N is Function-yielding;

    end

    registration

      cluster non empty constituted-Functions for 1-sorted;

      existence

      proof

        take A = 1-sorted (# { {} } #);

        thus the carrier of A is non empty;

        let a be Element of A;

        thus thesis;

      end;

    end

    registration

      cluster strict non empty constituted-Functions for RelStr;

      existence

      proof

        take A = RelStr (# { {} }, ( id { {} }) #);

        thus A is strict non empty;

        let a be Element of A;

        thus thesis;

      end;

    end

    registration

      let R be constituted-Functions 1-sorted;

      cluster -> Function-yielding for NetStr over R;

      coherence

      proof

        let N be NetStr over R;

        let x be object;

        assume x in ( dom the mapping of N);

        then (the mapping of N . x) in ( rng the mapping of N) by FUNCT_1:def 3;

        hence thesis;

      end;

    end

    registration

      let R be constituted-Functions 1-sorted;

      cluster strict Function-yielding for NetStr over R;

      existence

      proof

        take A = NetStr (# the carrier of R, ( id the carrier of R), ( id the carrier of R) #);

        thus A is strict;

        let x be object;

        assume x in ( dom the mapping of A);

        hence thesis by FUNCT_1: 18;

      end;

    end

    registration

      let R be non empty constituted-Functions 1-sorted;

      cluster strict non empty Function-yielding for NetStr over R;

      existence

      proof

        take A = NetStr (# the carrier of R, ( id the carrier of R), ( id the carrier of R) #);

        thus A is strict non empty;

        let x be object;

        assume x in ( dom the mapping of A);

        hence thesis by FUNCT_1: 18;

      end;

    end

    registration

      let R be constituted-Functions 1-sorted, N be Function-yielding NetStr over R;

      cluster the mapping of N -> Function-yielding;

      coherence by Def2;

    end

    registration

      let R be non empty constituted-Functions 1-sorted;

      cluster strict Function-yielding for net of R;

      existence

      proof

        set p = the Element of R;

        set N = the net of R;

        take ( ConstantNet (N,p));

        thus thesis;

      end;

    end

    registration

      let S be non empty 1-sorted, N be non empty NetStr over S;

      cluster ( rng the mapping of N) -> non empty;

      coherence ;

    end

    registration

      let S be non empty 1-sorted, N be non empty NetStr over S;

      cluster ( rng ( netmap (N,S))) -> non empty;

      coherence ;

    end

    theorem :: YELLOW14:7

    for A,B,C be non empty RelStr, f be Function of B, C, g,h be Function of A, B st g <= h & f is monotone holds (f * g) <= (f * h)

    proof

      let A,B,C be non empty RelStr, f be Function of B, C, g,h be Function of A, B such that

       A1: g <= h and

       A2: for x,y be Element of B st x <= y holds (f . x) <= (f . y);

      for x be Element of A holds ((f * g) . x) <= ((f * h) . x)

      proof

        let x be Element of A;



         A3: ((f * g) . x) = (f . (g . x)) & ((f * h) . x) = (f . (h . x)) by FUNCT_2: 15;

        (g . x) <= (h . x) by A1, YELLOW_2: 9;

        hence thesis by A2, A3;

      end;

      hence thesis by YELLOW_2: 9;

    end;

    theorem :: YELLOW14:8

    for S be non empty TopSpace, T be non empty TopSpace-like TopRelStr, f,g be Function of S, T, x,y be Element of ( ContMaps (S,T)) st x = f & y = g holds x <= y iff f <= g

    proof

      let S be non empty TopSpace, T be non empty TopSpace-like TopRelStr, f,g be Function of S, T, x,y be Element of ( ContMaps (S,T)) such that

       A1: x = f & y = g;



       A2: ( ContMaps (S,T)) is full SubRelStr of (T |^ the carrier of S) by WAYBEL24:def 3;

      then

      reconsider x1 = x, y1 = y as Element of (T |^ the carrier of S) by YELLOW_0: 58;

      hereby

        assume x <= y;

        then x1 <= y1 by A2, YELLOW_0: 59;

        hence f <= g by A1, WAYBEL10: 11;

      end;

      assume f <= g;

      then x1 <= y1 by A1, WAYBEL10: 11;

      hence thesis by A2, YELLOW_0: 60;

    end;

    definition

      let I be non empty set, R be non empty RelStr, f be Element of (R |^ I), i be Element of I;

      :: original: .

      redefine

      func f . i -> Element of R ;

      coherence

      proof

        reconsider g = f as Element of ( product (I --> R)) by YELLOW_1:def 5;

        (g . i) is Element of ((I --> R) . i);

        hence thesis;

      end;

    end

    begin

    theorem :: YELLOW14:9



     Th9: for S,T be RelStr, f be Function of S, T st f is isomorphic holds f is onto

    proof

      let S,T be RelStr, f be Function of S, T such that

       A1: f is isomorphic;

      per cases ;

        suppose S is non empty & T is non empty;

        hence ( rng f) = the carrier of T by A1, WAYBEL_0: 66;

      end;

        suppose S is empty or T is empty;

        then T is empty by A1, WAYBEL_0:def 38;

        then the carrier of T = {} ;

        hence ( rng f) = the carrier of T;

      end;

    end;

    registration

      let S,T be RelStr;

      cluster isomorphic -> onto for Function of S, T;

      coherence by Th9;

    end

    theorem :: YELLOW14:10



     Th10: for S,T be non empty RelStr, f be Function of S, T st f is isomorphic holds (f /" ) is isomorphic

    proof

      let S,T be non empty RelStr, f be Function of S, T;

      assume

       A1: f is isomorphic;

      then (ex g be Function of T, S st g = (f qua Function " ) & g is monotone) & ( rng f) = the carrier of T by WAYBEL_0: 66, WAYBEL_0:def 38;

      hence thesis by A1, TOPS_2:def 4, WAYBEL_0: 68;

    end;

    theorem :: YELLOW14:11

    for S,T be non empty RelStr st (S,T) are_isomorphic & S is with_infima holds T is with_infima

    proof

      let S,T be non empty RelStr;

      given f be Function of S, T such that

       A1: f is isomorphic;

      assume

       A2: for a,b be Element of S holds ex c be Element of S st c <= a & c <= b & for c9 be Element of S st c9 <= a & c9 <= b holds c9 <= c;

      let x,y be Element of T;

      consider c be Element of S such that

       A3: c <= ((f /" ) . x) & c <= ((f /" ) . y) and

       A4: for c9 be Element of S st c9 <= ((f /" ) . x) & c9 <= ((f /" ) . y) holds c9 <= c by A2;

      take (f . c);



       A5: ex g be Function of T, S st g = (f qua Function " ) & g is monotone by A1, WAYBEL_0:def 38;



       A6: ( rng f) = the carrier of T by A1, WAYBEL_0: 66;



       A7: (f /" ) = (f qua Function " ) by A1, TOPS_2:def 4;

      (f . c) <= (f . ((f /" ) . x)) & (f . c) <= (f . ((f /" ) . y)) by A1, A3, WAYBEL_0: 66;

      hence (f . c) <= x & (f . c) <= y by A1, A6, A7, FUNCT_1: 35;

      let z9 be Element of T;

      assume z9 <= x & z9 <= y;

      then ((f /" ) . z9) <= ((f /" ) . x) & ((f /" ) . z9) <= ((f /" ) . y) by A7, A5, WAYBEL_1:def 2;

      then ((f /" ) . z9) <= c by A4;

      then (f . ((f /" ) . z9)) <= (f . c) by A1, WAYBEL_0: 66;

      hence thesis by A1, A6, A7, FUNCT_1: 35;

    end;

    theorem :: YELLOW14:12

    for S,T be non empty RelStr st (S,T) are_isomorphic & S is with_suprema holds T is with_suprema

    proof

      let S,T be non empty RelStr;

      given f be Function of S, T such that

       A1: f is isomorphic;

      assume

       A2: for a,b be Element of S holds ex c be Element of S st a <= c & b <= c & for c9 be Element of S st a <= c9 & b <= c9 holds c <= c9;

      let x,y be Element of T;

      consider c be Element of S such that

       A3: ((f /" ) . x) <= c & ((f /" ) . y) <= c and

       A4: for c9 be Element of S st ((f /" ) . x) <= c9 & ((f /" ) . y) <= c9 holds c <= c9 by A2;

      take (f . c);



       A5: ex g be Function of T, S st g = (f qua Function " ) & g is monotone by A1, WAYBEL_0:def 38;



       A6: ( rng f) = the carrier of T by A1, WAYBEL_0: 66;



       A7: (f /" ) = (f qua Function " ) by A1, TOPS_2:def 4;

      (f . ((f /" ) . x)) <= (f . c) & (f . ((f /" ) . y)) <= (f . c) by A1, A3, WAYBEL_0: 66;

      hence x <= (f . c) & y <= (f . c) by A1, A6, A7, FUNCT_1: 35;

      let z9 be Element of T;

      assume x <= z9 & y <= z9;

      then ((f /" ) . x) <= ((f /" ) . z9) & ((f /" ) . y) <= ((f /" ) . z9) by A7, A5, WAYBEL_1:def 2;

      then c <= ((f /" ) . z9) by A4;

      then (f . c) <= (f . ((f /" ) . z9)) by A1, WAYBEL_0: 66;

      hence thesis by A1, A6, A7, FUNCT_1: 35;

    end;

    theorem :: YELLOW14:13



     Th13: for L be RelStr st L is empty holds L is bounded

    proof

      let L be RelStr such that

       A1: L is empty;

      set x = the Element of L;

      thus L is lower-bounded

      proof

        take x;

        let a be Element of L;

        assume a in the carrier of L;

        hence thesis by A1;

      end;

      take x;

      let a be Element of L;

      assume a in the carrier of L;

      hence thesis by A1;

    end;

    registration

      cluster empty -> bounded for RelStr;

      coherence by Th13;

    end

    theorem :: YELLOW14:14

    for S,T be RelStr st (S,T) are_isomorphic & S is lower-bounded holds T is lower-bounded

    proof

      let S,T be RelStr;

      given f be Function of S, T such that

       A1: f is isomorphic;

      per cases ;

        suppose S is non empty & T is non empty;

        then

        reconsider s = S, t = T as non empty RelStr;

        given X be Element of S such that

         A2: X is_<=_than the carrier of S;

        reconsider x = X as Element of s;

        reconsider g = f as Function of s, t;

        reconsider y = (g . x) as Element of T;

        take y;

        y is_<=_than (g .: ( [#] S)) by A1, A2, YELLOW_2: 13;

        then y is_<=_than ( rng g) by RELSET_1: 22;

        hence thesis by A1, WAYBEL_0: 66;

      end;

        suppose S is empty or T is empty;

        then T is empty by A1, WAYBEL_0:def 38;

        then

        reconsider T as bounded RelStr;

        T is lower-bounded;

        hence thesis;

      end;

    end;

    theorem :: YELLOW14:15

    for S,T be RelStr st (S,T) are_isomorphic & S is upper-bounded holds T is upper-bounded

    proof

      let S,T be RelStr;

      given f be Function of S, T such that

       A1: f is isomorphic;

      per cases ;

        suppose S is non empty & T is non empty;

        then

        reconsider s = S, t = T as non empty RelStr;

        given X be Element of S such that

         A2: X is_>=_than the carrier of S;

        reconsider x = X as Element of s;

        reconsider g = f as Function of s, t;

        reconsider y = (g . x) as Element of T;

        take y;

        y is_>=_than (g .: ( [#] S)) by A1, A2, YELLOW_2: 14;

        then y is_>=_than ( rng g) by RELSET_1: 22;

        hence thesis by A1, WAYBEL_0: 66;

      end;

        suppose S is empty or T is empty;

        then T is empty by A1, WAYBEL_0:def 38;

        then

        reconsider T as bounded RelStr;

        T is lower-bounded;

        hence thesis;

      end;

    end;

    theorem :: YELLOW14:16

    for S,T be non empty RelStr, A be Subset of S, f be Function of S, T st f is isomorphic & ex_sup_of (A,S) holds ex_sup_of ((f .: A),T)

    proof

      let S,T be non empty RelStr, A be Subset of S, f be Function of S, T such that

       A1: f is isomorphic;



       A2: (f " (f .: A)) c= A by A1, FUNCT_1: 82;



       A3: ( rng f) = ( [#] T) by A1, WAYBEL_0: 66;



       A4: (f /" ) = (f qua Function " ) by A1, TOPS_2:def 4;

      given a be Element of S such that

       A5: A is_<=_than a and

       A6: for b be Element of S st A is_<=_than b holds b >= a and

       A7: for c be Element of S st A is_<=_than c & for b be Element of S st A is_<=_than b holds b >= c holds c = a;

      take (f . a);

      thus (f .: A) is_<=_than (f . a) by A1, A5, WAYBEL13: 19;



       A8: (f /" ) is isomorphic by A1, Th10;



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

      then A c= (f " (f .: A)) by FUNCT_1: 76;

      then

       A10: (f " (f .: A)) = A by A2;

      hereby

        let b be Element of T;

        assume (f .: A) is_<=_than b;

        then ((f /" ) .: (f .: A)) is_<=_than ((f /" ) . b) by A8, WAYBEL13: 19;

        then (f " (f .: A)) is_<=_than ((f /" ) . b) by A1, A3, TOPS_2: 55;

        then ((f /" ) . b) >= a by A6, A10;

        then (f . ((f /" ) . b)) >= (f . a) by A1, WAYBEL_0: 66;

        hence b >= (f . a) by A1, A3, A4, FUNCT_1: 35;

      end;

      let c be Element of T;

      assume

       A11: (f .: A) is_<=_than c;

      assume

       A12: for b be Element of T st (f .: A) is_<=_than b holds b >= c;



       A13: for b be Element of S st A is_<=_than b holds b >= ((f /" ) . c)

      proof

        let b be Element of S;

        assume A is_<=_than b;

        then (f .: A) is_<=_than (f . b) by A1, WAYBEL13: 19;

        then (f . b) >= c by A12;

        then ((f /" ) . (f . b)) >= ((f /" ) . c) by A8, WAYBEL_0: 66;

        hence thesis by A1, A4, A9, FUNCT_1: 34;

      end;

      ((f /" ) .: (f .: A)) is_<=_than ((f /" ) . c) by A8, A11, WAYBEL13: 19;

      then A is_<=_than ((f /" ) . c) by A1, A3, A10, TOPS_2: 55;

      then ((f /" ) . c) = a by A7, A13;

      hence thesis by A1, A3, A4, FUNCT_1: 35;

    end;

    theorem :: YELLOW14:17

    for S,T be non empty RelStr, A be Subset of S, f be Function of S, T st f is isomorphic & ex_inf_of (A,S) holds ex_inf_of ((f .: A),T)

    proof

      let S,T be non empty RelStr, A be Subset of S, f be Function of S, T such that

       A1: f is isomorphic;



       A2: (f " (f .: A)) c= A by A1, FUNCT_1: 82;



       A3: ( rng f) = ( [#] T) by A1, WAYBEL_0: 66;



       A4: (f /" ) = (f qua Function " ) by A1, TOPS_2:def 4;

      given a be Element of S such that

       A5: A is_>=_than a and

       A6: for b be Element of S st A is_>=_than b holds b <= a and

       A7: for c be Element of S st A is_>=_than c & for b be Element of S st A is_>=_than b holds b <= c holds c = a;

      take (f . a);

      thus (f .: A) is_>=_than (f . a) by A1, A5, WAYBEL13: 18;



       A8: (f /" ) is isomorphic by A1, Th10;



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

      then A c= (f " (f .: A)) by FUNCT_1: 76;

      then

       A10: (f " (f .: A)) = A by A2;

      hereby

        let b be Element of T;

        assume (f .: A) is_>=_than b;

        then ((f /" ) .: (f .: A)) is_>=_than ((f /" ) . b) by A8, WAYBEL13: 18;

        then (f " (f .: A)) is_>=_than ((f /" ) . b) by A1, A3, TOPS_2: 55;

        then ((f /" ) . b) <= a by A6, A10;

        then (f . ((f /" ) . b)) <= (f . a) by A1, WAYBEL_0: 66;

        hence b <= (f . a) by A1, A3, A4, FUNCT_1: 35;

      end;

      let c be Element of T;

      assume

       A11: (f .: A) is_>=_than c;

      assume

       A12: for b be Element of T st (f .: A) is_>=_than b holds b <= c;



       A13: for b be Element of S st A is_>=_than b holds b <= ((f /" ) . c)

      proof

        let b be Element of S;

        assume A is_>=_than b;

        then (f .: A) is_>=_than (f . b) by A1, WAYBEL13: 18;

        then (f . b) <= c by A12;

        then ((f /" ) . (f . b)) <= ((f /" ) . c) by A8, WAYBEL_0: 66;

        hence thesis by A1, A4, A9, FUNCT_1: 34;

      end;

      ((f /" ) .: (f .: A)) is_>=_than ((f /" ) . c) by A8, A11, WAYBEL13: 18;

      then A is_>=_than ((f /" ) . c) by A1, A3, A10, TOPS_2: 55;

      then ((f /" ) . c) = a by A7, A13;

      hence thesis by A1, A3, A4, FUNCT_1: 35;

    end;

    begin

    theorem :: YELLOW14:18

    for S,T be TopStruct st ((S,T) are_homeomorphic or ex f be Function of S, T st ( dom f) = ( [#] S) & ( rng f) = ( [#] T)) holds S is empty iff T is empty

    proof

      let S,T be TopStruct;

      assume

       A1: (S,T) are_homeomorphic or ex f be Function of S, T st ( dom f) = ( [#] S) & ( rng f) = ( [#] T);

      per cases by A1;

        suppose (S,T) are_homeomorphic ;

        then

        consider f be Function of S, T such that

         A2: f is being_homeomorphism;

        ( rng f) = ( [#] T) & ( dom f) = ( [#] S) by A2;

        hence thesis;

      end;

        suppose ex f be Function of S, T st ( dom f) = ( [#] S) & ( rng f) = ( [#] T);

        hence thesis;

      end;

    end;

    theorem :: YELLOW14:19

    for T be non empty TopSpace holds (T, the TopStruct of T) are_homeomorphic

    proof

      let T be non empty TopSpace;

      reconsider f = ( id T) as Function of T, the TopStruct of T;

      take f;

      thus ( dom f) = ( [#] T);



      thus ( rng f) = ( [#] T)

      .= ( [#] the TopStruct of T);

      thus f is one-to-one;

      thus f is continuous by YELLOW12: 36;

      thus thesis by YELLOW12: 36;

    end;

    registration

      let T be Scott reflexive non empty TopRelStr;

      cluster open -> inaccessible upper for Subset of T;

      coherence by WAYBEL11:def 4;

      cluster inaccessible upper -> open for Subset of T;

      coherence by WAYBEL11:def 4;

    end

    theorem :: YELLOW14:20

    for T be TopStruct, x,y be Point of T, X,Y be Subset of T st X = {x} & ( Cl X) c= ( Cl Y) holds x in ( Cl Y)

    proof

      let T be TopStruct, x,y be Point of T, X,Y be Subset of T such that

       A1: X = {x} and

       A2: ( Cl X) c= ( Cl Y);

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

      then

       A3: X c= ( Cl Y) by A2;

      x in X by A1, TARSKI:def 1;

      hence thesis by A3;

    end;

    theorem :: YELLOW14:21

    for T be TopStruct, x,y be Point of T, Y,V be Subset of T st Y = {y} & x in ( Cl Y) & V is open & x in V holds y in V

    proof

      let T be TopStruct, x,y be Point of T, Y,V be Subset of T such that

       A1: Y = {y};

      assume x in ( Cl Y) & V is open & x in V;

      then Y meets V by PRE_TOPC:def 7;

      hence thesis by A1, ZFMISC_1: 50;

    end;

    theorem :: YELLOW14:22

    for T be TopStruct, x,y be Point of T, X,Y be Subset of T st X = {x} & Y = {y} holds (for V be Subset of T st V is open holds (x in V implies y in V)) implies ( Cl X) c= ( Cl Y)

    proof

      let T be TopStruct, x,y be Point of T, X,Y be Subset of T;

      assume that

       A1: X = {x} and

       A2: Y = {y} & for V be Subset of T st V is open holds x in V implies y in V;

      let z be object;

      assume

       A3: z in ( Cl X);

      for V be Subset of T st V is open holds z in V implies Y meets V

      proof

        let V be Subset of T;

        assume that

         A4: V is open and

         A5: z in V;

        X meets V by A3, A4, A5, PRE_TOPC:def 7;

        then x in V by A1, ZFMISC_1: 50;

        hence thesis by A2, A4, ZFMISC_1: 48;

      end;

      hence thesis by A3, PRE_TOPC:def 7;

    end;

    theorem :: YELLOW14:23



     Th23: for S,T be non empty TopSpace, A be irreducible Subset of S, B be Subset of T st A = B & the TopStruct of S = the TopStruct of T holds B is irreducible

    proof

      let S,T be non empty TopSpace, A be irreducible Subset of S, B be Subset of T such that

       A1: A = B and

       A2: the TopStruct of S = the TopStruct of T;

      A is non empty closed by YELLOW_8:def 3;

      hence B is non empty closed by A1, A2, TOPS_3: 79;

      let B1,B2 be Subset of T such that

       A3: B1 is closed & B2 is closed and

       A4: B = (B1 \/ B2);

      reconsider A1 = B1, A2 = B2 as Subset of S by A2;

      A1 is closed & A2 is closed by A2, A3, TOPS_3: 79;

      hence thesis by A1, A4, YELLOW_8:def 3;

    end;

    theorem :: YELLOW14:24



     Th24: for S,T be non empty TopSpace, a be Point of S, b be Point of T, A be Subset of S, B be Subset of T st a = b & A = B & the TopStruct of S = the TopStruct of T & a is_dense_point_of A holds b is_dense_point_of B

    proof

      let S,T be non empty TopSpace, a be Point of S, b be Point of T, A be Subset of S, B be Subset of T;

      assume a = b & A = B & the TopStruct of S = the TopStruct of T & a in A & A c= ( Cl {a});

      hence b in B & B c= ( Cl {b}) by TOPS_3: 80;

    end;

    theorem :: YELLOW14:25



     Th25: for S,T be TopStruct, A be Subset of S, B be Subset of T st A = B & the TopStruct of S = the TopStruct of T & A is compact holds B is compact

    proof

      let S,T be TopStruct, A be Subset of S, B be Subset of T such that

       A1: A = B and

       A2: the TopStruct of S = the TopStruct of T and

       A3: for F be Subset-Family of S st F is Cover of A & F is open holds ex G be Subset-Family of S st G c= F & G is Cover of A & G is finite;

      let F be Subset-Family of T such that

       A4: F is Cover of B & F is open;

      reconsider K = F as Subset-Family of S by A2;

      consider L be Subset-Family of S such that

       A5: L c= K & L is Cover of A & L is finite by A1, A2, A3, A4, WAYBEL_9: 19;

      reconsider G = L as Subset-Family of T by A2;

      take G;

      thus thesis by A1, A5;

    end;

    theorem :: YELLOW14:26

    for S,T be non empty TopSpace st the TopStruct of S = the TopStruct of T & S is sober holds T is sober

    proof

      let S,T be non empty TopSpace such that

       A1: the TopStruct of S = the TopStruct of T and

       A2: for A be irreducible Subset of S holds ex a be Point of S st a is_dense_point_of A & for b be Point of S st b is_dense_point_of A holds a = b;

      let B be irreducible Subset of T;

      reconsider A = B as irreducible Subset of S by A1, Th23;

      consider a be Point of S such that

       A3: a is_dense_point_of A and

       A4: for b be Point of S st b is_dense_point_of A holds a = b by A2;

      reconsider p = a as Point of T by A1;

      take p;

      thus p is_dense_point_of B by A1, A3, Th24;

      let q be Point of T;

      reconsider b = q as Point of S by A1;

      assume q is_dense_point_of B;

      then b is_dense_point_of A by A1, Th24;

      hence thesis by A4;

    end;

    theorem :: YELLOW14:27

    for S,T be non empty TopSpace st the TopStruct of S = the TopStruct of T & S is locally-compact holds T is locally-compact

    proof

      let S,T be non empty TopSpace such that

       A1: the TopStruct of S = the TopStruct of T and

       A2: for x be Point of S, X be Subset of S st x in X & X is open holds ex Y be Subset of S st x in ( Int Y) & Y c= X & Y is compact;

      let x be Point of T, X be Subset of T such that

       A3: x in X & X is open;

      reconsider A = X as Subset of S by A1;

      consider B be Subset of S such that

       A4: x in ( Int B) & B c= A & B is compact by A1, A2, A3, TOPS_3: 76;

      reconsider Y = B as Subset of T by A1;

      take Y;

      thus thesis by A1, A4, Th25, TOPS_3: 77;

    end;

    theorem :: YELLOW14:28

    for S,T be TopStruct st the TopStruct of S = the TopStruct of T & S is compact holds T is compact

    proof

      let S,T be TopStruct such that

       A1: the TopStruct of S = the TopStruct of T and

       A2: for F be Subset-Family of S st F is Cover of S & F is open holds ex G be Subset-Family of S st G c= F & G is Cover of S & G is finite;

      let F be Subset-Family of T such that

       A3: F is Cover of T & F is open;

      reconsider K = F as Subset-Family of S by A1;

      consider L be Subset-Family of S such that

       A4: L c= K & L is Cover of S & L is finite by A1, A2, A3, WAYBEL_9: 19;

      reconsider G = L as Subset-Family of T by A1;

      take G;

      thus thesis by A1, A4;

    end;

    definition

      let I be non empty set, T be non empty TopSpace, x be Point of ( product (I --> T)), i be Element of I;

      :: original: .

      redefine

      func x . i -> Element of T ;

      coherence

      proof

        (x . i) is Point of T;

        hence thesis;

      end;

    end

    theorem :: YELLOW14:29



     Th29: for M be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of M, x,y be Point of ( product J) holds x in ( Cl {y}) iff for i be Element of M holds (x . i) in ( Cl {(y . i)})

    proof

      let M be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of M, x,y be Point of ( product J);

      hereby

        assume

         A1: x in ( Cl {y});

        let i be Element of M;

        x in the carrier of ( product J);

        then x in ( product ( Carrier J)) by WAYBEL18:def 3;

        then

        consider f be Function such that

         A2: x = f and

         A3: ( dom f) = ( dom ( Carrier J)) and

         A4: for z be object st z in ( dom ( Carrier J)) holds (f . z) in (( Carrier J) . z) by CARD_3:def 5;



         A5: i in M;

        for G be Subset of (J . i) st G is open holds (x . i) in G implies {(y . i)} meets G

        proof

          let G be Subset of (J . i);

          assume that

           A6: G is open and

           A7: (x . i) in G;

          reconsider G9 = G as Subset of (J . i);

          ( [#] (J . i)) <> {} & ( proj (J,i)) is continuous by WAYBEL18: 5;

          then

           A8: (( proj (J,i)) " G9) is open by A6, TOPS_2: 43;



           A9: for z be object st z in ( dom (( Carrier J) +* (i,G))) holds (f . z) in ((( Carrier J) +* (i,G)) . z)

          proof

            let z be object;

            assume z in ( dom (( Carrier J) +* (i,G)));

            then

             A10: z in ( dom ( Carrier J)) by FUNCT_7: 30;

            per cases ;

              suppose z = i;

              hence thesis by A2, A7, A10, FUNCT_7: 31;

            end;

              suppose z <> i;

              then ((( Carrier J) +* (i,G)) . z) = (( Carrier J) . z) by FUNCT_7: 32;

              hence thesis by A4, A10;

            end;

          end;



           A11: ( product (( Carrier J) +* (i,G9))) = (( proj (J,i)) " G9) by WAYBEL18: 4;

          ( dom f) = ( dom (( Carrier J) +* (i,G))) by A3, FUNCT_7: 30;

          then x in ( product (( Carrier J) +* (i,G))) by A2, A9, CARD_3:def 5;

          then {y} meets (( proj (J,i)) " G9) by A1, A8, A11, PRE_TOPC:def 7;

          then y in ( product (( Carrier J) +* (i,G))) by A11, ZFMISC_1: 50;

          then

          consider g be Function such that

           A12: y = g and ( dom g) = ( dom (( Carrier J) +* (i,G))) and

           A13: for z be object st z in ( dom (( Carrier J) +* (i,G))) holds (g . z) in ((( Carrier J) +* (i,G)) . z) by CARD_3:def 5;



           A14: i in ( dom ( Carrier J)) by A5, PARTFUN1:def 2;

          then i in ( dom (( Carrier J) +* (i,G))) by FUNCT_7: 30;

          then (g . i) in ((( Carrier J) +* (i,G)) . i) by A13;

          then (g . i) in G by A14, FUNCT_7: 31;

          hence thesis by A12, ZFMISC_1: 48;

        end;

        hence (x . i) in ( Cl {(y . i)}) by PRE_TOPC:def 7;

      end;

      reconsider K = ( product_prebasis J) as prebasis of ( product J) by WAYBEL18:def 3;

      assume

       A15: for i be Element of M holds (x . i) in ( Cl {(y . i)});

      for Z be finite Subset-Family of ( product J) st Z c= K & x in ( Intersect Z) holds ( Intersect Z) meets {y}

      proof

        let Z be finite Subset-Family of ( product J);

        assume that

         A16: Z c= K and

         A17: x in ( Intersect Z);

        for Y be set st Y in Z holds y in Y

        proof

          let Y be set;

          y in the carrier of ( product J);

          then y in ( product ( Carrier J)) by WAYBEL18:def 3;

          then

          consider g be Function such that

           A18: y = g and

           A19: ( dom g) = ( dom ( Carrier J)) and

           A20: for z be object st z in ( dom ( Carrier J)) holds (g . z) in (( Carrier J) . z) by CARD_3:def 5;

          assume

           A21: Y in Z;

          then Y in K by A16;

          then

          consider i be set, W be TopStruct, V be Subset of W such that

           A22: i in M and

           A23: V is open and

           A24: W = (J . i) and

           A25: Y = ( product (( Carrier J) +* (i,V))) by WAYBEL18:def 2;

          reconsider i as Element of M by A22;

          reconsider V as Subset of (J . i) by A24;

          x in Y by A17, A21, SETFAM_1: 43;

          then

           A26: ex f be Function st x = f & ( dom f) = ( dom (( Carrier J) +* (i,V))) & for z be object st z in ( dom (( Carrier J) +* (i,V))) holds (f . z) in ((( Carrier J) +* (i,V)) . z) by A25, CARD_3:def 5;

          (x . i) in ( Cl {(y . i)}) by A15;

          then

           A27: (x . i) in V implies {(y . i)} meets V by A23, A24, PRE_TOPC:def 7;



           A28: for z be object st z in ( dom (( Carrier J) +* (i,V))) holds (g . z) in ((( Carrier J) +* (i,V)) . z)

          proof

            let z be object;

            assume

             A29: z in ( dom (( Carrier J) +* (i,V)));

            then

             A30: z in ( dom ( Carrier J)) by FUNCT_7: 30;

            per cases ;

              suppose

               A31: z = i;

              then ((( Carrier J) +* (i,V)) . z) = V by A30, FUNCT_7: 31;

              hence thesis by A27, A26, A18, A29, A31, ZFMISC_1: 50;

            end;

              suppose z <> i;

              then ((( Carrier J) +* (i,V)) . z) = (( Carrier J) . z) by FUNCT_7: 32;

              hence thesis by A20, A30;

            end;

          end;

          ( dom g) = ( dom (( Carrier J) +* (i,V))) by A19, FUNCT_7: 30;

          hence thesis by A25, A18, A28, CARD_3:def 5;

        end;

        then y in {y} & y in ( Intersect Z) by SETFAM_1: 43, TARSKI:def 1;

        hence thesis by XBOOLE_0: 3;

      end;

      hence thesis by YELLOW_9: 38;

    end;

    theorem :: YELLOW14:30

    for M be non empty set, T be non empty TopSpace, x,y be Point of ( product (M --> T)) holds x in ( Cl {y}) iff for i be Element of M holds (x . i) in ( Cl {(y . i)})

    proof

      let M be non empty set, T be non empty TopSpace, x,y be Point of ( product (M --> T));

      reconsider J = (M --> T) as TopStruct-yielding non-Empty ManySortedSet of M;

      reconsider x9 = x, y9 = y as Point of ( product J);

      thus x in ( Cl {y}) implies for i be Element of M holds (x . i) in ( Cl {(y . i)})

      proof

        assume

         A1: x in ( Cl {y});

        let i be Element of M;

        (x9 . i) in ( Cl {(y9 . i)}) by A1, Th29;

        hence thesis;

      end;

      assume for i be Element of M holds (x . i) in ( Cl {(y . i)});

      then for i be Element of M holds (x9 . i) in ( Cl {(y9 . i)});

      hence thesis by Th29;

    end;

    theorem :: YELLOW14:31



     Th31: for M be non empty set, i be Element of M, J be TopStruct-yielding non-Empty ManySortedSet of M, x be Point of ( product J) holds ( pi (( Cl {x}),i)) = ( Cl {(x . i)})

    proof

      let M be non empty set, i be Element of M, J be TopStruct-yielding non-Empty ManySortedSet of M, x be Point of ( product J);

      consider f be object such that

       A1: f in ( Cl {x}) by XBOOLE_0:def 1;



       A2: f in the carrier of ( product J) by A1;

      thus ( pi (( Cl {x}),i)) c= ( Cl {(x . i)})

      proof

        let a be object;

        assume a in ( pi (( Cl {x}),i));

        then ex f be Function st f in ( Cl {x}) & a = (f . i) by CARD_3:def 6;

        hence thesis by Th29;

      end;

      reconsider f as Element of ( product J) by A1;

      let a be object;

      set y = (f +* (i .--> a));



       A3: ( dom ( Carrier J)) = M by PARTFUN1:def 2;



       A4: f in ( product ( Carrier J)) by A2, WAYBEL18:def 3;

      then

       A5: ( dom f) = M by A3, CARD_3: 9;

      assume

       A7: a in ( Cl {(x . i)});



       A8: for m be object st m in ( dom ( Carrier J)) holds (y . m) in (( Carrier J) . m)

      proof

        let m be object;

        assume

         A9: m in ( dom ( Carrier J));

        then

         A10: ex R be 1-sorted st R = (J . m) & (( Carrier J) . m) = the carrier of R by PRALG_1:def 15;

        per cases ;

          suppose

           A11: m = i;

          then (y . m) = a by FUNCT_7: 94;

          hence thesis by A7, A10, A11;

        end;

          suppose m <> i;

          then not m in ( dom (i .--> a)) by TARSKI:def 1;

          then (y . m) = (f . m) by FUNCT_4: 11;

          hence thesis by A4, A9, CARD_3: 9;

        end;

      end;

      ( dom y) = (( dom f) \/ ( dom (i .--> a))) by FUNCT_4:def 1

      .= (M \/ {i}) by A5

      .= M by ZFMISC_1: 40;

      then y in ( product ( Carrier J)) by A3, A8, CARD_3: 9;

      then

      reconsider y = (f +* (i .--> a)) as Element of ( product J) by WAYBEL18:def 3;

      for m be Element of M holds (y . m) in ( Cl {(x . m)})

      proof

        let m be Element of M;

        per cases ;

          suppose m = i;

          hence thesis by A7, FUNCT_7: 94;

        end;

          suppose m <> i;

          then not m in ( dom (i .--> a)) by TARSKI:def 1;

          then (y . m) = (f . m) by FUNCT_4: 11;

          hence thesis by A1, Th29;

        end;

      end;

      then

       A12: (f +* (i .--> a)) in ( Cl {x}) by Th29;

      ((f +* (i .--> a)) . i) = a by FUNCT_7: 94;

      hence thesis by A12, CARD_3:def 6;

    end;

    theorem :: YELLOW14:32

    for M be non empty set, i be Element of M, T be non empty TopSpace, x be Point of ( product (M --> T)) holds ( pi (( Cl {x}),i)) = ( Cl {(x . i)})

    proof

      let M be non empty set, i be Element of M, T be non empty TopSpace, x be Point of ( product (M --> T));

      ((M --> T) . i) = T;

      hence thesis by Th31;

    end;

    theorem :: YELLOW14:33

    for X,Y be non empty TopStruct, f be Function of X, Y, g be Function of Y, X st f = ( id X) & g = ( id X) & f is continuous & g is continuous holds the TopStruct of X = the TopStruct of Y

    proof

      let X,Y be non empty TopStruct, f be Function of X, Y, g be Function of Y, X such that

       A1: f = ( id X) and

       A2: g = ( id X) and

       A3: f is continuous and

       A4: g is continuous;



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

      .= the carrier of Y by A2, FUNCT_2:def 1;



       A6: ( [#] Y) <> {} ;



       A7: ( [#] X) <> {} ;

      the topology of X = the topology of Y

      proof

        hereby

          let A be object;

          assume

           A8: A in the topology of X;

          then

          reconsider B = A as Subset of X;

          B is open by A8;

          then

           A9: (g " B) is open by A4, A7, TOPS_2: 43;

          (g " B) = B by A2, FUNCT_2: 94;

          hence A in the topology of Y by A9;

        end;

        let A be object;

        assume

         A10: A in the topology of Y;

        then

        reconsider B = A as Subset of Y;

        B is open by A10;

        then

         A11: (f " B) is open by A3, A6, TOPS_2: 43;

        (f " B) = B by A1, A5, FUNCT_2: 94;

        hence thesis by A11;

      end;

      hence thesis by A5;

    end;

    theorem :: YELLOW14:34

    for X,Y be non empty TopSpace, f be Function of X, Y st ( corestr f) is continuous holds f is continuous

    proof

      let X,Y be non empty TopSpace, f be Function of X, Y such that

       A1: ( corestr f) is continuous;

      ( corestr f) = f by WAYBEL18:def 7;

      hence thesis by A1, PRE_TOPC: 26;

    end;

    registration

      let X be non empty TopSpace, Y be non empty SubSpace of X;

      cluster ( incl Y) -> continuous;

      coherence by TMAP_1: 87;

    end

    theorem :: YELLOW14:35

    for T be non empty TopSpace, f be Function of T, T st (f * f) = f holds (( corestr f) * ( incl ( Image f))) = ( id ( Image f))

    proof

      let T be non empty TopSpace, f be Function of T, T such that

       A1: (f * f) = f;

      set cf = ( corestr f), i = ( incl ( Image f));

      for x be object st x in the carrier of ( Image f) holds ((cf * i) . x) = (( id ( Image f)) . x)

      proof



         A2: the carrier of ( Image f) c= the carrier of T by BORSUK_1: 1;

        let x be object;

        assume

         A3: x in the carrier of ( Image f);

        the carrier of ( Image f) = ( rng f) by WAYBEL18: 9;

        then

         A4: ex y be object st y in ( dom f) & (f . y) = x by A3, FUNCT_1:def 3;



        thus ((cf * i) . x) = (cf . (i . x)) by A3, FUNCT_2: 15

        .= (cf . x) by A3, A2, TMAP_1: 84

        .= (f . x) by WAYBEL18:def 7

        .= x by A1, A4, FUNCT_2: 15

        .= (( id ( Image f)) . x) by A3, FUNCT_1: 18;

      end;

      hence thesis;

    end;

    theorem :: YELLOW14:36

    for Y be non empty TopSpace, W be non empty SubSpace of Y holds ( corestr ( incl W)) is being_homeomorphism

    proof

      let Y be non empty TopSpace, W be non empty SubSpace of Y;

      set ci = ( corestr ( incl W));

      thus ( dom ci) = ( [#] W) by FUNCT_2:def 1;

      thus

       A1: ( rng ci) = ( [#] ( Image ( incl W))) by FUNCT_2:def 3;



       A2: ci = ( incl W) by WAYBEL18:def 7

      .= (( id Y) | W) by TMAP_1:def 6

      .= (( id the carrier of Y) | the carrier of W) by TMAP_1:def 4;

      hence

       A3: ci is one-to-one by FUNCT_1: 52;



       A4: for P be Subset of W st P is open holds ((ci /" ) " P) is open

      proof

        let P be Subset of W;

        assume P in the topology of W;

        then

         A5: ex Q be Subset of Y st Q in the topology of Y & P = (Q /\ ( [#] W)) by PRE_TOPC:def 4;



         A6: the carrier of W is non empty Subset of Y by BORSUK_1: 1;

        then

         A7: P is Subset of Y by XBOOLE_1: 1;



         A8: ( [#] W) = ( rng (( id the carrier of Y) | the carrier of W)) by A6, Th2

        .= ( rng (( id Y) | W)) by TMAP_1:def 4

        .= ( rng ( incl W)) by TMAP_1:def 6

        .= ( [#] ( Image ( incl W))) by WAYBEL18: 9;

        ((ci /" ) " P) = ((( id the carrier of Y) | the carrier of W) .: P) by A1, A2, A3, TOPS_2: 54

        .= (( id the carrier of Y) .: P) by FUNCT_2: 97

        .= P by A7, FUNCT_1: 92;

        hence ((ci /" ) " P) in the topology of ( Image ( incl W)) by A5, A8, PRE_TOPC:def 4;

      end;

      thus ci is continuous by WAYBEL18: 10;

      ( [#] W) <> {} ;

      hence thesis by A4, TOPS_2: 43;

    end;

    theorem :: YELLOW14:37



     Th37: for M be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of M st for i be Element of M holds (J . i) is T_0 TopSpace holds ( product J) is T_0

    proof

      let M be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of M such that

       A1: for i be Element of M holds (J . i) is T_0 TopSpace;

      for x,y be Point of ( product J) st x <> y holds ( Cl {x}) <> ( Cl {y})

      proof

        let x,y be Point of ( product J) such that

         A2: x <> y and

         A3: ( Cl {x}) = ( Cl {y});

        y in the carrier of ( product J);

        then y in ( product ( Carrier J)) by WAYBEL18:def 3;

        then ( dom y) = ( dom ( Carrier J)) by CARD_3: 9;

        then

         A4: ( dom y) = M by PARTFUN1:def 2;

        x in the carrier of ( product J);

        then x in ( product ( Carrier J)) by WAYBEL18:def 3;

        then ( dom x) = ( dom ( Carrier J)) by CARD_3: 9;

        then ( dom x) = M by PARTFUN1:def 2;

        then

        consider i be object such that

         A5: i in M and

         A6: (x . i) <> (y . i) by A2, A4, FUNCT_1: 2;

        reconsider i as Element of M by A5;



         A7: ( pi (( Cl {y}),i)) = ( Cl {(y . i)}) by Th31;

        (J . i) is T_0 TopSpace & ( pi (( Cl {x}),i)) = ( Cl {(x . i)}) by A1, Th31;

        hence contradiction by A3, A6, A7, TSP_1:def 5;

      end;

      hence thesis by TSP_1:def 5;

    end;

    registration

      let I be non empty set, T be non empty T_0 TopSpace;

      cluster ( product (I --> T)) -> T_0;

      coherence

      proof

        for i be Element of I holds ((I --> T) . i) is T_0 TopSpace;

        hence thesis by Th37;

      end;

    end

    theorem :: YELLOW14:38



     Th38: for M be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of M st for i be Element of M holds (J . i) is T_1 TopSpace-like holds ( product J) is T_1

    proof

      let M be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of M such that

       A1: for i be Element of M holds (J . i) is T_1 TopSpace-like;

      for p be Point of ( product J) holds {p} is closed

      proof

        let p be Point of ( product J);

         {p} = ( Cl {p})

        proof

          thus {p} c= ( Cl {p}) by PRE_TOPC: 18;

          let a be object;

          assume

           A2: a in ( Cl {p});

          then

          reconsider a, p as Element of ( product J);



           A3: for i be object st i in M holds (a . i) = (p . i)

          proof

            let i be object;

            assume i in M;

            then

            reconsider i as Element of M;

            (J . i) is TopSpace & (J . i) is T_1 by A1;

            then

             A4: {(p . i)} is closed by URYSOHN1: 19;

            (a . i) in ( Cl {(p . i)}) by A2, Th29;

            then (a . i) in {(p . i)} by A4, PRE_TOPC: 22;

            hence thesis by TARSKI:def 1;

          end;

          p in the carrier of ( product J);

          then p in ( product ( Carrier J)) by WAYBEL18:def 3;

          then ( dom p) = ( dom ( Carrier J)) by CARD_3: 9;

          then

           A5: ( dom p) = M by PARTFUN1:def 2;

          a in the carrier of ( product J);

          then a in ( product ( Carrier J)) by WAYBEL18:def 3;

          then ( dom a) = ( dom ( Carrier J)) by CARD_3: 9;

          then ( dom a) = M by PARTFUN1:def 2;

          then a = p by A5, A3, FUNCT_1: 2;

          hence thesis by TARSKI:def 1;

        end;

        hence thesis;

      end;

      hence thesis by URYSOHN1: 19;

    end;

    registration

      let I be non empty set, T be non empty T_1 TopSpace;

      cluster ( product (I --> T)) -> T_1;

      coherence

      proof

        for i be Element of I holds ((I --> T) . i) is T_1 TopSpace-like;

        hence thesis by Th38;

      end;

    end