waybel26.miz



    begin

    notation

      let I be set;

      let J be RelStr-yielding ManySortedSet of I;

      synonym I -POS_prod J for product J;

    end

    notation

      let I be set;

      let J be TopStruct-yielding non-Empty ManySortedSet of I;

      synonym I -TOP_prod J for product J;

    end

    definition

      let X,Y be non empty TopSpace;

      :: WAYBEL26:def1

      func oContMaps (X,Y) -> non empty strict RelStr equals ( ContMaps (X,( Omega Y)));

      coherence ;

    end

    registration

      let X,Y be non empty TopSpace;

      cluster ( oContMaps (X,Y)) -> reflexive transitive constituted-Functions;

      coherence ;

    end

    registration

      let X be non empty TopSpace;

      let Y be non empty T_0 TopSpace;

      cluster ( oContMaps (X,Y)) -> antisymmetric;

      coherence ;

    end

    theorem :: WAYBEL26:1

    

     Th1: for X,Y be non empty TopSpace holds for a be set holds a is Element of ( oContMaps (X,Y)) iff a is continuous Function of X, ( Omega Y)

    proof

      let X,Y be non empty TopSpace;

      let a be set;

      hereby

        assume a is Element of ( oContMaps (X,Y));

        then ex f be Function of X, ( Omega Y) st a = f & f is continuous by WAYBEL24:def 3;

        hence a is continuous Function of X, ( Omega Y);

      end;

      assume a is continuous Function of X, ( Omega Y);

      hence thesis by WAYBEL24:def 3;

    end;

    theorem :: WAYBEL26:2

    

     Th2: for X,Y be non empty TopSpace holds for a be set holds a is Element of ( oContMaps (X,Y)) iff a is continuous Function of X, Y

    proof

      let X,Y be non empty TopSpace;

      let a be set;

      

       A1: the TopStruct of ( Omega Y) = the TopStruct of Y & the TopStruct of X = the TopStruct of X by WAYBEL25:def 2;

      hereby

        assume a is Element of ( oContMaps (X,Y));

        then a is continuous Function of X, ( Omega Y) by Th1;

        hence a is continuous Function of X, Y by A1, YELLOW12: 36;

      end;

      assume a is continuous Function of X, Y;

      then a is continuous Function of X, ( Omega Y) by A1, YELLOW12: 36;

      hence thesis by Th1;

    end;

    theorem :: WAYBEL26:3

    

     Th3: for X,Y be non empty TopSpace holds for a,b be Element of ( oContMaps (X,Y)) holds for f,g be Function of X, ( Omega Y) st a = f & b = g holds a <= b iff f <= g

    proof

      let X,Y be non empty TopSpace;

      let a,b be Element of ( oContMaps (X,Y));

      

       A1: ( oContMaps (X,Y)) is full SubRelStr of (( Omega Y) |^ the carrier of X) by WAYBEL24:def 3;

      then

      reconsider x = a, y = b as Element of (( Omega Y) |^ the carrier of X) by YELLOW_0: 58;

      

       A2: a <= b iff x <= y by A1, YELLOW_0: 59, YELLOW_0: 60;

      let f,g be Function of X, ( Omega Y);

      assume a = f & b = g;

      hence thesis by A2, WAYBEL10: 11;

    end;

    definition

      let X,Y be non empty TopSpace;

      let x be Point of X;

      let A be Subset of ( oContMaps (X,Y));

      :: original: pi

      redefine

      func pi (A,x) -> Subset of ( Omega Y) ;

      coherence

      proof

        set XY = ( oContMaps (X,Y));

        XY is SubRelStr of (( Omega Y) |^ the carrier of X) by WAYBEL24:def 3;

        then the carrier of XY c= the carrier of (( Omega Y) |^ the carrier of X) by YELLOW_0:def 13;

        then

        reconsider A as Subset of (( Omega Y) |^ the carrier of X) by XBOOLE_1: 1;

        ( pi (A,x)) is Subset of ( Omega Y);

        hence thesis;

      end;

    end

    registration

      let X,Y be non empty TopSpace;

      let x be set;

      let A be non empty Subset of ( oContMaps (X,Y));

      cluster ( pi (A,x)) -> non empty;

      coherence

      proof

        set XY = ( oContMaps (X,Y));

        XY is SubRelStr of (( Omega Y) |^ the carrier of X) by WAYBEL24:def 3;

        then the carrier of XY c= the carrier of (( Omega Y) |^ the carrier of X) by YELLOW_0:def 13;

        then

        reconsider A as non empty Subset of (( Omega Y) |^ the carrier of X) by XBOOLE_1: 1;

        ( pi (A,x)) <> {} ;

        hence thesis;

      end;

    end

    theorem :: WAYBEL26:4

    

     Th4: ( Omega Sierpinski_Space ) is TopAugmentation of ( BoolePoset { 0 })

    proof

      set S = the strict Scott TopAugmentation of ( BoolePoset { 0 });

      

       A1: the RelStr of S = ( BoolePoset { 0 }) by YELLOW_9:def 4;

      ( BoolePoset { 0 }) = ( InclPoset ( bool { 0 })) by YELLOW_1: 4;

      then

       A2: the carrier of ( BoolePoset { 0 }) = { 0 , 1} by YELLOW14: 1, YELLOW_1: 1;

      the carrier of Sierpinski_Space = { 0 , 1} & the topology of S = the topology of Sierpinski_Space by WAYBEL18: 12, WAYBEL18:def 9;

      

      then ( Omega Sierpinski_Space ) = ( Omega S) by A2, A1, WAYBEL25: 13

      .= S by WAYBEL25: 15;

      hence thesis;

    end;

    theorem :: WAYBEL26:5

    

     Th5: for X be non empty TopSpace holds ex f be Function of ( InclPoset the topology of X), ( oContMaps (X, Sierpinski_Space )) st f is isomorphic & for V be open Subset of X holds (f . V) = ( chi (V,the carrier of X))

    proof

      let X be non empty TopSpace;

      deffunc F( set) = ( chi ($1,the carrier of X));

      consider f be Function such that

       A1: ( dom f) = the topology of X and

       A2: for a be set st a in the topology of X holds (f . a) = F(a) from FUNCT_1:sch 5;

      

       A3: ( rng f) c= the carrier of ( oContMaps (X, Sierpinski_Space ))

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider a be object such that

         A4: a in ( dom f) and

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

        reconsider a as Subset of X by A1, A4;

        a is open by A1, A4, PRE_TOPC:def 2;

        then ( chi (a,the carrier of X)) is continuous Function of X, Sierpinski_Space by YELLOW16: 46;

        then x is continuous Function of X, Sierpinski_Space by A1, A2, A4, A5;

        then x is Element of ( oContMaps (X, Sierpinski_Space )) by Th2;

        hence thesis;

      end;

      set S = ( InclPoset the topology of X);

      

       A6: the carrier of ( InclPoset the topology of X) = the topology of X by YELLOW_1: 1;

      then

      reconsider f as Function of ( InclPoset the topology of X), ( oContMaps (X, Sierpinski_Space )) by A1, A3, FUNCT_2: 2;

       A7:

      now

        let x,y be Element of S;

        x in the topology of X & y in the topology of X by A6;

        then

        reconsider V = x, W = y as open Subset of X by PRE_TOPC:def 2;

        set cx = ( chi (V,the carrier of X)), cy = ( chi (W,the carrier of X));

        

         A8: (f . x) = cx & (f . y) = cy by A2, A6;

        cx is continuous Function of X, Sierpinski_Space by YELLOW16: 46;

        then

         A9: cx is Element of ( oContMaps (X, Sierpinski_Space )) by Th2;

        cy is continuous Function of X, Sierpinski_Space by YELLOW16: 46;

        then cy is Element of ( oContMaps (X, Sierpinski_Space )) by Th2;

        then

        reconsider cx, cy as continuous Function of X, ( Omega Sierpinski_Space ) by A9, Th1;

        x <= y iff V c= W by YELLOW_1: 3;

        then x <= y iff cx <= cy by Th4, YELLOW16: 49;

        hence x <= y iff (f . x) <= (f . y) by A8, Th3;

      end;

      set T = ( oContMaps (X, Sierpinski_Space ));

      

       A10: ( rng f) = the carrier of T

      proof

        the topology of Sierpinski_Space = { {} , {1}, { 0 , 1}} by WAYBEL18:def 9;

        then {1} in the topology of Sierpinski_Space by ENUMSET1:def 1;

        then

        reconsider V = {1} as open Subset of Sierpinski_Space by PRE_TOPC:def 2;

        thus ( rng f) c= the carrier of T;

        let t be object;

        assume t in the carrier of T;

        then

        reconsider g = t as continuous Function of X, Sierpinski_Space by Th2;

        ( [#] Sierpinski_Space ) <> {} ;

        then

         A11: (g " V) is open by TOPS_2: 43;

        then

        reconsider c = ( chi ((g " V),the carrier of X)) as Function of X, Sierpinski_Space by YELLOW16: 46;

        now

          let x be Element of X;

          x in (g " V) or not x in (g " V);

          then

           A12: (g . x) in V & (c . x) = 1 or not (g . x) in V & (c . x) = 0 by FUNCT_2: 38, FUNCT_3:def 3;

          the carrier of Sierpinski_Space = { 0 , 1} by WAYBEL18:def 9;

          then (g . x) = 0 or (g . x) = 1 by TARSKI:def 2;

          hence (g . x) = (c . x) by A12, TARSKI:def 1;

        end;

        then

         A13: g = c by FUNCT_2: 63;

        

         A14: (g " V) in the topology of X by A11, PRE_TOPC:def 2;

        then (f . (g " V)) = ( chi ((g " V),the carrier of X)) by A2;

        hence thesis by A1, A14, A13, FUNCT_1:def 3;

      end;

      take f;

      f is one-to-one

      proof

        let x,y be Element of S;

        x in the topology of X & y in the topology of X by A6;

        then

        reconsider V = x, W = y as Subset of X;

        (f . x) = ( chi (V,the carrier of X)) & (f . y) = ( chi (W,the carrier of X)) by A2, A6;

        hence thesis by FUNCT_3: 38;

      end;

      hence f is isomorphic by A10, A7, WAYBEL_0: 66;

      let V be open Subset of X;

      V in the topology of X by PRE_TOPC:def 2;

      hence thesis by A2;

    end;

    theorem :: WAYBEL26:6

    

     Th6: for X be non empty TopSpace holds (( InclPoset the topology of X),( oContMaps (X, Sierpinski_Space ))) are_isomorphic

    proof

      let X be non empty TopSpace;

      consider f be Function of ( InclPoset the topology of X), ( oContMaps (X, Sierpinski_Space )) such that

       A1: f is isomorphic and for V be open Subset of X holds (f . V) = ( chi (V,the carrier of X)) by Th5;

      take f;

      thus thesis by A1;

    end;

    definition

      let X,Y,Z be non empty TopSpace;

      let f be continuous Function of Y, Z;

      :: WAYBEL26:def2

      func oContMaps (X,f) -> Function of ( oContMaps (X,Y)), ( oContMaps (X,Z)) means

      : Def2: for g be continuous Function of X, Y holds (it . g) = (f * g);

      uniqueness

      proof

        let G1,G2 be Function of ( oContMaps (X,Y)), ( oContMaps (X,Z)) such that

         A1: for g be continuous Function of X, Y holds (G1 . g) = (f * g) and

         A2: for g be continuous Function of X, Y holds (G2 . g) = (f * g);

        now

          thus the carrier of ( oContMaps (X,Z)) <> {} ;

          let x be Element of ( oContMaps (X,Y));

          reconsider g = x as continuous Function of X, Y by Th2;

          

          thus (G1 . x) = (f * g) by A1

          .= (G2 . x) by A2;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      existence

      proof

        deffunc F( set) = ($1 (#) f);

        consider F be Function such that

         A3: ( dom F) = the carrier of ( oContMaps (X,Y)) and

         A4: for x be set st x in the carrier of ( oContMaps (X,Y)) holds (F . x) = F(x) from FUNCT_1:sch 5;

        ( rng F) c= the carrier of ( oContMaps (X,Z))

        proof

          let y be object;

          assume y in ( rng F);

          then

          consider x be object such that

           A5: x in ( dom F) and

           A6: y = (F . x) by FUNCT_1:def 3;

          reconsider g = x as continuous Function of X, Y by A3, A5, Th2;

          y = (g (#) f) by A3, A4, A5, A6

          .= (f * g);

          then y is Element of ( oContMaps (X,Z)) by Th2;

          hence thesis;

        end;

        then

        reconsider F as Function of ( oContMaps (X,Y)), ( oContMaps (X,Z)) by A3, FUNCT_2: 2;

        take F;

        let g be continuous Function of X, Y;

        g is Element of ( oContMaps (X,Y)) by Th2;

        

        hence (F . g) = (g (#) f) by A4

        .= (f * g);

      end;

      :: WAYBEL26:def3

      func oContMaps (f,X) -> Function of ( oContMaps (Z,X)), ( oContMaps (Y,X)) means

      : Def3: for g be continuous Function of Z, X holds (it . g) = (g * f);

      uniqueness

      proof

        let G1,G2 be Function of ( oContMaps (Z,X)), ( oContMaps (Y,X)) such that

         A7: for g be continuous Function of Z, X holds (G1 . g) = (g * f) and

         A8: for g be continuous Function of Z, X holds (G2 . g) = (g * f);

        now

          thus the carrier of ( oContMaps (Y,X)) <> {} ;

          let x be Element of ( oContMaps (Z,X));

          reconsider g = x as continuous Function of Z, X by Th2;

          

          thus (G1 . x) = (g * f) by A7

          .= (G2 . x) by A8;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      existence

      proof

        deffunc F( set) = (f (#) $1);

        consider F be Function such that

         A9: ( dom F) = the carrier of ( oContMaps (Z,X)) and

         A10: for x be set st x in the carrier of ( oContMaps (Z,X)) holds (F . x) = F(x) from FUNCT_1:sch 5;

        ( rng F) c= the carrier of ( oContMaps (Y,X))

        proof

          let y be object;

          assume y in ( rng F);

          then

          consider x be object such that

           A11: x in ( dom F) and

           A12: y = (F . x) by FUNCT_1:def 3;

          reconsider g = x as continuous Function of Z, X by A9, A11, Th2;

          y = (f (#) g) by A9, A10, A11, A12

          .= (g * f);

          then y is Element of ( oContMaps (Y,X)) by Th2;

          hence thesis;

        end;

        then

        reconsider F as Function of ( oContMaps (Z,X)), ( oContMaps (Y,X)) by A9, FUNCT_2: 2;

        take F;

        let g be continuous Function of Z, X;

        g is Element of ( oContMaps (Z,X)) by Th2;

        

        hence (F . g) = (f (#) g) by A10

        .= (g * f);

      end;

    end

    theorem :: WAYBEL26:7

    

     Th7: for X be non empty TopSpace holds for Y be monotone-convergence T_0-TopSpace holds ( oContMaps (X,Y)) is up-complete

    proof

      let X be non empty TopSpace;

      let Y be monotone-convergence T_0-TopSpace;

      ( ContMaps (X,( Omega Y))) is directed-sups-inheriting full SubRelStr of (( Omega Y) |^ the carrier of X) by WAYBEL24:def 3, WAYBEL25: 43;

      hence thesis by YELLOW16: 5;

    end;

    theorem :: WAYBEL26:8

    

     Th8: for X,Y,Z be non empty TopSpace holds for f be continuous Function of Y, Z holds ( oContMaps (X,f)) is monotone

    proof

      let X,Y,Z be non empty TopSpace;

      let f be continuous Function of Y, Z;

      let a,b be Element of ( oContMaps (X,Y));

       the TopStruct of Y = the TopStruct of ( Omega Y) & the TopStruct of Z = the TopStruct of ( Omega Z) by WAYBEL25:def 2;

      then

      reconsider f9 = f as continuous Function of ( Omega Y), ( Omega Z) by YELLOW12: 36;

      reconsider g1 = a, g2 = b as continuous Function of X, ( Omega Y) by Th1;

      set Xf = ( oContMaps (X,f));

      reconsider fg1 = (f9 * g1), fg2 = (f9 * g2) as Function of X, ( Omega Z);

      g2 is continuous Function of X, Y by Th2;

      then

       A1: (Xf . b) = (f9 * g2) by Def2;

      assume a <= b;

      then

       A2: g1 <= g2 by Th3;

      now

        let x be set;

        assume x in the carrier of X;

        then

        reconsider x9 = x as Element of X;

        

         A3: ((f9 * g2) . x9) = (f9 . (g2 . x9)) by FUNCT_2: 15;

        (ex a,b be Element of ( Omega Y) st a = (g1 . x9) & b = (g2 . x9) & a <= b) & ((f9 * g1) . x9) = (f9 . (g1 . x9)) by A2, FUNCT_2: 15;

        then ((f9 * g1) . x9) <= ((f9 * g2) . x9) by A3, WAYBEL_1:def 2;

        hence ex a,b be Element of ( Omega Z) st a = ((f9 * g1) . x) & b = ((f9 * g2) . x) & a <= b;

      end;

      then

       A4: fg1 <= fg2;

      g1 is continuous Function of X, Y by Th2;

      then (Xf . a) = (f9 * g1) by Def2;

      hence (Xf . a) <= (Xf . b) by A1, A4, Th3;

    end;

    theorem :: WAYBEL26:9

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

    proof

      let X,Y be non empty TopSpace;

      let f be continuous Function of Y, Y such that

       A1: f is idempotent;

      set Xf = ( oContMaps (X,f));

      now

        let g be Element of ( oContMaps (X,Y));

        reconsider h = g as continuous Function of X, Y by Th2;

        

        thus ((Xf * Xf) . g) = (Xf . (Xf . g)) by FUNCT_2: 15

        .= (Xf . (f * h)) by Def2

        .= (f * (f * h)) by Def2

        .= ((f * f) * h) by RELAT_1: 36

        .= (f * h) by A1, QUANTAL1:def 9

        .= (Xf . g) by Def2;

      end;

      then (Xf * Xf) = Xf by FUNCT_2: 63;

      hence thesis by QUANTAL1:def 9;

    end;

    theorem :: WAYBEL26:10

    

     Th10: for X,Y,Z be non empty TopSpace holds for f be continuous Function of Y, Z holds ( oContMaps (f,X)) is monotone

    proof

      let X,Y,Z be non empty TopSpace;

      let f be continuous Function of Y, Z;

      let a,b be Element of ( oContMaps (Z,X));

      reconsider g1 = a, g2 = b as continuous Function of Z, ( Omega X) by Th1;

      set Xf = ( oContMaps (f,X));

       the TopStruct of Y = the TopStruct of ( Omega Y) & the TopStruct of Z = the TopStruct of ( Omega Z) by WAYBEL25:def 2;

      then

      reconsider f9 = f as continuous Function of ( Omega Y), ( Omega Z) by YELLOW12: 36;

      g2 is continuous Function of Z, X by Th2;

      then

       A1: (Xf . b) = (g2 qua Function * f9) by Def3;

      g1 is continuous Function of Z, X by Th2;

      then

       A2: (Xf . a) = (g1 qua Function * f9) by Def3;

      then

      reconsider fg1 = (g1 qua Function * f9), fg2 = (g2 qua Function * f9) as Function of Y, ( Omega X) by A1, Th1;

      assume a <= b;

      then

       A3: g1 <= g2 by Th3;

      now

        let x be set;

        assume x in the carrier of Y;

        then

        reconsider x9 = x as Element of Y;

        ((g1 * f) . x9) = (g1 . (f . x9)) & ((g2 * f) . x9) = (g2 . (f . x9)) by FUNCT_2: 15;

        hence ex a,b be Element of ( Omega X) st a = ((g1 * f) . x) & b = ((g2 * f) . x) & a <= b by A3;

      end;

      then fg1 <= fg2;

      hence (Xf . a) <= (Xf . b) by A2, A1, Th3;

    end;

    theorem :: WAYBEL26:11

    

     Th11: for X,Y be non empty TopSpace holds for f be continuous Function of Y, Y st f is idempotent holds ( oContMaps (f,X)) is idempotent

    proof

      let X,Y be non empty TopSpace;

      let f be continuous Function of Y, Y such that

       A1: f is idempotent;

      set fX = ( oContMaps (f,X));

      now

        let g be Element of ( oContMaps (Y,X));

        reconsider h = g as continuous Function of Y, X by Th2;

        

        thus ((fX * fX) . g) = (fX . (fX . g)) by FUNCT_2: 15

        .= (fX . (h * f)) by Def3

        .= ((h * f) * f) by Def3

        .= (h * (f * f)) by RELAT_1: 36

        .= (h * f) by A1, QUANTAL1:def 9

        .= (fX . g) by Def3;

      end;

      then (fX * fX) = fX by FUNCT_2: 63;

      hence thesis by QUANTAL1:def 9;

    end;

    theorem :: WAYBEL26:12

    

     Th12: for X,Y,Z be non empty TopSpace holds for f be continuous Function of Y, Z holds for x be Element of X, A be Subset of ( oContMaps (X,Y)) holds ( pi ((( oContMaps (X,f)) .: A),x)) = (f .: ( pi (A,x)))

    proof

      let X,Y,Z be non empty TopSpace;

      let f be continuous Function of Y, Z;

      set Xf = ( oContMaps (X,f));

      let x be Element of X, A be Subset of ( oContMaps (X,Y));

      thus ( pi ((Xf .: A),x)) c= (f .: ( pi (A,x)))

      proof

        let a be object;

        assume a in ( pi ((Xf .: A),x));

        then

        consider h be Function such that

         A1: h in (Xf .: A) and

         A2: a = (h . x) by CARD_3:def 6;

        consider g be object such that

         A3: g in the carrier of ( oContMaps (X,Y)) and

         A4: g in A and

         A5: h = (Xf . g) by A1, FUNCT_2: 64;

        reconsider g as continuous Function of X, Y by A3, Th2;

        h = (f * g) by A5, Def2;

        then

         A6: a = (f . (g . x)) by A2, FUNCT_2: 15;

        (g . x) in ( pi (A,x)) by A4, CARD_3:def 6;

        hence thesis by A6, FUNCT_2: 35;

      end;

      let a be object;

      assume a in (f .: ( pi (A,x)));

      then

      consider b be object such that b in the carrier of Y and

       A7: b in ( pi (A,x)) and

       A8: a = (f . b) by FUNCT_2: 64;

      consider g be Function such that

       A9: g in A and

       A10: b = (g . x) by A7, CARD_3:def 6;

      reconsider g as continuous Function of X, Y by A9, Th2;

      (f * g) = (Xf . g) by Def2;

      then

       A11: (f * g) in (Xf .: A) by A9, FUNCT_2: 35;

      a = ((f * g) . x) by A8, A10, FUNCT_2: 15;

      hence thesis by A11, CARD_3:def 6;

    end;

    theorem :: WAYBEL26:13

    

     Th13: for X be non empty TopSpace holds for Y,Z be monotone-convergence T_0-TopSpace holds for f be continuous Function of Y, Z holds ( oContMaps (X,f)) is directed-sups-preserving

    proof

      let X be non empty TopSpace;

      let Y,Z be monotone-convergence T_0-TopSpace;

      let f be continuous Function of Y, Z;

      let A be Subset of ( oContMaps (X,Y));

      reconsider sA = ( sup A) as continuous Function of X, Y by Th2;

      set Xf = ( oContMaps (X,f));

      reconsider sfA = ( sup (Xf .: A)), XfsA = (Xf . ( sup A)) as Function of X, ( Omega Z) by Th1;

      reconsider XZ = ( oContMaps (X,Z)) as directed-sups-inheriting non empty full SubRelStr of (( Omega Z) |^ the carrier of X) by WAYBEL24:def 3, WAYBEL25: 43;

      assume A is non empty directed;

      then

      reconsider A9 = A as non empty directed Subset of ( oContMaps (X,Y));

      reconsider fA9 = (Xf .: A9) as non empty directed Subset of ( oContMaps (X,Z)) by Th8, YELLOW_2: 15;

      reconsider XY = ( oContMaps (X,Y)) as directed-sups-inheriting non empty full SubRelStr of (( Omega Y) |^ the carrier of X) by WAYBEL24:def 3, WAYBEL25: 43;

      reconsider B = A9 as non empty directed Subset of XY;

      reconsider B9 = B as non empty directed Subset of (( Omega Y) |^ the carrier of X) by YELLOW_2: 7;

      reconsider fB = fA9 as non empty directed Subset of XZ;

      reconsider fB9 = fB as non empty directed Subset of (( Omega Z) |^ the carrier of X) by YELLOW_2: 7;

      assume ex_sup_of (A,( oContMaps (X,Y)));

      set I = the carrier of X;

      set J1 = (I --> ( Omega Y));

      set J2 = (I --> ( Omega Z));

       the TopStruct of Y = the TopStruct of ( Omega Y) & the TopStruct of Z = the TopStruct of ( Omega Z) by WAYBEL25:def 2;

      then

      reconsider f9 = f as continuous Function of ( Omega Y), ( Omega Z) by YELLOW12: 36;

       ex_sup_of (fB9,(( Omega Z) |^ the carrier of X)) by WAYBEL_0: 75;

      then

       A1: ( sup fB9) = ( sup (( oContMaps (X,f)) .: A)) by WAYBEL_0: 7;

      ( oContMaps (X,Z)) is up-complete & fA9 is directed by Th7;

      hence ex_sup_of ((( oContMaps (X,f)) .: A),( oContMaps (X,Z))) by WAYBEL_0: 75;

      

       A2: (( Omega Z) |^ I) = (I -POS_prod J2) by YELLOW_1:def 5;

      then

      reconsider fB99 = fB9 as non empty directed Subset of (I -POS_prod J2);

      now

        let x be Element of X;

        (J2 . x) = ( Omega Z) & ( pi (fB99,x)) is directed by FUNCOP_1: 7, YELLOW16: 35;

        hence ex_sup_of (( pi (fB99,x)),(J2 . x)) by WAYBEL_0: 75;

      end;

      then

       A3: ex_sup_of (fB99,(I -POS_prod J2)) by YELLOW16: 31;

      

       A4: (( Omega Y) |^ the carrier of X) = (I -POS_prod J1) by YELLOW_1:def 5;

      then

      reconsider B99 = B9 as non empty directed Subset of (I -POS_prod J1);

      

       A5: ex_sup_of (B9,(( Omega Y) |^ the carrier of X)) by WAYBEL_0: 75;

      then

       A6: ( sup B9) = ( sup A) by WAYBEL_0: 7;

      now

        let x be Element of X;

        

         A7: (J1 . x) = ( Omega Y) by FUNCOP_1: 7;

        then

        reconsider Bx = ( pi (B99,x)) as directed non empty Subset of ( Omega Y) by YELLOW16: 35;

        

         A8: (J2 . x) = ( Omega Z) & ex_sup_of (Bx,( Omega Y)) by FUNCOP_1: 7, WAYBEL_0: 75;

        

         A9: (( sup B99) . x) = ( sup ( pi (B99,x))) by A5, A4, YELLOW16: 33;

        

         A10: f9 preserves_sup_of Bx & ( pi (fB99,x)) = (f9 .: Bx) by Th12, WAYBEL_0:def 37;

        

        thus (sfA . x) = ( sup ( pi (fB99,x))) by A1, A2, A3, YELLOW16: 33

        .= (f . ( sup Bx)) by A8, A10

        .= ((f * sA) . x) by A6, A4, A9, A7, FUNCT_2: 15

        .= (XfsA . x) by Def2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: WAYBEL26:14

    

     Th14: for X,Y,Z be non empty TopSpace holds for f be continuous Function of Y, Z holds for x be Element of Y, A be Subset of ( oContMaps (Z,X)) holds ( pi ((( oContMaps (f,X)) .: A),x)) = ( pi (A,(f . x)))

    proof

      let X,Y,Z be non empty TopSpace;

      let f be continuous Function of Y, Z;

      set fX = ( oContMaps (f,X));

      let x be Element of Y, A be Subset of ( oContMaps (Z,X));

      thus ( pi ((fX .: A),x)) c= ( pi (A,(f . x)))

      proof

        let a be object;

        assume a in ( pi ((fX .: A),x));

        then

        consider h be Function such that

         A1: h in (fX .: A) and

         A2: a = (h . x) by CARD_3:def 6;

        consider g be object such that

         A3: g in the carrier of ( oContMaps (Z,X)) and

         A4: g in A and

         A5: h = (fX . g) by A1, FUNCT_2: 64;

        reconsider g as continuous Function of Z, X by A3, Th2;

        h = (g * f) by A5, Def3;

        then a = (g . (f . x)) by A2, FUNCT_2: 15;

        hence thesis by A4, CARD_3:def 6;

      end;

      let a be object;

      assume a in ( pi (A,(f . x)));

      then

      consider g be Function such that

       A6: g in A and

       A7: a = (g . (f . x)) by CARD_3:def 6;

      reconsider g as continuous Function of Z, X by A6, Th2;

      (g * f) = (fX . g) by Def3;

      then

       A8: (g * f) in (fX .: A) by A6, FUNCT_2: 35;

      a = ((g * f) . x) by A7, FUNCT_2: 15;

      hence thesis by A8, CARD_3:def 6;

    end;

    theorem :: WAYBEL26:15

    

     Th15: for Y,Z be non empty TopSpace holds for X be monotone-convergence T_0-TopSpace holds for f be continuous Function of Y, Z holds ( oContMaps (f,X)) is directed-sups-preserving

    proof

      let Y,Z be non empty TopSpace;

      let X be monotone-convergence T_0-TopSpace;

      let f be continuous Function of Y, Z;

      let A be Subset of ( oContMaps (Z,X));

      reconsider sA = ( sup A) as continuous Function of Z, X by Th2;

      set fX = ( oContMaps (f,X));

      reconsider sfA = ( sup (fX .: A)), XfsA = (fX . ( sup A)) as Function of Y, ( Omega X) by Th1;

      reconsider YX = ( oContMaps (Y,X)) as directed-sups-inheriting non empty full SubRelStr of (( Omega X) |^ the carrier of Y) by WAYBEL24:def 3, WAYBEL25: 43;

      assume A is non empty directed;

      then

      reconsider A9 = A as non empty directed Subset of ( oContMaps (Z,X));

      reconsider fA9 = (fX .: A9) as non empty directed Subset of ( oContMaps (Y,X)) by Th10, YELLOW_2: 15;

      reconsider ZX = ( oContMaps (Z,X)) as directed-sups-inheriting non empty full SubRelStr of (( Omega X) |^ the carrier of Z) by WAYBEL24:def 3, WAYBEL25: 43;

      reconsider B = A9 as non empty directed Subset of ZX;

      reconsider B9 = B as non empty directed Subset of (( Omega X) |^ the carrier of Z) by YELLOW_2: 7;

      reconsider fB = fA9 as non empty directed Subset of YX;

      reconsider fB9 = fB as non empty directed Subset of (( Omega X) |^ the carrier of Y) by YELLOW_2: 7;

      assume ex_sup_of (A,( oContMaps (Z,X)));

      set I1 = the carrier of Z, I2 = the carrier of Y;

      set J1 = (I1 --> ( Omega X));

      set J2 = (I2 --> ( Omega X));

       ex_sup_of (fB9,(( Omega X) |^ the carrier of Y)) by WAYBEL_0: 75;

      then

       A1: ( sup fB9) = ( sup (( oContMaps (f,X)) .: A)) by WAYBEL_0: 7;

      ( oContMaps (Y,X)) is up-complete & fA9 is directed by Th7;

      hence ex_sup_of ((( oContMaps (f,X)) .: A),( oContMaps (Y,X))) by WAYBEL_0: 75;

      

       A2: (( Omega X) |^ I2) = (I2 -POS_prod J2) by YELLOW_1:def 5;

      then

      reconsider fB99 = fB9 as non empty directed Subset of (I2 -POS_prod J2);

      now

        let x be Element of Y;

        (J2 . x) = ( Omega X) & ( pi (fB99,x)) is directed by FUNCOP_1: 7, YELLOW16: 35;

        hence ex_sup_of (( pi (fB99,x)),(J2 . x)) by WAYBEL_0: 75;

      end;

      then

       A3: ex_sup_of (fB99,(I2 -POS_prod J2)) by YELLOW16: 31;

      

       A4: (( Omega X) |^ I1) = (I1 -POS_prod J1) by YELLOW_1:def 5;

      then

      reconsider B99 = B9 as non empty directed Subset of (I1 -POS_prod J1);

      

       A5: ex_sup_of (B9,(( Omega X) |^ the carrier of Z)) by WAYBEL_0: 75;

      then

       A6: ( sup B9) = ( sup A) by WAYBEL_0: 7;

      now

        let x be Element of Y;

        

         A7: (J1 . (f . x)) = ( Omega X) & (J2 . x) = ( Omega X) by FUNCOP_1: 7;

        

         A8: ( pi (fB99,x)) = ( pi (B99,(f . x))) by Th14;

        

        thus (sfA . x) = ( sup ( pi (fB99,x))) by A1, A2, A3, YELLOW16: 33

        .= (( sup B99) . (f . x)) by A5, A4, A7, A8, YELLOW16: 33

        .= ((sA * f) . x) by A6, A4, FUNCT_2: 15

        .= (XfsA . x) by Def3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: WAYBEL26:16

    

     Th16: for X,Z be non empty TopSpace holds for Y be non empty SubSpace of Z holds ( oContMaps (X,Y)) is full SubRelStr of ( oContMaps (X,Z))

    proof

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

      set XY = ( oContMaps (X,Y)), XZ = ( oContMaps (X,Z));

      

       A1: ( Omega Y) is full SubRelStr of ( Omega Z) by WAYBEL25: 17;

      

       A2: ( [#] Y) c= ( [#] Z) by PRE_TOPC:def 4;

      XY is SubRelStr of XZ

      proof

        thus

         A3: the carrier of XY c= the carrier of XZ

        proof

          let x be object;

          assume x in the carrier of XY;

          then

          reconsider f = x as continuous Function of X, Y by Th2;

          ( dom f) = the carrier of X & ( rng f) c= the carrier of Z by A2, FUNCT_2:def 1;

          then x is continuous Function of X, Z by FUNCT_2: 2, PRE_TOPC: 26;

          then x is Element of XZ by Th2;

          hence thesis;

        end;

        let x,y be object;

        assume

         A4: [x, y] in the InternalRel of XY;

        reconsider x, y as Element of XY by A4, ZFMISC_1: 87;

        reconsider a = x, b = y as Element of XZ by A3;

        reconsider f = x, g = y as continuous Function of X, ( Omega Y) by Th1;

        reconsider f9 = a, g9 = b as continuous Function of X, ( Omega Z) by Th1;

        x <= y by A4, ORDERS_2:def 5;

        then f <= g by Th3;

        then f9 <= g9 by A1, YELLOW16: 2;

        then a <= b by Th3;

        hence thesis by ORDERS_2:def 5;

      end;

      then

      reconsider XY as non empty SubRelStr of XZ;

      

       A5: (the InternalRel of XZ |_2 the carrier of XY) = (the InternalRel of XZ /\ [:the carrier of XY, the carrier of XY:]) by WELLORD1:def 6;

      the InternalRel of XY = (the InternalRel of XZ |_2 the carrier of XY) qua set

      proof

        the InternalRel of XY c= the InternalRel of XZ by YELLOW_0:def 13;

        hence the InternalRel of XY c= (the InternalRel of XZ |_2 the carrier of XY) by A5, XBOOLE_1: 19;

        let x,y be object;

        assume

         A6: [x, y] in (the InternalRel of XZ |_2 the carrier of XY);

        then

         A7: [x, y] in [:the carrier of XY, the carrier of XY:] by A5, XBOOLE_0:def 4;

        reconsider x, y as Element of XY by A7, ZFMISC_1: 87;

        the carrier of XY c= the carrier of XZ by YELLOW_0:def 13;

        then

        reconsider a = x, b = y as Element of XZ;

        reconsider f9 = a, g9 = b as continuous Function of X, ( Omega Z) by Th1;

        reconsider f = x, g = y as continuous Function of X, ( Omega Y) by Th1;

         [a, b] in the InternalRel of XZ by A5, A6, XBOOLE_0:def 4;

        then a <= b by ORDERS_2:def 5;

        then f9 <= g9 by Th3;

        then f <= g by A1, YELLOW16: 3;

        then x <= y by Th3;

        hence thesis by ORDERS_2:def 5;

      end;

      hence thesis by YELLOW_0:def 14;

    end;

    theorem :: WAYBEL26:17

    

     Th17: for Z be monotone-convergence T_0-TopSpace holds for Y be non empty SubSpace of Z holds for f be continuous Function of Z, Y st f is being_a_retraction holds ( Omega Y) is directed-sups-inheriting SubRelStr of ( Omega Z)

    proof

      let Z be monotone-convergence T_0-TopSpace;

      let Y be non empty SubSpace of Z;

      reconsider OZ = ( Omega Z) as non empty up-complete non empty Poset;

      reconsider OY = ( Omega Y) as full non empty SubRelStr of ( Omega Z) by WAYBEL25: 17;

      let f be continuous Function of Z, Y;

      

       A1: the RelStr of OZ = the RelStr of ( Omega Z);

      ( [#] Y) c= ( [#] Z) by PRE_TOPC:def 4;

      then ( dom f) = the carrier of Z & ( rng f) c= the carrier of Z by FUNCT_2:def 1;

      then

       A2: f is continuous Function of Z, Z by PRE_TOPC: 26, RELSET_1: 4;

       the TopStruct of ( Omega Z) = the TopStruct of Z by WAYBEL25:def 2;

      then

      reconsider f9 = f as continuous Function of ( Omega Z), ( Omega Z) by A2, YELLOW12: 36;

      reconsider g = f9 as Function of OZ, OZ;

      assume

       A3: f is being_a_retraction;

      then g is idempotent directed-sups-preserving by YELLOW16: 45;

      then

       A4: ( Image g) is directed-sups-inheriting by YELLOW16: 6;

       the TopStruct of ( Omega Y) = the TopStruct of Y & ( rng g) = the carrier of ( subrelstr ( rng g)) by WAYBEL25:def 2, YELLOW_0:def 15;

      then OY is directed-sups-inheriting by A3, A4, A1, WAYBEL21: 22, YELLOW16: 44;

      hence thesis;

    end;

    

     Lm1: for Z be monotone-convergence T_0-TopSpace holds for Y be non empty SubSpace of Z holds for f be continuous Function of Z, Y st f is being_a_retraction holds Y is monotone-convergence

    proof

      let Z be monotone-convergence T_0-TopSpace;

      let Y be non empty SubSpace of Z;

      let f be continuous Function of Z, Y;

      assume f is being_a_retraction;

      then Y is_a_retract_of Z;

      hence thesis by WAYBEL25: 36, YELLOW16: 56;

    end;

    theorem :: WAYBEL26:18

    

     Th18: for X be non empty TopSpace holds for Z be monotone-convergence T_0-TopSpace holds for Y be non empty SubSpace of Z holds for f be continuous Function of Z, Y st f is being_a_retraction holds ( oContMaps (X,f)) is_a_retraction_of (( oContMaps (X,Z)),( oContMaps (X,Y)))

    proof

      let X be non empty TopSpace;

      let Z be monotone-convergence T_0-TopSpace;

      let Y be non empty SubSpace of Z;

      set XY = ( oContMaps (X,Y)), XZ = ( oContMaps (X,Z));

      reconsider uXZ = XZ as up-complete non empty Poset by Th7;

      let f be continuous Function of Z, Y;

      set F = ( oContMaps (X,f));

      reconsider sXY = XY as full non empty SubRelStr of uXZ by Th16;

      assume

       A1: f is being_a_retraction;

      then

      reconsider Y9 = Y as monotone-convergence T_0-TopSpace by Lm1;

      ( oContMaps (X,Y9)) is up-complete by Th7;

      hence F is directed-sups-preserving Function of XZ, XY by Th13;

      

       A2: the carrier of sXY c= the carrier of uXZ by YELLOW_0:def 13;

       A3:

      now

        let x be object;

        

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

        

         A5: ( rng f) = the carrier of Y & f is idempotent by A1, YELLOW16: 44, YELLOW16: 45;

        assume

         A6: x in the carrier of XY;

        then

        reconsider a = x as Element of XZ by A2;

        reconsider a as continuous Function of X, Z by Th2;

        x is Function of X, Y by A6, Th2;

        then ( rng a) c= the carrier of Y by RELAT_1:def 19;

        then (f * a) = a by A5, A4, YELLOW16: 4;

        

        hence (( id XY) . x) = (f * a) by A6, FUNCT_1: 18

        .= (F . a) by Def2

        .= ((F | the carrier of XY) . x) by A6, FUNCT_1: 49;

      end;

      (F | the carrier of XY) is Function of the carrier of XY, the carrier of XY by A2, FUNCT_2: 32;

      then ( dom ( id XY)) = the carrier of XY & ( dom (F | the carrier of XY)) = the carrier of XY by FUNCT_2:def 1;

      hence (F | the carrier of XY) = ( id XY) by A3, FUNCT_1: 2;

      ( Omega Y) is directed-sups-inheriting full SubRelStr of ( Omega Z) by A1, Th17, WAYBEL25: 17;

      then ( oContMaps (X,Y9)) is directed-sups-inheriting full non empty SubRelStr of (( Omega Y) |^ the carrier of X) & (( Omega Y) |^ the carrier of X) is directed-sups-inheriting full SubRelStr of (( Omega Z) |^ the carrier of X) by WAYBEL24:def 3, WAYBEL25: 43, YELLOW16: 39, YELLOW16: 42;

      then ( oContMaps (X,Z)) is directed-sups-inheriting full non empty SubRelStr of (( Omega Z) |^ the carrier of X) & ( oContMaps (X,Y)) is directed-sups-inheriting full SubRelStr of (( Omega Z) |^ the carrier of X) by WAYBEL24:def 3, WAYBEL25: 43, YELLOW16: 26, YELLOW16: 27;

      hence thesis by Th16, YELLOW16: 28;

    end;

    theorem :: WAYBEL26:19

    

     Th19: for X be non empty TopSpace holds for Z be monotone-convergence T_0-TopSpace holds for Y be non empty SubSpace of Z st Y is_a_retract_of Z holds ( oContMaps (X,Y)) is_a_retract_of ( oContMaps (X,Z))

    proof

      let X be non empty TopSpace;

      let Z be monotone-convergence T_0-TopSpace;

      let Y be non empty SubSpace of Z;

      given f be continuous Function of Z, Y such that

       A1: f is being_a_retraction;

      take ( oContMaps (X,f));

      thus thesis by A1, Th18;

    end;

    theorem :: WAYBEL26:20

    

     Th20: for X,Y,Z be non empty TopSpace holds for f be continuous Function of Y, Z st f is being_homeomorphism holds ( oContMaps (X,f)) is isomorphic

    proof

      let X,Y,Z be non empty TopSpace;

      let f be continuous Function of Y, Z;

      set XY = ( oContMaps (X,Y)), XZ = ( oContMaps (X,Z));

      assume

       A1: f is being_homeomorphism;

      then

      reconsider g = (f " ) as continuous Function of Z, Y by TOPS_2:def 5;

      set Xf = ( oContMaps (X,f)), Xg = ( oContMaps (X,g));

      

       A2: f is one-to-one & ( rng f) = ( [#] Z) by A1, TOPS_2:def 5;

      now

        let a be Element of XZ;

        reconsider h = a as continuous Function of X, Z by Th2;

        

        thus ((Xf * Xg) . a) = (Xf . (Xg . a)) by FUNCT_2: 15

        .= (Xf . (g * h)) by Def2

        .= (f * (g * h)) by Def2

        .= ((f * g) * h) by RELAT_1: 36

        .= (( id the carrier of Z) * h) by A2, TOPS_2: 52

        .= a by FUNCT_2: 17

        .= (( id XZ) . a);

      end;

      then

       A3: (Xf * Xg) = ( id XZ) by FUNCT_2: 63;

      

       A4: ( dom f) = ( [#] Y) by A1, TOPS_2:def 5;

      now

        let a be Element of XY;

        reconsider h = a as continuous Function of X, Y by Th2;

        

        thus ((Xg * Xf) . a) = (Xg . (Xf . a)) by FUNCT_2: 15

        .= (Xg . (f * h)) by Def2

        .= (g * (f * h)) by Def2

        .= ((g * f) * h) by RELAT_1: 36

        .= (( id the carrier of Y) * h) by A2, A4, TOPS_2: 52

        .= a by FUNCT_2: 17

        .= (( id XY) . a);

      end;

      then

       A5: (Xg * Xf) = ( id XY) by FUNCT_2: 63;

      Xf is monotone & Xg is monotone by Th8;

      hence thesis by A5, A3, YELLOW16: 15;

    end;

    theorem :: WAYBEL26:21

    

     Th21: for X,Y,Z be non empty TopSpace st (Y,Z) are_homeomorphic holds (( oContMaps (X,Y)),( oContMaps (X,Z))) are_isomorphic

    proof

      let X,Y,Z be non empty TopSpace;

      given f be Function of Y, Z such that

       A1: f is being_homeomorphism;

      reconsider f as continuous Function of Y, Z by A1, TOPS_2:def 5;

      take ( oContMaps (X,f));

      thus thesis by A1, Th20;

    end;

    theorem :: WAYBEL26:22

    

     Th22: for X be non empty TopSpace holds for Z be monotone-convergence T_0-TopSpace holds for Y be non empty SubSpace of Z st Y is_a_retract_of Z & ( oContMaps (X,Z)) is complete continuous holds ( oContMaps (X,Y)) is complete continuous by Th19, YELLOW16: 21, YELLOW16: 22;

    theorem :: WAYBEL26:23

    

     Th23: for X be non empty TopSpace holds for Y,Z be monotone-convergence T_0-TopSpace st Y is_Retract_of Z & ( oContMaps (X,Z)) is complete continuous holds ( oContMaps (X,Y)) is complete continuous

    proof

      let X be non empty TopSpace;

      let Y,Z be monotone-convergence T_0-TopSpace;

      assume Y is_Retract_of Z;

      then

      consider S be non empty SubSpace of Z such that

       A1: S is_a_retract_of Z and

       A2: (S,Y) are_homeomorphic by YELLOW16: 57;

      assume ( oContMaps (X,Z)) is complete continuous;

      then

       A3: ( oContMaps (X,S)) is complete continuous by A1, Th22;

      (( oContMaps (X,S)),( oContMaps (X,Y))) are_isomorphic by A2, Th21;

      hence thesis by A3, WAYBEL15: 9, WAYBEL20: 18;

    end;

    theorem :: WAYBEL26:24

    

     Th24: for Y be non trivial T_0-TopSpace st not Y is T_1 holds Sierpinski_Space is_Retract_of Y

    proof

      let Y be non trivial T_0-TopSpace;

      given p,q be Point of Y such that

       A1: p <> q and

       A2: for W,V be Subset of Y st W is open & V is open & p in W & not q in W & q in V holds p in V;

      (ex V be Subset of Y st V is open & p in V & not q in V) or ex W be Subset of Y st W is open & not p in W & q in W by A1, TSP_1:def 3;

      then

      consider V be Subset of Y such that

       A3: V is open and

       A4: p in V & not q in V or not p in V & q in V;

      

       A5: the TopStruct of ( Omega Y) = the TopStruct of Y by WAYBEL25:def 2;

      then

      consider x,y be Element of ( Omega Y) such that

       A6: p in V & not q in V & x = q & y = p or not p in V & q in V & x = p & y = q by A4;

      now

        let W be open Subset of ( Omega Y);

        W is open Subset of Y by A5, TOPS_3: 76;

        hence x in W implies y in W by A2, A3, A6;

      end;

      then (( 0 ,1) --> (x,y)) is continuous Function of Sierpinski_Space , ( Omega Y) by YELLOW16: 47;

      then

      reconsider i = (( 0 ,1) --> (x,y)) as continuous Function of Sierpinski_Space , Y by A5, YELLOW12: 36;

      reconsider V as open Subset of ( Omega Y) by A3, A5, TOPS_3: 76;

      reconsider c = ( chi (V,the carrier of Y)) as continuous Function of Y, Sierpinski_Space by A3, YELLOW16: 46;

      (c * i) = ( id Sierpinski_Space ) by A5, A6, YELLOW16: 48;

      hence thesis by WAYBEL25:def 1;

    end;

    theorem :: WAYBEL26:25

    

     Th25: for X be non empty TopSpace holds for Y be non trivial T_0-TopSpace st ( oContMaps (X,Y)) is with_suprema holds not Y is T_1

    proof

      let X be non empty TopSpace;

      let Y be non trivial T_0-TopSpace;

      consider a,b be Element of Y such that

       A1: a <> b by STRUCT_0:def 10;

      set i = the Element of X;

      reconsider f = (X --> a), g = (X --> b) as continuous Function of X, Y;

      assume ( oContMaps (X,Y)) is with_suprema;

      then

      reconsider XY = ( oContMaps (X,Y)) as sup-Semilattice;

      reconsider ef = f, eg = g as Element of XY by Th2;

      reconsider h = (ef "\/" eg), f = ef, g = eg as continuous Function of X, ( Omega Y) by Th1;

      

       A2: (f . i) = a & (g . i) = b by FUNCOP_1: 7;

      now

        eg <= (ef "\/" eg) by YELLOW_0: 22;

        then g <= h by Th3;

        then

         A3: ex x,y be Element of ( Omega Y) st x = (g . i) & y = (h . i) & x <= y;

        ef <= (ef "\/" eg) by YELLOW_0: 22;

        then f <= h by Th3;

        then

         A4: ex x,y be Element of ( Omega Y) st x = (f . i) & y = (h . i) & x <= y;

        assume

         A5: not ex x,y be Element of ( Omega Y) st x <= y & x <> y;

        then not ((f . i) <= (h . i) & (f . i) <> (h . i));

        hence contradiction by A1, A2, A5, A4, A3;

      end;

      then

      consider x,y be Element of ( Omega Y) such that

       A6: x <= y and

       A7: x <> y;

      

       A8: the TopStruct of ( Omega Y) = the TopStruct of Y by WAYBEL25:def 2;

      then

      reconsider p = x, q = y as Element of Y;

      take p, q;

      thus p <> q by A7;

      let W,V be Subset of Y;

      assume W is open;

      then

      reconsider W as open Subset of ( Omega Y) by A8, TOPS_3: 76;

      W is upper;

      hence thesis by A6;

    end;

    registration

      cluster Sierpinski_Space -> non trivial monotone-convergence;

      coherence

      proof

        

         A1: 1 in { 0 , 1} by TARSKI:def 2;

        the carrier of Sierpinski_Space = { 0 , 1} & 0 in { 0 , 1} by TARSKI:def 2, WAYBEL18:def 9;

        hence thesis by A1;

      end;

    end

    registration

      cluster injective monotone-convergence non trivial for T_0-TopSpace;

      existence

      proof

        take Sierpinski_Space ;

        thus thesis;

      end;

    end

    theorem :: WAYBEL26:26

    

     Th26: for X be non empty TopSpace holds for Y be monotone-convergence non trivial T_0-TopSpace st ( oContMaps (X,Y)) is complete continuous holds ( InclPoset the topology of X) is continuous

    proof

      let X be non empty TopSpace;

      let Y be monotone-convergence non trivial T_0-TopSpace;

      assume

       A1: ( oContMaps (X,Y)) is complete continuous;

      then Sierpinski_Space is_Retract_of Y by Th24, Th25;

      then

       A2: ( oContMaps (X, Sierpinski_Space )) is complete continuous by A1, Th23;

      (( InclPoset the topology of X),( oContMaps (X, Sierpinski_Space ))) are_isomorphic by Th6;

      hence thesis by A2, WAYBEL15: 9, WAYBEL_1: 6;

    end;

    theorem :: WAYBEL26:27

    

     Th27: for X be non empty TopSpace, x be Point of X holds for Y be monotone-convergence T_0-TopSpace holds ex F be directed-sups-preserving projection Function of ( oContMaps (X,Y)), ( oContMaps (X,Y)) st (for f be continuous Function of X, Y holds (F . f) = (X --> (f . x))) & ex h be continuous Function of X, X st h = (X --> x) & F = ( oContMaps (h,Y))

    proof

      let X be non empty TopSpace, x be Point of X;

      let Y be monotone-convergence T_0-TopSpace;

      set XY = ( oContMaps (X,Y));

      reconsider f = (X --> x) as continuous Function of X, X;

      set F = ( oContMaps (f,Y));

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

      

      then (f * f) = (the carrier of X --> (f . x)) by FUNCOP_1: 17

      .= f by FUNCOP_1: 7;

      then f is idempotent by QUANTAL1:def 9;

      then F is directed-sups-preserving idempotent Function of XY, XY by Th11, Th15;

      then

      reconsider F as directed-sups-preserving projection Function of XY, XY by WAYBEL_1:def 13;

      take F;

      hereby

        let h be continuous Function of X, Y;

        

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

        

        thus (F . h) = (h * (the carrier of X --> x)) by Def3

        .= (X --> (h . x)) by A1, FUNCOP_1: 17;

      end;

      thus thesis;

    end;

    theorem :: WAYBEL26:28

    

     Th28: for X be non empty TopSpace, Y be monotone-convergence T_0-TopSpace st ( oContMaps (X,Y)) is complete continuous holds ( Omega Y) is complete continuous

    proof

      let X be non empty TopSpace, Y be monotone-convergence T_0-TopSpace such that

       A1: ( oContMaps (X,Y)) is complete continuous;

      set b = the Element of X;

      

       A2: the TopStruct of ( Omega Y) = the TopStruct of Y by WAYBEL25:def 2;

      consider F be directed-sups-preserving projection Function of ( oContMaps (X,Y)), ( oContMaps (X,Y)) such that

       A3: for f be continuous Function of X, Y holds (F . f) = (X --> (f . b)) and ex h be continuous Function of X, X st h = (X --> b) & F = ( oContMaps (h,Y)) by Th27;

      ( oContMaps (X,Y)) is full SubRelStr of (( Omega Y) |^ the carrier of X) by WAYBEL24:def 3;

      then

      reconsider imF = ( Image F) as full non empty SubRelStr of (( Omega Y) |^ the carrier of X) by YELLOW16: 26;

      

       A4: the carrier of imF = ( rng F) by YELLOW_0:def 15;

      

       A5: ( dom F) = the carrier of ( oContMaps (X,Y)) by FUNCT_2: 52;

      now

        let a be set;

        hereby

          assume a is Element of imF;

          then

          consider h be object such that

           A6: h in ( dom F) and

           A7: a = (F . h) by A4, FUNCT_1:def 3;

          reconsider h as continuous Function of X, Y by A6, Th2;

          reconsider x = (h . b) as Element of ( Omega Y) by A2;

          a = (X --> (h . b)) by A3, A7

          .= (the carrier of X --> x);

          hence ex x be Element of ( Omega Y) st a = (the carrier of X --> x);

        end;

        given x be Element of ( Omega Y) such that

         A8: a = (the carrier of X --> x);

        a = (X --> x) by A8;

        then

         A9: a is Element of ( oContMaps (X,Y)) by Th1;

        then

        reconsider h = a as continuous Function of X, Y by Th2;

        

         A10: (X --> (h . b)) = (the carrier of X --> (h . b));

        (h . b) = x by A8, FUNCOP_1: 7;

        then (F . a) = (X --> x) by A3, A10;

        hence a is Element of imF by A4, A5, A8, A9, FUNCT_1:def 3;

      end;

      then (( Omega Y),imF) are_isomorphic by YELLOW16: 50;

      then

       A11: (imF,( Omega Y)) are_isomorphic by WAYBEL_1: 6;

      ( Image F) is complete continuous LATTICE by A1, WAYBEL15: 15, YELLOW_2: 35;

      hence thesis by A11, WAYBEL15: 9, WAYBEL20: 18;

    end;

    theorem :: WAYBEL26:29

    

     Th29: for X be non empty 1-sorted, I be non empty set holds for J be TopStruct-yielding non-Empty ManySortedSet of I holds for f be Function of X, (I -TOP_prod J) holds for i be Element of I holds (( commute f) . i) = (( proj (J,i)) * f)

    proof

      let X be non empty 1-sorted, I be non empty set;

      let J be TopStruct-yielding non-Empty ManySortedSet of I;

      let f be Function of X, (I -TOP_prod J);

      

       A1: the carrier of (I -TOP_prod J) = ( product ( Carrier J)) by WAYBEL18:def 3;

      let i be Element of I;

      

       A2: ( dom ( Carrier J)) = I by PARTFUN1:def 2;

      

       A3: ( rng f) c= ( Funcs (I,( Union ( Carrier J))))

      proof

        let g be object;

        assume g in ( rng f);

        then

        consider h be Function such that

         A4: g = h and

         A5: ( dom h) = I and

         A6: for x be object st x in I holds (h . x) in (( Carrier J) . x) by A1, A2, CARD_3:def 5;

        ( rng h) c= ( Union ( Carrier J))

        proof

          let y be object;

          

           A7: ( dom ( Carrier J)) = I by PARTFUN1:def 2;

          assume y in ( rng h);

          then

          consider x be object such that

           A8: x in ( dom h) and

           A9: y = (h . x) by FUNCT_1:def 3;

          (h . x) in (( Carrier J) . x) by A5, A6, A8;

          hence thesis by A5, A8, A9, A7, CARD_5: 2;

        end;

        hence thesis by A4, A5, FUNCT_2:def 2;

      end;

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

      then

       A10: f in ( Funcs (the carrier of X,( Funcs (I,( Union ( Carrier J)))))) by A3, FUNCT_2:def 2;

      then ( commute f) in ( Funcs (I,( Funcs (the carrier of X,( Union ( Carrier J)))))) by FUNCT_6: 55;

      then

       A11: ex g be Function st ( commute f) = g & ( dom g) = I & ( rng g) c= ( Funcs (the carrier of X,( Union ( Carrier J)))) by FUNCT_2:def 2;

      then (( commute f) . i) in ( rng ( commute f)) by FUNCT_1:def 3;

      then

      consider g be Function such that

       A12: (( commute f) . i) = g and

       A13: ( dom g) = the carrier of X and ( rng g) c= ( Union ( Carrier J)) by A11, FUNCT_2:def 2;

       A14:

      now

        let x be object;

        

         A15: ( dom ( proj (( Carrier J),i))) = ( product ( Carrier J)) by CARD_3:def 16;

        assume x in the carrier of X;

        then

        reconsider a = x as Element of X;

        consider h be Function such that

         A16: (f . a) = h and ( dom h) = I and for x be object st x in I holds (h . x) in (( Carrier J) . x) by A1, A2, CARD_3:def 5;

        ((( proj (J,i)) * f) . a) = (( proj (J,i)) . (f . a)) by FUNCT_2: 15

        .= (( proj (( Carrier J),i)) . (f . a)) by WAYBEL18:def 4

        .= (h . i) by A1, A16, A15, CARD_3:def 16;

        hence (g . x) = ((( proj (J,i)) * f) . x) by A10, A12, A16, FUNCT_6: 56;

      end;

      ( dom (( proj (J,i)) * f)) = the carrier of X by FUNCT_2:def 1;

      hence thesis by A12, A13, A14, FUNCT_1: 2;

    end;

    theorem :: WAYBEL26:30

    

     Th30: for S be 1-sorted, M be set holds ( Carrier (M --> S)) = (M --> the carrier of S)

    proof

      let S be 1-sorted, M be set;

      now

        let i be object;

        assume

         A1: i in M;

        then ((M --> S) . i) = S & ex R be 1-sorted st R = ((M --> S) . i) & (( Carrier (M --> S)) . i) = the carrier of R by FUNCOP_1: 7, PRALG_1:def 15;

        hence (( Carrier (M --> S)) . i) = ((M --> the carrier of S) . i) by A1, FUNCOP_1: 7;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: WAYBEL26:31

    

     Th31: for X,Y be non empty TopSpace, M be non empty set holds for f be continuous Function of X, (M -TOP_prod (M --> Y)) holds ( commute f) is Function of M, the carrier of ( oContMaps (X,Y))

    proof

      let X,Y be non empty TopSpace, M be non empty set;

      let f be continuous Function of X, (M -TOP_prod (M --> Y));

      

       A1: ( rng f) c= ( Funcs (M,the carrier of Y))

      proof

        let g be object;

        assume

         A2: g in ( rng f);

        

         A3: ( dom (M --> the carrier of Y)) = M by FUNCOP_1: 13;

        the carrier of (M -TOP_prod (M --> Y)) = ( product ( Carrier (M --> Y))) by WAYBEL18:def 3

        .= ( product (M --> the carrier of Y)) by Th30;

        then

        consider h be Function such that

         A4: g = h and

         A5: ( dom h) = M and

         A6: for x be object st x in M holds (h . x) in ((M --> the carrier of Y) . x) by A2, A3, CARD_3:def 5;

        ( rng h) c= the carrier of Y

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A7: x in ( dom h) and

           A8: y = (h . x) by FUNCT_1:def 3;

          ((M --> the carrier of Y) . x) = the carrier of Y by A5, A7, FUNCOP_1: 7;

          hence thesis by A5, A6, A7, A8;

        end;

        hence thesis by A4, A5, FUNCT_2:def 2;

      end;

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

      then f in ( Funcs (the carrier of X,( Funcs (M,the carrier of Y)))) by A1, FUNCT_2:def 2;

      then

       A9: ( commute f) in ( Funcs (M,( Funcs (the carrier of X,the carrier of Y)))) by FUNCT_6: 55;

      

       A10: ( rng ( commute f)) c= the carrier of ( oContMaps (X,Y))

      proof

        let g be object;

        assume g in ( rng ( commute f));

        then

        consider i be object such that

         A11: i in ( dom ( commute f)) and

         A12: g = (( commute f) . i) by FUNCT_1:def 3;

        ex h be Function st ( commute f) = h & ( dom h) = M & ( rng h) c= ( Funcs (the carrier of X,the carrier of Y)) by A9, FUNCT_2:def 2;

        then

        reconsider i as Element of M by A11;

        

         A13: ((M --> Y) . i) = Y by FUNCOP_1: 7;

        g = (( proj ((M --> Y),i)) * f) by A12, Th29;

        then g is continuous Function of X, Y by A13, WAYBEL18: 6;

        then g is Element of ( oContMaps (X,Y)) by Th2;

        hence thesis;

      end;

      ex g be Function st ( commute f) = g & ( dom g) = M & ( rng g) c= ( Funcs (the carrier of X,the carrier of Y)) by A9, FUNCT_2:def 2;

      hence thesis by A10, FUNCT_2: 2;

    end;

    theorem :: WAYBEL26:32

    

     Th32: for X,Y be non empty TopSpace holds the carrier of ( oContMaps (X,Y)) c= ( Funcs (the carrier of X,the carrier of Y))

    proof

      let X,Y be non empty TopSpace;

      ( oContMaps (X,Y)) is SubRelStr of (( Omega Y) |^ the carrier of X) by WAYBEL24:def 3;

      then

       A1: the carrier of ( oContMaps (X,Y)) c= the carrier of (( Omega Y) |^ the carrier of X) by YELLOW_0:def 13;

       the TopStruct of Y = the TopStruct of ( Omega Y) by WAYBEL25:def 2;

      hence thesis by A1, YELLOW_1: 28;

    end;

    theorem :: WAYBEL26:33

    

     Th33: for X,Y be non empty TopSpace, M be non empty set holds for f be Function of M, the carrier of ( oContMaps (X,Y)) holds ( commute f) is continuous Function of X, (M -TOP_prod (M --> Y))

    proof

      let X,Y be non empty TopSpace, M be non empty set;

      let f be Function of M, the carrier of ( oContMaps (X,Y));

      reconsider B = ( product_prebasis (M --> Y)) as prebasis of (M -TOP_prod (M --> Y)) by WAYBEL18:def 3;

      

       A1: ( Carrier (M --> Y)) = (M --> the carrier of Y) by Th30;

      the carrier of ( oContMaps (X,Y)) c= ( Funcs (the carrier of X,the carrier of Y)) by Th32;

      then ( dom f) = M & ( rng f) c= ( Funcs (the carrier of X,the carrier of Y)) by FUNCT_2:def 1;

      then

       A2: f in ( Funcs (M,( Funcs (the carrier of X,the carrier of Y)))) by FUNCT_2:def 2;

      then ( commute f) in ( Funcs (the carrier of X,( Funcs (M,the carrier of Y)))) by FUNCT_6: 55;

      then

       A3: ex g be Function st ( commute f) = g & ( dom g) = the carrier of X & ( rng g) c= ( Funcs (M,the carrier of Y)) by FUNCT_2:def 2;

      the carrier of (M -TOP_prod (M --> Y)) = ( product ( Carrier (M --> Y))) by WAYBEL18:def 3;

      then the carrier of (M -TOP_prod (M --> Y)) = ( Funcs (M,the carrier of Y)) by A1, CARD_3: 11;

      then

      reconsider g = ( commute f) as Function of X, (M -TOP_prod (M --> Y)) by A3, FUNCT_2: 2;

      now

        let P be Subset of (M -TOP_prod (M --> Y));

        assume P in B;

        then

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

         A4: i in M and

         A5: V is open and

         A6: T = ((M --> Y) . i) and

         A7: P = ( product (( Carrier (M --> Y)) +* (i,V))) by WAYBEL18:def 2;

        reconsider i as Element of M by A4;

        set FP = (( Carrier (M --> Y)) +* (i,V));

        

         A8: ( dom FP) = ( dom ( Carrier (M --> Y))) by FUNCT_7: 30;

        reconsider fi = (f . i) as continuous Function of X, Y by Th2;

        

         A9: ( dom ( Carrier (M --> Y))) = M by A1, FUNCOP_1: 13;

        then

         A10: (FP . i) = V by FUNCT_7: 31;

        

         A11: T = Y by A4, A6, FUNCOP_1: 7;

        now

          let x be set;

          hereby

            reconsider Q = (fi " V) as Subset of X;

            assume

             A12: x in (g " P);

            then (g . x) in P by FUNCT_2: 38;

            then

            consider gx be Function such that

             A13: (g . x) = gx and ( dom gx) = ( dom FP) and

             A14: for z be object st z in ( dom FP) holds (gx . z) in (FP . z) by A7, CARD_3:def 5;

            

             A15: (gx . i) = (fi . x) by A2, A12, A13, FUNCT_6: 56;

            take Q;

            ( [#] Y) <> {} ;

            hence Q is open by A5, A11, TOPS_2: 43;

            thus Q c= (g " P)

            proof

              let a be object;

              assume

               A16: a in Q;

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

              then

              consider ga be Function such that

               A17: (g . a) = ga and

               A18: ( dom ga) = M and

               A19: ( rng ga) c= the carrier of Y by A3, FUNCT_2:def 2;

              

               A20: (fi . a) in V by A16, FUNCT_2: 38;

              now

                let z be object;

                assume

                 A21: z in M;

                then z <> i & ((M --> the carrier of Y) . z) = the carrier of Y or z = i by FUNCOP_1: 7;

                then z <> i & (ga . z) in ( rng ga) & (FP . z) = the carrier of Y or z = i by A1, A18, A21, FUNCT_1:def 3, FUNCT_7: 32;

                hence (ga . z) in (FP . z) by A2, A10, A16, A20, A17, A19, FUNCT_6: 56;

              end;

              then ga in P by A7, A8, A9, A18, CARD_3: 9;

              hence thesis by A16, A17, FUNCT_2: 38;

            end;

            (gx . i) in V by A8, A9, A10, A14;

            hence x in Q by A12, A15, FUNCT_2: 38;

          end;

          thus (ex Q be Subset of X st Q is open & Q c= (g " P) & x in Q) implies x in (g " P);

        end;

        hence (g " P) is open by TOPS_1: 25;

      end;

      hence thesis by YELLOW_9: 36;

    end;

    theorem :: WAYBEL26:34

    

     Th34: for X be non empty TopSpace, M be non empty set holds ex F be Function of ( oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space )))), (M -POS_prod (M --> ( oContMaps (X, Sierpinski_Space )))) st F is isomorphic & for f be continuous Function of X, (M -TOP_prod (M --> Sierpinski_Space )) holds (F . f) = ( commute f)

    proof

      let X be non empty TopSpace, M be non empty set;

      set S = Sierpinski_Space , S9M = (M -TOP_prod (M --> S));

      set XxxS9M = ( oContMaps (X,S9M)), XxS = ( oContMaps (X,S));

      set XxS9xM = (M -POS_prod (M --> XxS));

      deffunc F( Element of XxxS9M) = ( commute $1);

      consider F be ManySortedSet of the carrier of XxxS9M such that

       A1: for f be Element of XxxS9M holds (F . f) = F(f) from PBOOLE:sch 5;

      

       A2: ( dom F) = the carrier of XxxS9M by PARTFUN1:def 2;

      ( rng F) c= the carrier of XxS9xM

      proof

        let g be object;

        assume g in ( rng F);

        then

        consider f be object such that

         A3: f in ( dom F) and

         A4: g = (F . f) by FUNCT_1:def 3;

        reconsider f as continuous Function of X, S9M by A3, Th2;

        g = ( commute f) by A1, A3, A4;

        then

        reconsider g as Function of M, the carrier of XxS by Th31;

        ( dom g) = M & ( rng g) c= the carrier of XxS by FUNCT_2:def 1;

        then g in ( Funcs (M,the carrier of XxS)) by FUNCT_2:def 2;

        then g in the carrier of (XxS |^ M) by YELLOW_1: 28;

        hence thesis by YELLOW_1:def 5;

      end;

      then

      reconsider F as Function of XxxS9M, XxS9xM by A2, FUNCT_2: 2;

      deffunc F( Element of XxS9xM) = ( commute $1);

      consider G be ManySortedSet of the carrier of XxS9xM such that

       A5: for f be Element of XxS9xM holds (G . f) = F(f) from PBOOLE:sch 5;

      

       A6: ( dom G) = the carrier of XxS9xM by PARTFUN1:def 2;

      

       A7: ( rng G) c= the carrier of XxxS9M

      proof

        let g be object;

        assume g in ( rng G);

        then

        consider f be object such that

         A8: f in ( dom G) and

         A9: g = (G . f) by FUNCT_1:def 3;

        f in the carrier of (XxS |^ M) by A6, A8, YELLOW_1:def 5;

        then f in ( Funcs (M,the carrier of XxS)) by YELLOW_1: 28;

        then

        consider f9 be Function such that

         A10: f = f9 and

         A11: ( dom f9) = M & ( rng f9) c= the carrier of XxS by FUNCT_2:def 2;

        

         A12: f9 is Function of M, the carrier of XxS by A11, FUNCT_2: 2;

        g = ( commute f9) by A5, A8, A9, A10;

        then g is continuous Function of X, S9M by A12, Th33;

        then g is Element of XxxS9M by Th2;

        hence thesis;

      end;

      take F;

      

       A13: the carrier of S9M = ( product ( Carrier (M --> S))) by WAYBEL18:def 3

      .= ( product (M --> the carrier of S)) by Th30

      .= ( Funcs (M,the carrier of S)) by CARD_3: 11;

      reconsider G as Function of XxS9xM, XxxS9M by A6, A7, FUNCT_2: 2;

      

       A14: the carrier of XxxS9M c= ( Funcs (the carrier of X,the carrier of S9M)) by Th32;

      now

        let a be Element of XxxS9M;

        

         A15: ( commute ( commute a)) = a by A14, A13, FUNCT_6: 57;

        

        thus ((G * F) . a) = (G . (F . a)) by FUNCT_2: 15

        .= ( commute (F . a)) by A5

        .= a by A1, A15

        .= (( id XxxS9M) . a);

      end;

      then

       A16: (G * F) = ( id XxxS9M) by FUNCT_2: 63;

      

       A17: the RelStr of ( Omega S9M) = (M -POS_prod (M --> ( Omega S))) by WAYBEL25: 14;

      

       A18: F is monotone

      proof

        let a,b be Element of XxxS9M such that

         A19: a <= b;

        reconsider f9 = a, g9 = b as continuous Function of X, S9M by Th2;

        reconsider f = a, g = b as continuous Function of X, ( Omega S9M) by Th1;

        now

          let i be Element of M;

          

           A20: ((M --> XxS) . i) = XxS by FUNCOP_1: 7;

          then

          reconsider Fai = ((F . a) . i), Fbi = ((F . b) . i) as continuous Function of X, ( Omega S) by Th1;

          now

            let j be set;

            assume j in the carrier of X;

            then

            reconsider x = j as Element of X;

            b in the carrier of XxxS9M & (F . b) = ( commute g) by A1;

            then

             A21: (Fbi . x) = ((g9 . x) . i) by A14, A13, FUNCT_6: 56;

            reconsider fx = (f . x), gx = (g . x) as Element of (M -POS_prod (M --> ( Omega S))) by A17;

            a in the carrier of XxxS9M & (F . a) = ( commute f) by A1;

            then

             A22: (Fai . x) = ((f9 . x) . i) by A14, A13, FUNCT_6: 56;

            f <= g by A19, Th3;

            then ex a,b be Element of ( Omega S9M) st a = (f . x) & b = (g . x) & a <= b;

            then fx <= gx by A17, YELLOW_0: 1;

            then

             A23: (fx . i) <= (gx . i) by WAYBEL_3: 28;

            ((M --> ( Omega S)) . i) = ( Omega S) by FUNCOP_1: 7;

            hence ex a,b be Element of ( Omega S) st a = (Fai . j) & b = (Fbi . j) & a <= b by A22, A21, A23;

          end;

          then Fai <= Fbi;

          hence ((F . a) . i) <= ((F . b) . i) by A20, Th3;

        end;

        hence thesis by WAYBEL_3: 28;

      end;

      

       A24: the carrier of XxS9xM = the carrier of (XxS |^ M) by YELLOW_1:def 5

      .= ( Funcs (M,the carrier of XxS)) by YELLOW_1: 28;

      then

       A25: the carrier of XxS9xM c= ( Funcs (M,( Funcs (the carrier of X,the carrier of S)))) by Th32, FUNCT_5: 56;

      

       A26: G is monotone

      proof

        let a,b be Element of XxS9xM such that

         A27: a <= b;

        reconsider f = (G . a), g = (G . b) as continuous Function of X, ( Omega S9M) by Th1;

        now

          let i be set;

          assume i in the carrier of X;

          then

          reconsider x = i as Element of X;

          reconsider fx = (f . x), gx = (g . x) as Element of (M -POS_prod (M --> ( Omega S))) by A17;

          now

            let j be Element of M;

            

             A28: ((M --> XxS) . j) = XxS by FUNCOP_1: 7;

            then

            reconsider aj = (a . j), bj = (b . j) as continuous Function of X, ( Omega S) by Th1;

            (a . j) <= (b . j) by A27, WAYBEL_3: 28;

            then aj <= bj by A28, Th3;

            then

             A29: ex a,b be Element of ( Omega S) st a = (aj . x) & b = (bj . x) & a <= b;

            b in the carrier of XxS9xM & (G . b) = ( commute b) by A5;

            then

             A30: (gx . j) = (bj . x) by A25, FUNCT_6: 56;

            a in the carrier of XxS9xM & (G . a) = ( commute a) by A5;

            then (fx . j) = (aj . x) by A25, FUNCT_6: 56;

            hence (fx . j) <= (gx . j) by A30, A29, FUNCOP_1: 7;

          end;

          then fx <= gx by WAYBEL_3: 28;

          hence ex a,b be Element of ( Omega S9M) st a = (f . i) & b = (g . i) & a <= b by A17, YELLOW_0: 1;

        end;

        then f <= g;

        hence thesis by Th3;

      end;

      now

        let a be Element of XxS9xM;

        a in ( Funcs (M,the carrier of XxS)) & ( Funcs (M,the carrier of XxS)) c= ( Funcs (M,( Funcs (the carrier of X,the carrier of S)))) by A24, Th32, FUNCT_5: 56;

        then

         A31: ( commute ( commute a)) = a by FUNCT_6: 57;

        

        thus ((F * G) . a) = (F . (G . a)) by FUNCT_2: 15

        .= ( commute (G . a)) by A1

        .= a by A5, A31

        .= (( id XxS9xM) . a);

      end;

      then (F * G) = ( id XxS9xM) by FUNCT_2: 63;

      hence F is isomorphic by A18, A26, A16, YELLOW16: 15;

      let f be continuous Function of X, (M -TOP_prod (M --> Sierpinski_Space ));

      f is Element of XxxS9M by Th2;

      hence thesis by A1;

    end;

    theorem :: WAYBEL26:35

    

     Th35: for X be non empty TopSpace, M be non empty set holds (( oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space )))),(M -POS_prod (M --> ( oContMaps (X, Sierpinski_Space ))))) are_isomorphic

    proof

      let X be non empty TopSpace, M be non empty set;

      consider F be Function of ( oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space )))), (M -POS_prod (M --> ( oContMaps (X, Sierpinski_Space )))) such that

       A1: F is isomorphic and for f be continuous Function of X, (M -TOP_prod (M --> Sierpinski_Space )) holds (F . f) = ( commute f) by Th34;

      take F;

      thus thesis by A1;

    end;

    theorem :: WAYBEL26:36

    

     Th36: for X be non empty TopSpace st ( InclPoset the topology of X) is continuous holds for Y be injective T_0-TopSpace holds ( oContMaps (X,Y)) is complete continuous

    proof

      let X be non empty TopSpace such that

       A1: ( InclPoset the topology of X) is continuous;

      (( InclPoset the topology of X),( oContMaps (X, Sierpinski_Space ))) are_isomorphic by Th6;

      then

      reconsider XS = ( oContMaps (X, Sierpinski_Space )) as complete continuous non empty Poset by A1, WAYBEL15: 9, WAYBEL20: 18;

      let Y be injective T_0-TopSpace;

      consider M be non empty set such that

       A2: Y is_Retract_of (M -TOP_prod (M --> Sierpinski_Space )) by WAYBEL18: 19;

      for i be Element of M holds ((M --> Sierpinski_Space ) . i) is injective by FUNCOP_1: 7;

      then

      reconsider MS = (M -TOP_prod (M --> Sierpinski_Space )) as injective T_0-TopSpace by WAYBEL18: 7;

      for i be Element of M holds ((M --> XS) . i) is complete continuous LATTICE by FUNCOP_1: 7;

      then

       A3: (M -POS_prod (M --> XS)) is complete continuous by WAYBEL20: 33;

      ((M -POS_prod (M --> ( oContMaps (X, Sierpinski_Space )))),( oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space ))))) are_isomorphic by Th35, WAYBEL_1: 6;

      then ( oContMaps (X,MS)) is complete continuous by A3, WAYBEL15: 9, WAYBEL20: 18;

      hence thesis by A2, Th23;

    end;

    registration

      cluster non trivial complete Scott for TopLattice;

      existence

      proof

        set L = ( BoolePoset { 0 });

        set T = the Scott TopAugmentation of L;

        take T;

        ( BoolePoset { 0 }) = ( InclPoset ( bool { 0 })) & the RelStr of T = the RelStr of L by YELLOW_1: 4, YELLOW_9:def 4;

        then

         A1: the carrier of T = ( bool { 0 }) by YELLOW_1: 1;

         0 in { 0 , 1} & 1 in { 0 , 1} by TARSKI:def 2;

        hence thesis by A1, YELLOW14: 1;

      end;

    end

    theorem :: WAYBEL26:37

    for X be non empty TopSpace holds for L be non trivial complete Scott TopLattice holds ( oContMaps (X,L)) is complete continuous iff ( InclPoset the topology of X) is continuous & L is continuous

    proof

      let X be non empty TopSpace;

      let L be non trivial complete Scott TopLattice;

      

       A1: L is Scott TopAugmentation of L by YELLOW_9: 44;

      ( Omega L) = the TopRelStr of L by WAYBEL25: 15;

      then

       A2: the RelStr of ( Omega L) = the RelStr of L;

      

       A3: L is monotone-convergence by WAYBEL25: 29;

      hereby

        assume

         A4: ( oContMaps (X,L)) is complete continuous;

        hence ( InclPoset the topology of X) is continuous by A3, Th26;

        ( Omega L) is continuous by A1, A4, Th28;

        hence L is continuous by A2, YELLOW12: 15;

      end;

      thus thesis by A1, Th36;

    end;

    registration

      let f be Function;

      cluster ( Union ( disjoin f)) -> Relation-like;

      coherence by CARD_3: 21;

    end

    definition

      let f be Function;

      :: WAYBEL26:def4

      func *graph f -> Relation equals (( Union ( disjoin f)) ~ );

      correctness ;

    end

    reserve x,y for object,

f for Function;

    theorem :: WAYBEL26:38

    

     Th38: [x, y] in ( *graph f) iff x in ( dom f) & y in (f . x)

    proof

      

       A1: [x, y] in ( *graph f) iff [y, x] in ( Union ( disjoin f)) by RELAT_1:def 7;

      ( [y, x] `1 ) = y & ( [y, x] `2 ) = x;

      hence thesis by A1, CARD_3: 22;

    end;

    theorem :: WAYBEL26:39

    

     Th39: for X be finite set holds ( proj1 X) is finite & ( proj2 X) is finite

    proof

      deffunc F( object) = ($1 `1 );

      let X be finite set;

      consider f be Function such that

       A1: ( dom f) = X & for x be object st x in X holds (f . x) = F(x) from FUNCT_1:sch 3;

      

       A2: ( proj1 X) c= ( rng f)

      proof

        let x be object;

        assume x in ( proj1 X);

        then

        consider y be object such that

         A3: [x, y] in X by XTUPLE_0:def 12;

        ( [x, y] `1 ) = x;

        then (f . [x, y]) = x by A1, A3;

        hence thesis by A1, A3, FUNCT_1:def 3;

      end;

      ( rng f) is finite by A1, FINSET_1: 8;

      hence ( proj1 X) is finite by A2;

      deffunc F( object) = ($1 `2 );

      consider f be Function such that

       A4: ( dom f) = X & for x be object st x in X holds (f . x) = F(x) from FUNCT_1:sch 3;

      

       A5: ( proj2 X) c= ( rng f)

      proof

        let x be object;

        assume x in ( proj2 X);

        then

        consider y be object such that

         A6: [y, x] in X by XTUPLE_0:def 13;

        ( [y, x] `2 ) = x;

        then (f . [y, x]) = x by A4, A6;

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

      end;

      ( rng f) is finite by A4, FINSET_1: 8;

      hence thesis by A5;

    end;

    theorem :: WAYBEL26:40

    

     Th40: for X,Y be non empty TopSpace holds for S be Scott TopAugmentation of ( InclPoset the topology of Y) holds for f be Function of X, S st ( *graph f) is open Subset of [:X, Y:] holds f is continuous

    proof

      let X,Y be non empty TopSpace;

      let S be Scott TopAugmentation of ( InclPoset the topology of Y);

      let f be Function of X, S;

      

       A1: the RelStr of S = the RelStr of ( InclPoset the topology of Y) by YELLOW_9:def 4;

      

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

      assume ( *graph f) is open Subset of [:X, Y:];

      then

      consider AA be Subset-Family of [:X, Y:] such that

       A3: ( *graph f) = ( union AA) and

       A4: for e be set st e in AA holds ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] & X1 is open & Y1 is open by BORSUK_1: 5;

      

       A5: the carrier of ( InclPoset the topology of Y) = the topology of Y by YELLOW_1: 1;

       A6:

      now

        let P be Subset of S;

        assume

         A7: P is open;

        now

          let x be set;

          hereby

            defpred P[ object, object] means x in ($2 `1 ) & $1 in ($2 `2 ) & [:($2 `1 ), ($2 `2 ):] c= ( *graph f);

            assume

             A8: x in (f " P);

            then

            reconsider y = x as Element of X;

             A9:

            now

              let e be object;

              assume e in (f . x);

              then [x, e] in ( *graph f) by A2, A8, Th38;

              then

              consider V be set such that

               A10: [x, e] in V and

               A11: V in AA by A3, TARSKI:def 4;

              consider A be Subset of X, B be Subset of Y such that

               A12: V = [:A, B:] and

               A13: A is open & B is open by A4, A11;

              reconsider u = [A, B] as object;

              take u;

              A in the topology of X & B in the topology of Y by A13, PRE_TOPC:def 2;

              hence u in [:the topology of X, the topology of Y:] by ZFMISC_1: 87;

              thus P[e, u] by A3, A10, A11, A12, ZFMISC_1: 74, ZFMISC_1: 87;

            end;

            consider g be Function such that

             A14: ( dom g) = (f . x) & ( rng g) c= [:the topology of X, the topology of Y:] and

             A15: for a be object st a in (f . x) holds P[a, (g . a)] from FUNCT_1:sch 6( A9);

            set J = { ( union A) where A be Subset of ( proj2 ( rng g)) : A is finite };

            

             A16: ( proj2 ( rng g)) c= the topology of Y by A14, FUNCT_5: 11;

            

             A17: J c= the topology of Y

            proof

              let x be object;

              assume x in J;

              then

              consider A be Subset of ( proj2 ( rng g)) such that

               A18: x = ( union A) and A is finite;

              

               A19: A c= the topology of Y by A16;

              then A is Subset-Family of Y by XBOOLE_1: 1;

              hence thesis by A18, A19, PRE_TOPC:def 1;

            end;

            ( {} ( proj2 ( rng g))) in J by ZFMISC_1: 2;

            then

            reconsider J as non empty Subset of ( InclPoset the topology of Y) by A17, YELLOW_1: 1;

            J is directed

            proof

              let a,b be Element of ( InclPoset the topology of Y);

              assume a in J;

              then

              consider A be Subset of ( proj2 ( rng g)) such that

               A20: a = ( union A) and

               A21: A is finite;

              assume b in J;

              then

              consider B be Subset of ( proj2 ( rng g)) such that

               A22: b = ( union B) and

               A23: B is finite;

              reconsider AB = (A \/ B) as finite Subset of ( proj2 ( rng g)) by A21, A23;

              take ab = (a "\/" b);

              

               A24: (a \/ b) = ab by WAYBEL14: 18;

              ( union AB) = (a \/ b) by A20, A22, ZFMISC_1: 78;

              hence ab in J by A24;

              a c= ab & b c= ab by A24, XBOOLE_1: 7;

              hence thesis by YELLOW_1: 3;

            end;

            then

            reconsider J9 = J as non empty directed Subset of S by A1, WAYBEL_0: 3;

            

             A25: ( proj2 ( rng g)) c= ( bool (f . x))

            proof

              let z be object;

              reconsider zz = z as set by TARSKI: 1;

              assume z in ( proj2 ( rng g));

              then

              consider z1 be object such that

               A26: [z1, z] in ( rng g) by XTUPLE_0:def 13;

              

               A27: ( [z1, z] `1 ) = z1;

              reconsider zz1 = z1 as set by TARSKI: 1;

              

               A28: ex a be object st a in ( dom g) & [z1, z] = (g . a) by A26, FUNCT_1:def 3;

              then

               A29: x in zz1 by A14, A15, A27;

              ( [z1, z] `2 ) = z;

              then

               A30: [:zz1, zz:] c= ( *graph f) by A14, A15, A28, A27;

              zz c= (f . x)

              proof

                let a be object;

                assume a in zz;

                then [x, a] in [:zz1, zz:] by A29, ZFMISC_1: 87;

                hence thesis by A30, Th38;

              end;

              hence thesis;

            end;

            ( union J) = (f . y)

            proof

              thus ( union J) c= (f . y)

              proof

                let a be object;

                assume a in ( union J);

                then

                consider u be set such that

                 A31: a in u and

                 A32: u in J by TARSKI:def 4;

                consider A be Subset of ( proj2 ( rng g)) such that

                 A33: u = ( union A) and A is finite by A32;

                A c= ( bool (f . y)) by A25;

                then u c= ( union ( bool (f . y))) by A33, ZFMISC_1: 77;

                then u c= (f . y) by ZFMISC_1: 81;

                hence thesis by A31;

              end;

              let a be object;

              assume

               A34: a in (f . y);

              then

               A35: (g . a) in ( rng g) by A14, FUNCT_1:def 3;

              then (g . a) = [((g . a) `1 ), ((g . a) `2 )] by A14, MCART_1: 21;

              then ((g . a) `2 ) in ( proj2 ( rng g)) by A35, XTUPLE_0:def 13;

              then

              reconsider A = {((g . a) `2 )} as Subset of ( proj2 ( rng g)) by ZFMISC_1: 31;

              ( union A) = ((g . a) `2 ) by ZFMISC_1: 25;

              then

               A36: ((g . a) `2 ) in J;

              a in ((g . a) `2 ) by A15, A34;

              hence thesis by A36, TARSKI:def 4;

            end;

            then ( sup J) = (f . y) by YELLOW_1: 22;

            then

             A37: ( sup J9) = (f . y) by A1, YELLOW_0: 17, YELLOW_0: 26;

            (f . y) in the topology of Y by A5, A1;

            then

            reconsider W = (f . y) as open Subset of Y by PRE_TOPC:def 2;

            

             A38: ( proj1 ( rng g)) c= the topology of X by A14, FUNCT_5: 11;

            defpred P[ object, object] means ex c1,d be set st d = $1 & [c1, $1] = (g . $2) & x in c1 & $2 in d & $2 in (f . x) & [:c1, d:] c= ( *graph f);

            (f . x) in P by A8, FUNCT_2: 38;

            then J meets P by A7, A37, WAYBEL11:def 1;

            then

            consider a be object such that

             A39: a in J and

             A40: a in P by XBOOLE_0: 3;

            reconsider a as Element of S by A40;

            consider A be Subset of ( proj2 ( rng g)) such that

             A41: a = ( union A) and

             A42: A is finite by A39;

             A43:

            now

              let c be object;

              assume c in A;

              then

              consider c1 be object such that

               A44: [c1, c] in ( rng g) by XTUPLE_0:def 13;

              reconsider cc1 = c1 as set by TARSKI: 1;

              consider a be object such that

               A45: a in ( dom g) and

               A46: [c1, c] = (g . a) by A44, FUNCT_1:def 3;

              reconsider cc = c as set by TARSKI: 1;

              reconsider a as object;

              take a;

              thus a in W by A14, A45;

              

               A47: ( [c1, c] `1 ) = c1;

              then

               A48: x in cc1 by A14, A15, A45, A46;

              

               A49: ( [c1, c] `2 ) = c;

              then [:cc1, cc:] c= ( *graph f) by A14, A15, A45, A46, A47;

              hence P[c, a] by A14, A15, A45, A46, A49, A48;

            end;

            consider hh be Function such that

             A50: ( dom hh) = A & ( rng hh) c= W and

             A51: for c be object st c in A holds P[c, (hh . c)] from FUNCT_1:sch 6( A43);

            set B = ( proj1 (g .: ( rng hh)));

            (g .: ( rng hh)) c= ( rng g) by RELAT_1: 111;

            then B c= ( proj1 ( rng g)) by XTUPLE_0: 8;

            then

             A52: B c= the topology of X by A38;

            then

            reconsider B as Subset-Family of X by XBOOLE_1: 1;

            reconsider B as Subset-Family of X;

            reconsider Q = ( Intersect B) as Subset of X;

            take Q;

            (g .: ( rng hh)) is finite by A42, A50, FINSET_1: 5, FINSET_1: 8;

            then B is finite by Th39;

            then Q in ( FinMeetCl the topology of X) by A52, CANTOR_1:def 3;

            then Q in the topology of X by CANTOR_1: 5;

            hence Q is open by PRE_TOPC:def 2;

            thus Q c= (f " P)

            proof

              let z be object;

              assume

               A53: z in Q;

              then

              reconsider zz = z as Element of X;

              reconsider fz = (f . zz), aa = a as Element of ( InclPoset the topology of Y) by A1;

              a c= (f . zz)

              proof

                let p be object;

                assume p in a;

                then

                consider q be set such that

                 A54: p in q and

                 A55: q in A by A41, TARSKI:def 4;

                 P[q, (hh . q)] by A51, A55;

                then

                consider q1,d be set such that

                 A56: d = q and

                 A57: [q1, q] = (g . (hh . q)) and

                 A58: (hh . q) in (f . x) and

                 A59: [:q1, d:] c= ( *graph f);

                (hh . q) in ( rng hh) by A50, A55, FUNCT_1:def 3;

                then [q1, q] in (g .: ( rng hh)) by A14, A57, A58, FUNCT_1:def 6;

                then q1 in B by XTUPLE_0:def 12;

                then zz in q1 by A53, SETFAM_1: 43;

                then [zz, p] in [:q1, q:] by A54, ZFMISC_1: 87;

                hence thesis by A59, Th38, A56;

              end;

              then aa <= fz by YELLOW_1: 3;

              then a <= (f . zz) by A1, YELLOW_0: 1;

              then (f . zz) in P by A7, A40, WAYBEL_0:def 20;

              hence thesis by FUNCT_2: 38;

            end;

            now

              let c1 be set;

              assume c1 in B;

              then

              consider c be object such that

               A60: [c1, c] in (g .: ( rng hh)) by XTUPLE_0:def 12;

              consider b be object such that b in ( dom g) and

               A61: b in ( rng hh) and

               A62: [c1, c] = (g . b) by A60, FUNCT_1:def 6;

              consider c9 be object such that

               A63: c9 in ( dom hh) and

               A64: b = (hh . c9) by A61, FUNCT_1:def 3;

              ex c91,d be set st d = c9 & [c91, c9] = (g . (hh . c9)) & x in c91 & (hh . c9) in d & (hh . c9) in (f . x) & [:c91, d:] c= ( *graph f) by A50, A51, A63;

              hence x in c1 by A62, A64, XTUPLE_0: 1;

            end;

            hence x in Q by A8, SETFAM_1: 43;

          end;

          assume ex Q be Subset of X st Q is open & Q c= (f " P) & x in Q;

          hence x in (f " P);

        end;

        hence (f " P) is open by TOPS_1: 25;

      end;

      ( [#] S) <> {} ;

      hence thesis by A6, TOPS_2: 43;

    end;

    definition

      let W be Relation, X be set;

      :: WAYBEL26:def5

      func (W,X) *graph -> Function means

      : Def5: ( dom it ) = X & for x be object st x in X holds (it . x) = ( Im (W,x));

      existence

      proof

        deffunc F( object) = ( Im (W,$1));

        thus ex f be Function st ( dom f) = X & for x be object st x in X holds (f . x) = F(x) from FUNCT_1:sch 3;

      end;

      correctness

      proof

        let f,g be Function such that

         A1: ( dom f) = X and

         A2: for x be object st x in X holds (f . x) = ( Im (W,x)) and

         A3: ( dom g) = X and

         A4: for x be object st x in X holds (g . x) = ( Im (W,x));

        now

          let x be object;

          assume

           A5: x in X;

          

          hence (f . x) = ( Im (W,x)) by A2

          .= (g . x) by A4, A5;

        end;

        hence thesis by A1, A3, FUNCT_1: 2;

      end;

    end

    theorem :: WAYBEL26:41

    

     Th41: for W be Relation, X be set st ( dom W) c= X holds ( *graph ((W,X) *graph )) = W

    proof

      let W be Relation, X be set such that

       A1: ( dom W) c= X;

      

       A2: ( dom ((W,X) *graph )) = X by Def5;

      now

        let x,y be object;

        hereby

          assume [x, y] in ( *graph ((W,X) *graph ));

          then x in X & y in (((W,X) *graph ) . x) by A2, Th38;

          then y in ( Im (W,x)) by Def5;

          then ex z be object st [z, y] in W & z in {x} by RELAT_1:def 13;

          hence [x, y] in W by TARSKI:def 1;

        end;

        assume

         A3: [x, y] in W;

        then

         A4: x in ( dom W) by XTUPLE_0:def 12;

        x in {x} by TARSKI:def 1;

        then y in ( Im (W,x)) by A3, RELAT_1:def 13;

        then y in (((W,X) *graph ) . x) by A1, A4, Def5;

        hence [x, y] in ( *graph ((W,X) *graph )) by A1, A2, A4, Th38;

      end;

      hence thesis;

    end;

    registration

      let X,Y be TopSpace;

      cluster -> Relation-like for Subset of [:X, Y:];

      coherence

      proof

        let r be Subset of [:X, Y:];

        r is Subset of [:the carrier of X, the carrier of Y:] by BORSUK_1:def 2;

        hence thesis;

      end;

      cluster -> Relation-like for Element of the topology of [:X, Y:];

      coherence ;

    end

    theorem :: WAYBEL26:42

    

     Th42: for X,Y be non empty TopSpace holds for W be open Subset of [:X, Y:] holds for x be Point of X holds ( Im (W,x)) is open Subset of Y

    proof

      let X,Y be non empty TopSpace, W be open Subset of [:X, Y:];

      let x be Point of X;

      reconsider W as Relation of the carrier of X, the carrier of Y by BORSUK_1:def 2;

      reconsider A = (W .: {x}) as Subset of Y;

      now

        let y be set;

        hereby

          assume y in A;

          then

          consider z be object such that

           A1: [z, y] in W and

           A2: z in {x} by RELAT_1:def 13;

          consider AA be Subset-Family of [:X, Y:] such that

           A3: W = ( union AA) and

           A4: for e be set st e in AA holds ex X1 be Subset of X, Y1 be Subset of Y st e = [:X1, Y1:] & X1 is open & Y1 is open by BORSUK_1: 5;

          z = x by A2, TARSKI:def 1;

          then

          consider e be set such that

           A5: [x, y] in e and

           A6: e in AA by A1, A3, TARSKI:def 4;

          consider X1 be Subset of X, Y1 be Subset of Y such that

           A7: e = [:X1, Y1:] and X1 is open and

           A8: Y1 is open by A4, A6;

          take Y1;

          thus Y1 is open by A8;

          

           A9: x in X1 by A5, A7, ZFMISC_1: 87;

          thus Y1 c= A

          proof

            let z be object;

            assume z in Y1;

            then [x, z] in e by A7, A9, ZFMISC_1: 87;

            then

             A10: [x, z] in W by A3, A6, TARSKI:def 4;

            x in {x} by TARSKI:def 1;

            hence thesis by A10, RELAT_1:def 13;

          end;

          thus y in Y1 by A5, A7, ZFMISC_1: 87;

        end;

        thus (ex Q be Subset of Y st Q is open & Q c= A & y in Q) implies y in A;

      end;

      hence thesis by TOPS_1: 25;

    end;

    theorem :: WAYBEL26:43

    

     Th43: for X,Y be non empty TopSpace holds for S be Scott TopAugmentation of ( InclPoset the topology of Y) holds for W be open Subset of [:X, Y:] holds ((W,the carrier of X) *graph ) is continuous Function of X, S

    proof

      let X,Y be non empty TopSpace;

      let S be Scott TopAugmentation of ( InclPoset the topology of Y);

      let W be open Subset of [:X, Y:];

      set f = ((W,the carrier of X) *graph );

      reconsider W as Relation of the carrier of X, the carrier of Y by BORSUK_1:def 2;

      

       A1: ( dom f) = the carrier of X by Def5;

      

       A2: the carrier of ( InclPoset the topology of Y) = the topology of Y & the RelStr of S = the RelStr of ( InclPoset the topology of Y) by YELLOW_1: 1, YELLOW_9:def 4;

      ( rng f) c= the carrier of S

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A3: x in ( dom f) and

         A4: y = (f . x) by FUNCT_1:def 3;

        reconsider x as Element of X by A3, Def5;

        y = ( Im (W,x)) by A4, Def5;

        then y is open Subset of Y by Th42;

        hence thesis by A2, PRE_TOPC:def 2;

      end;

      then

      reconsider f as Function of X, S by A1, FUNCT_2: 2;

      ( dom W) c= the carrier of X;

      then ( *graph f) = W by Th41;

      hence thesis by Th40;

    end;

    theorem :: WAYBEL26:44

    

     Th44: for X,Y be non empty TopSpace holds for S be Scott TopAugmentation of ( InclPoset the topology of Y) holds for W1,W2 be open Subset of [:X, Y:] st W1 c= W2 holds for f1,f2 be Element of ( oContMaps (X,S)) st f1 = ((W1,the carrier of X) *graph ) & f2 = ((W2,the carrier of X) *graph ) holds f1 <= f2

    proof

      let X,Y be non empty TopSpace;

      let S be Scott TopAugmentation of ( InclPoset the topology of Y);

      let W1,W2 be open Subset of [:X, Y:] such that

       A1: W1 c= W2;

      let f1,f2 be Element of ( oContMaps (X,S)) such that

       A2: f1 = ((W1,the carrier of X) *graph ) & f2 = ((W2,the carrier of X) *graph );

      reconsider g1 = f1, g2 = f2 as continuous Function of X, ( Omega S) by Th1;

      S is TopAugmentation of S by YELLOW_9: 44;

      then

       A3: the RelStr of S = the RelStr of ( Omega S) by WAYBEL25: 16;

      

       A4: the RelStr of S = the RelStr of ( InclPoset the topology of Y) by YELLOW_9:def 4;

      now

        let j be set;

        assume j in the carrier of X;

        then

        reconsider x = j as Element of X;

        reconsider g1x = (g1 . x), g2x = (g2 . x) as Element of ( InclPoset the topology of Y) by A3, YELLOW_9:def 4;

        take a = (g1 . x), b = (g2 . x);

        thus a = (g1 . j) & b = (g2 . j);

        (g1 . x) = ( Im (W1,x)) & (g2 . x) = ( Im (W2,x)) by A2, Def5;

        then (g1 . x) c= (g2 . x) by A1, RELAT_1: 124;

        then g1x <= g2x by YELLOW_1: 3;

        hence a <= b by A4, A3, YELLOW_0: 1;

      end;

      then g1 <= g2;

      hence thesis by Th3;

    end;

    theorem :: WAYBEL26:45

    for X,Y be non empty TopSpace holds for S be Scott TopAugmentation of ( InclPoset the topology of Y) holds ex F be Function of ( InclPoset the topology of [:X, Y:]), ( oContMaps (X,S)) st F is monotone & for W be open Subset of [:X, Y:] holds (F . W) = ((W,the carrier of X) *graph )

    proof

      let X,Y be non empty TopSpace;

      let S be Scott TopAugmentation of ( InclPoset the topology of Y);

      deffunc F( Element of the topology of [:X, Y:]) = (($1,the carrier of X) *graph );

      consider F be ManySortedSet of the topology of [:X, Y:] such that

       A1: for R be Element of the topology of [:X, Y:] holds (F . R) = F(R) from PBOOLE:sch 5;

      

       A2: ( rng F) c= the carrier of ( oContMaps (X,S))

      proof

        let y be object;

        assume y in ( rng F);

        then

        consider x be object such that

         A3: x in ( dom F) and

         A4: y = (F . x) by FUNCT_1:def 3;

        reconsider x as Element of the topology of [:X, Y:] by A3;

        

         A5: x is open Subset of [:X, Y:] by PRE_TOPC:def 2;

        y = ((x,the carrier of X) *graph ) by A1, A4;

        then y is continuous Function of X, S by A5, Th43;

        then y is Element of ( oContMaps (X,S)) by Th2;

        hence thesis;

      end;

      

       A6: ( dom F) = the topology of [:X, Y:] by PARTFUN1:def 2;

      

       A7: the carrier of ( InclPoset the topology of [:X, Y:]) = the topology of [:X, Y:] by YELLOW_1: 1;

      then

      reconsider F as Function of ( InclPoset the topology of [:X, Y:]), ( oContMaps (X,S)) by A6, A2, FUNCT_2: 2;

      take F;

      thus F is monotone

      proof

        let x,y be Element of ( InclPoset the topology of [:X, Y:]);

        x in the topology of [:X, Y:] & y in the topology of [:X, Y:] by A7;

        then

        reconsider W1 = x, W2 = y as open Subset of [:X, Y:] by PRE_TOPC:def 2;

        assume x <= y;

        then

         A8: W1 c= W2 by YELLOW_1: 3;

        (F . x) = ((W1,the carrier of X) *graph ) & (F . y) = ((W2,the carrier of X) *graph ) by A1, A7;

        hence thesis by A8, Th44;

      end;

      let W be open Subset of [:X, Y:];

      W in the topology of [:X, Y:] by PRE_TOPC:def 2;

      hence thesis by A1;

    end;