waybel27.miz



    begin

    definition

      let F be Function;

      :: WAYBEL27:def1

      attr F is uncurrying means

      : Def1: (for x be set st x in ( dom F) holds x is Function-yielding Function) & for f be Function st f in ( dom F) holds (F . f) = ( uncurry f);

      :: WAYBEL27:def2

      attr F is currying means

      : Def2: (for x be set st x in ( dom F) holds x is Function & ( proj1 x) is Relation) & for f be Function st f in ( dom F) holds (F . f) = ( curry f);

      :: WAYBEL27:def3

      attr F is commuting means

      : Def3: (for x be set st x in ( dom F) holds x is Function-yielding Function) & for f be Function st f in ( dom F) holds (F . f) = ( commute f);

    end

    registration

      cluster empty -> uncurrying currying commuting for Function;

      coherence ;

    end

    registration

      cluster uncurrying currying commuting for Function;

      existence

      proof

        reconsider F = {} as Function;

        take F;

        thus thesis;

      end;

    end

    registration

      let F be uncurrying Function, X be set;

      cluster (F | X) -> uncurrying;

      coherence

      proof

        

         A1: for f be Function st f in ( dom (F | X)) holds ((F | X) . f) = ( uncurry f)

        proof

          let f be Function;

          assume

           A2: f in ( dom (F | X));

          then

           A3: f in ( dom F) by RELAT_1: 57;

          

          thus ((F | X) . f) = (F . f) by A2, FUNCT_1: 47

          .= ( uncurry f) by A3, Def1;

        end;

        for x be set st x in ( dom (F | X)) holds x is Function-yielding Function

        proof

          let x be set;

          assume x in ( dom (F | X));

          then x in ( dom F) by RELAT_1: 57;

          hence thesis by Def1;

        end;

        hence thesis by A1;

      end;

    end

    registration

      let F be currying Function, X be set;

      cluster (F | X) -> currying;

      coherence

      proof

        

         A1: for f be Function st f in ( dom (F | X)) holds ((F | X) . f) = ( curry f)

        proof

          let f be Function;

          assume

           A2: f in ( dom (F | X));

          then

           A3: f in ( dom F) by RELAT_1: 57;

          

          thus ((F | X) . f) = (F . f) by A2, FUNCT_1: 47

          .= ( curry f) by A3, Def2;

        end;

        for x be set st x in ( dom (F | X)) holds x is Function & ( proj1 x) is Relation

        proof

          let x be set;

          assume x in ( dom (F | X));

          then x in ( dom F) by RELAT_1: 57;

          hence thesis by Def2;

        end;

        hence thesis by A1;

      end;

    end

    theorem :: WAYBEL27:1

    

     Th1: for X,Y,Z,D be set st D c= ( Funcs (X,( Funcs (Y,Z)))) holds ex F be ManySortedSet of D st F is uncurrying & ( rng F) c= ( Funcs ( [:X, Y:],Z))

    proof

      let X,Y,Z,D be set such that

       A1: D c= ( Funcs (X,( Funcs (Y,Z))));

      per cases ;

        suppose D is empty;

        then

        reconsider F = {} as ManySortedSet of D by PARTFUN1:def 2, RELAT_1: 38, RELAT_1:def 18;

        take F;

        thus F is uncurrying;

        thus thesis;

      end;

        suppose D is non empty;

        then

        reconsider E = D as non empty functional set by A1;

        deffunc F( Function) = ( uncurry $1);

        consider F be ManySortedSet of E such that

         A2: for d be Element of E holds (F . d) = F(d) from PBOOLE:sch 5;

        reconsider F1 = F as ManySortedSet of D;

        take F1;

        thus F1 is uncurrying

        proof

          hereby

            let x be set;

            assume x in ( dom F1);

            then x in D;

            then

            consider x1 be Function such that

             A3: x1 = x and ( dom x1) = X and

             A4: ( rng x1) c= ( Funcs (Y,Z)) by A1, FUNCT_2:def 2;

            x1 is Function-yielding

            proof

              let a be object;

              assume a in ( dom x1);

              then (x1 . a) in ( rng x1) by FUNCT_1:def 3;

              hence thesis by A4;

            end;

            hence x is Function-yielding Function by A3;

          end;

          let f be Function;

          assume f in ( dom F1);

          then

          reconsider d = f as Element of E;

          

          thus (F1 . f) = (F . d)

          .= ( uncurry f) by A2;

        end;

        thus ( rng F1) c= ( Funcs ( [:X, Y:],Z))

        proof

          let y be object;

          assume y in ( rng F1);

          then

          consider x be object such that

           A5: x in ( dom F1) and

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

          reconsider d = x as Element of E by A5;

          

           A7: d in ( Funcs (X,( Funcs (Y,Z)))) by A1;

          y = ( uncurry d) by A2, A6;

          hence thesis by A7, FUNCT_6: 11;

        end;

      end;

    end;

    theorem :: WAYBEL27:2

    

     Th2: for X,Y,Z,D be set st D c= ( Funcs ( [:X, Y:],Z)) holds ex F be ManySortedSet of D st F is currying & ((Y = {} implies X = {} ) implies ( rng F) c= ( Funcs (X,( Funcs (Y,Z)))))

    proof

      let X,Y,Z,D be set;

      assume

       A1: D c= ( Funcs ( [:X, Y:],Z));

      per cases ;

        suppose D is empty;

        then

        reconsider F = {} as ManySortedSet of D by PARTFUN1:def 2, RELAT_1: 38, RELAT_1:def 18;

        take F;

        thus F is currying;

        assume Y = {} implies X = {} ;

        thus thesis;

      end;

        suppose D is non empty;

        then

        reconsider E = D as non empty functional set by A1;

        deffunc F( Function) = ( curry $1);

        consider F be ManySortedSet of E such that

         A2: for d be Element of E holds (F . d) = F(d) from PBOOLE:sch 5;

        reconsider F1 = F as ManySortedSet of D;

        take F1;

        thus F1 is currying

        proof

          hereby

            let x be set;

            assume x in ( dom F1);

            then

             A3: x in D;

            hence x is Function by A1;

            ex x1 be Function st x1 = x & ( dom x1) = [:X, Y:] & ( rng x1) c= Z by A3, A1, FUNCT_2:def 2;

            hence ( proj1 x) is Relation;

          end;

          let f be Function;

          assume f in ( dom F1);

          then

          reconsider d = f as Element of E;

          

          thus (F1 . f) = (F . d)

          .= ( curry f) by A2;

        end;

        assume

         A4: Y = {} implies X = {} ;

        thus ( rng F1) c= ( Funcs (X,( Funcs (Y,Z))))

        proof

          let y be object;

          assume y in ( rng F1);

          then

          consider x be object such that

           A5: x in ( dom F1) and

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

          reconsider d = x as Element of E by A5;

          

           A7: y = ( curry d) by A2, A6;

          

           A8: d in ( Funcs ( [:X, Y:],Z)) by A1;

          per cases ;

            suppose

             A9: [:X, Y:] = {} ;

            then

             A10: d is Function of {} , Z by A8, FUNCT_2: 66;

            now

              assume

               A11: X = {} ;

              then y is Function of X, ( Funcs (Y,Z)) by A7, A10, FUNCT_5: 42, RELSET_1: 12;

              hence thesis by A11, FUNCT_2: 8;

            end;

            hence thesis by A4, A9;

          end;

            suppose [:X, Y:] <> {} ;

            hence thesis by A7, A8, FUNCT_6: 10;

          end;

        end;

      end;

    end;

    registration

      let X,Y,Z be set;

      cluster uncurrying for ManySortedSet of ( Funcs (X,( Funcs (Y,Z))));

      existence

      proof

        ex F be ManySortedSet of ( Funcs (X,( Funcs (Y,Z)))) st F is uncurrying & ( rng F) c= ( Funcs ( [:X, Y:],Z)) by Th1;

        hence thesis;

      end;

      cluster currying for ManySortedSet of ( Funcs ( [:X, Y:],Z));

      existence

      proof

        ex F be ManySortedSet of ( Funcs ( [:X, Y:],Z)) st F is currying & ((Y = {} implies X = {} ) implies ( rng F) c= ( Funcs (X,( Funcs (Y,Z))))) by Th2;

        hence thesis;

      end;

    end

    theorem :: WAYBEL27:3

    

     Th3: for A,B be non empty set, C be set holds for f,g be commuting Function st ( dom f) c= ( Funcs (A,( Funcs (B,C)))) & ( rng f) c= ( dom g) holds (g * f) = ( id ( dom f))

    proof

      let A,B be non empty set;

      let C be set;

      let f,g be commuting Function;

      assume that

       A1: ( dom f) c= ( Funcs (A,( Funcs (B,C)))) and

       A2: ( rng f) c= ( dom g);

       A3:

      now

        let x be object;

        assume

         A4: x in ( dom f);

        then

        reconsider X = x as Function by Def3;

        

         A5: (f . x) in ( rng f) by A4, FUNCT_1:def 3;

        then

        reconsider Y = (f . x) as Function by A2, Def3;

        

        thus ((g * f) . x) = (g . (f . x)) by A4, FUNCT_1: 13

        .= ( commute Y) by A2, A5, Def3

        .= ( commute ( commute X)) by A4, Def3

        .= x by A1, A4, FUNCT_6: 57;

      end;

      ( dom (g * f)) = ( dom f) by A2, RELAT_1: 27;

      hence thesis by A3, FUNCT_1: 17;

    end;

    theorem :: WAYBEL27:4

    

     Th4: for B be non empty set, A,C be set holds for f be uncurrying Function holds for g be currying Function st ( dom f) c= ( Funcs (A,( Funcs (B,C)))) & ( rng f) c= ( dom g) holds (g * f) = ( id ( dom f))

    proof

      let B be non empty set;

      let A,C be set;

      let f be uncurrying Function;

      let g be currying Function;

      assume that

       A1: ( dom f) c= ( Funcs (A,( Funcs (B,C)))) and

       A2: ( rng f) c= ( dom g);

       A3:

      now

        let x be object;

        assume

         A4: x in ( dom f);

        then

        reconsider X = x as Function by Def1;

        

         A5: ex F be Function st X = F & ( dom F) = A & ( rng F) c= ( Funcs (B,C)) by A1, A4, FUNCT_2:def 2;

        

         A6: (f . x) in ( rng f) by A4, FUNCT_1:def 3;

        then

        reconsider Y = (f . x) as Function by A2, Def2;

        

        thus ((g * f) . x) = (g . (f . x)) by A4, FUNCT_1: 13

        .= ( curry Y) by A2, A6, Def2

        .= ( curry ( uncurry X)) by A4, Def1

        .= x by A5, FUNCT_5: 48;

      end;

      ( dom (g * f)) = ( dom f) by A2, RELAT_1: 27;

      hence thesis by A3, FUNCT_1: 17;

    end;

    theorem :: WAYBEL27:5

    

     Th5: for A,B,C be set holds for f be currying Function holds for g be uncurrying Function st ( dom f) c= ( Funcs ( [:A, B:],C)) & ( rng f) c= ( dom g) holds (g * f) = ( id ( dom f))

    proof

      let A,B,C be set;

      let f be currying Function;

      let g be uncurrying Function;

      assume that

       A1: ( dom f) c= ( Funcs ( [:A, B:],C)) and

       A2: ( rng f) c= ( dom g);

       A3:

      now

        let x be object;

        assume

         A4: x in ( dom f);

        then

        reconsider X = x as Function by Def2;

        

         A5: ex F be Function st X = F & ( dom F) = [:A, B:] & ( rng F) c= C by A1, A4, FUNCT_2:def 2;

        

         A6: (f . x) in ( rng f) by A4, FUNCT_1:def 3;

        then

        reconsider Y = (f . x) as Function by A2, Def1;

        

        thus ((g * f) . x) = (g . (f . x)) by A4, FUNCT_1: 13

        .= ( uncurry Y) by A2, A6, Def1

        .= ( uncurry ( curry X)) by A4, Def2

        .= x by A5, FUNCT_5: 49;

      end;

      ( dom (g * f)) = ( dom f) by A2, RELAT_1: 27;

      hence thesis by A3, FUNCT_1: 17;

    end;

    theorem :: WAYBEL27:6

    

     Th6: for f be Function-yielding Function holds for i,A be set st i in ( dom ( commute f)) holds ((( commute f) . i) .: A) c= ( pi ((f .: A),i))

    proof

      let f be Function-yielding Function;

      let i,A be set;

      

       A1: ( commute f) = ( curry' ( uncurry f)) by FUNCT_6:def 10

      .= ( curry ( ~ ( uncurry f))) by FUNCT_5:def 3;

      assume

       A2: i in ( dom ( commute f));

      thus ((( commute f) . i) .: A) c= ( pi ((f .: A),i))

      proof

        let x be object;

        assume x in ((( commute f) . i) .: A);

        then

        consider y be object such that

         A3: y in ( dom (( commute f) . i)) and

         A4: y in A and

         A5: x = ((( commute f) . i) . y) by FUNCT_1:def 6;

        

         A6: [i, y] in ( dom ( ~ ( uncurry f))) by A2, A1, A3, FUNCT_5: 31;

        then

         A7: [y, i] in ( dom ( uncurry f)) by FUNCT_4: 42;

        then ex a be object, g be Function, b be object st [y, i] = [a, b] & a in ( dom f) & g = (f . a) & b in ( dom g) by FUNCT_5:def 2;

        then y in ( dom f) by XTUPLE_0: 1;

        then

         A8: (f . y) in (f .: A) by A4, FUNCT_1:def 6;

        

         A9: ( [y, i] `2 ) = i;

        

         A10: ( [y, i] `1 ) = y;

        x = (( ~ ( uncurry f)) . (i,y)) by A2, A1, A3, A5, FUNCT_5: 31

        .= (( uncurry f) . (y,i)) by A6, FUNCT_4: 43

        .= ((f . y) qua Function . i) by A7, A10, A9, FUNCT_5:def 2;

        hence thesis by A8, CARD_3:def 6;

      end;

    end;

    theorem :: WAYBEL27:7

    

     Th7: for f be Function-yielding Function holds for i,A be set st for g be Function st g in (f .: A) holds i in ( dom g) holds ( pi ((f .: A),i)) c= ((( commute f) . i) .: A)

    proof

      let f be Function-yielding Function;

      let i,A be set;

      assume

       A1: for g be Function st g in (f .: A) holds i in ( dom g);

      let x be object;

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

      then

      consider g be Function such that

       A2: g in (f .: A) and

       A3: x = (g . i) by CARD_3:def 6;

      consider y be object such that

       A4: y in ( dom f) and

       A5: y in A and

       A6: g = (f . y) by A2, FUNCT_1:def 6;

      i in ( dom g) by A1, A2;

      then

       A7: [y, i] in ( dom ( uncurry f)) by A4, A6, FUNCT_5:def 2;

      then

       A8: [i, y] in ( dom ( ~ ( uncurry f))) by FUNCT_4:def 2;

      then

       A9: i in ( proj1 ( dom ( ~ ( uncurry f)))) by XTUPLE_0:def 12;

      then

       A10: i in ( dom ( curry ( ~ ( uncurry f)))) by FUNCT_5:def 1;

      

       A11: i in {i} by TARSKI:def 1;

      y in ( proj2 ( dom ( ~ ( uncurry f)))) by A8, XTUPLE_0:def 13;

      then [i, y] in [: {i}, ( proj2 ( dom ( ~ ( uncurry f)))):] by A11, ZFMISC_1: 87;

      then

       A12: [i, y] in (( dom ( ~ ( uncurry f))) /\ [: {i}, ( proj2 ( dom ( ~ ( uncurry f)))):]) by A8, XBOOLE_0:def 4;

      then

       A13: y in ( proj2 (( dom ( ~ ( uncurry f))) /\ [: {i}, ( proj2 ( dom ( ~ ( uncurry f)))):])) by XTUPLE_0:def 13;

      

       A14: ( [y, i] `2 ) = i;

      

       A15: ( [y, i] `1 ) = y;

      

       A16: ( commute f) = ( curry' ( uncurry f)) by FUNCT_6:def 10

      .= ( curry ( ~ ( uncurry f))) by FUNCT_5:def 3;

      

       A17: ex h be Function st (( curry ( ~ ( uncurry f))) . i) = h & ( dom h) = ( proj2 (( dom ( ~ ( uncurry f))) /\ [: {i}, ( proj2 ( dom ( ~ ( uncurry f)))):])) & for b be object st b in ( dom h) holds (h . b) = (( ~ ( uncurry f)) . (i,b)) by A9, FUNCT_5:def 1;

      then y in ( dom (( commute f) . i)) by A16, A12, XTUPLE_0:def 13;

      

      then ((( commute f) . i) . y) = (( ~ ( uncurry f)) . (i,y)) by A16, A10, FUNCT_5: 31

      .= (( uncurry f) . (y,i)) by A7, FUNCT_4:def 2

      .= x by A3, A6, A7, A15, A14, FUNCT_5:def 2;

      hence thesis by A5, A16, A17, A13, FUNCT_1:def 6;

    end;

    theorem :: WAYBEL27:8

    

     Th8: for X,Y be set, f be Function st ( rng f) c= ( Funcs (X,Y)) holds for i,A be set st i in X holds ((( commute f) . i) .: A) = ( pi ((f .: A),i))

    proof

      let X,Y be set, f be Function;

      assume

       A1: ( rng f) c= ( Funcs (X,Y));

      then

       A2: f in ( Funcs (( dom f),( Funcs (X,Y)))) by FUNCT_2:def 2;

      

       A3: f is Function-yielding

      proof

        let x be object;

        assume x in ( dom f);

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

        hence thesis by A1;

      end;

      let i,A be set;

      assume

       A4: i in X;

      per cases ;

        suppose ( dom f) = {} ;

        then

         A5: f = {} ;

        then (( commute f) . i) = {} by FUNCT_6: 58;

        then

         A6: ((( commute f) . i) .: A) = {} ;

        (f .: A) = {} by A5;

        hence thesis by A6, CARD_3: 13;

      end;

        suppose ( dom f) <> {} ;

        then ( commute f) in ( Funcs (X,( Funcs (( dom f),Y)))) by A2, A4, FUNCT_6: 55;

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

        hence ((( commute f) . i) .: A) c= ( pi ((f .: A),i)) by A3, A4, Th6;

        now

          let g be Function;

          

           A7: (f .: A) c= ( rng f) by RELAT_1: 111;

          assume g in (f .: A);

          then g in ( rng f) by A7;

          then ex h be Function st g = h & ( dom h) = X & ( rng h) c= Y by A1, FUNCT_2:def 2;

          hence i in ( dom g) by A4;

        end;

        hence thesis by A3, Th7;

      end;

    end;

    theorem :: WAYBEL27:9

    

     Th9: for f be Function holds for i,A be set st [:A, {i}:] c= ( dom f) holds ( pi ((( curry f) .: A),i)) = (f .: [:A, {i}:])

    proof

      let f be Function, i,A be set such that

       A1: [:A, {i}:] c= ( dom f);

      

       A2: i in {i} by TARSKI:def 1;

      thus ( pi ((( curry f) .: A),i)) c= (f .: [:A, {i}:])

      proof

        let x be object;

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

        then

        consider g be Function such that

         A3: g in (( curry f) .: A) and

         A4: x = (g . i) by CARD_3:def 6;

        consider a be object such that a in ( dom ( curry f)) and

         A5: a in A and

         A6: g = (( curry f) . a) by A3, FUNCT_1:def 6;

        

         A7: [a, i] in [:A, {i}:] by A2, A5, ZFMISC_1:def 2;

        then (f . (a,i)) in (f .: [:A, {i}:]) by A1, FUNCT_1:def 6;

        hence thesis by A1, A4, A6, A7, FUNCT_5: 20;

      end;

      let x be object;

      assume x in (f .: [:A, {i}:]);

      then

      consider y be object such that

       A8: y in ( dom f) and

       A9: y in [:A, {i}:] and

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

      consider y1,y2 be object such that

       A11: y1 in A and

       A12: y2 in {i} and

       A13: y = [y1, y2] by A9, ZFMISC_1:def 2;

      reconsider g = (( curry f) . y1) as Function;

      y1 in ( dom ( curry f)) by A8, A13, FUNCT_5: 19;

      then

       A14: g in (( curry f) .: A) by A11, FUNCT_1:def 6;

      

       A15: y2 = i by A12, TARSKI:def 1;

      x = (f . (y1,y2)) by A10, A13;

      then x = (g . i) by A15, A8, A13, FUNCT_5: 20;

      hence thesis by A14, CARD_3:def 6;

    end;

    registration

      let T be constituted-Functions 1-sorted;

      cluster the carrier of T -> functional;

      coherence ;

    end

    registration

      cluster constituted-Functions complete strict for LATTICE;

      existence

      proof

        set L = the complete LATTICE;

        take (L |^ {} );

        thus thesis;

      end;

      cluster constituted-Functions non empty for 1-sorted;

      existence

      proof

        set L = the complete LATTICE;

        take (L |^ {} );

        thus thesis;

      end;

    end

    registration

      let T be constituted-Functions non empty RelStr;

      cluster -> constituted-Functions for non empty SubRelStr of T;

      coherence

      proof

        let S be non empty SubRelStr of T;

        let a be Element of S;

        the carrier of S c= the carrier of T by YELLOW_0:def 13;

        hence thesis;

      end;

    end

    theorem :: WAYBEL27:10

    

     Th10: for S,T be complete LATTICE holds for f be idempotent Function of T, T holds for h be Function of S, ( Image f) holds (f * h) = h

    proof

      let S,T be complete LATTICE;

      let f be idempotent Function of T, T;

      let h be Function of S, ( Image f);

      ( rng h) c= the carrier of ( Image f);

      then

       A1: ( rng h) c= ( rng f) by YELLOW_0:def 15;

      (f * f) = f by QUANTAL1:def 9;

      then ( rng f) c= ( dom f) by FUNCT_1: 15;

      then ( rng h) c= ( dom f) by A1;

      hence thesis by A1, YELLOW16: 4;

    end;

    theorem :: WAYBEL27:11

    for S be non empty RelStr holds for T,T1 be non empty RelStr st T is SubRelStr of T1 holds for f be Function of S, T holds for f1 be Function of S, T1 holds f is monotone & f = f1 implies f1 is monotone

    proof

      let S be non empty RelStr;

      let T,T1 be non empty RelStr;

      assume

       A1: T is SubRelStr of T1;

      let f be Function of S, T;

      let f1 be Function of S, T1;

      assume that

       A2: f is monotone and

       A3: f = f1;

      thus f1 is monotone

      proof

        let x,y be Element of S;

        assume x <= y;

        then (f . x) <= (f . y) by A2;

        hence thesis by A1, A3, YELLOW_0: 59;

      end;

    end;

    theorem :: WAYBEL27:12

    

     Th12: for S be non empty RelStr holds for T,T1 be non empty RelStr st T is full SubRelStr of T1 holds for f be Function of S, T holds for f1 be Function of S, T1 holds f1 is monotone & f = f1 implies f is monotone

    proof

      let S be non empty RelStr;

      let T,T1 be non empty RelStr;

      assume

       A1: T is full SubRelStr of T1;

      let f be Function of S, T;

      let f1 be Function of S, T1;

      assume that

       A2: f1 is monotone and

       A3: f = f1;

      thus f is monotone

      proof

        let x,y be Element of S;

        assume x <= y;

        then (f1 . x) <= (f1 . y) by A2;

        hence thesis by A1, A3, YELLOW_0: 60;

      end;

    end;

    theorem :: WAYBEL27:13

    

     Th13: for X be set, V be Subset of X holds (( chi (V,X)) " {1}) = V & (( chi (V,X)) " { 0 }) = (X \ V)

    proof

      let X be set;

      let V be Subset of X;

      thus (( chi (V,X)) " {1}) = V

      proof

        thus (( chi (V,X)) " {1}) c= V

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume

           A1: x in (( chi (V,X)) " {1});

          then (( chi (V,X)) . x) in {1} by FUNCT_1:def 7;

          then (( chi (V,X)) . xx) = { 0 } by TARSKI:def 1, CARD_1: 49;

          then (( chi (V,X)) . xx) <> {} ;

          hence thesis by A1, FUNCT_3:def 3;

        end;

        let x be object;

        assume

         A2: x in V;

        then (( chi (V,X)) . x) = 1 by FUNCT_3:def 3;

        then

         A3: (( chi (V,X)) . x) in {1} by TARSKI:def 1;

        x in X by A2;

        then x in ( dom ( chi (V,X))) by FUNCT_3:def 3;

        hence thesis by A3, FUNCT_1:def 7;

      end;

      thus (( chi (V,X)) " { 0 }) = (X \ V)

      proof

        thus (( chi (V,X)) " { 0 }) c= (X \ V)

        proof

          let x be object;

          

           A4: x in V implies (( chi (V,X)) . x) = 1 by FUNCT_3:def 3;

          assume

           A5: x in (( chi (V,X)) " { 0 });

          then (( chi (V,X)) . x) in { 0 } by FUNCT_1:def 7;

          hence thesis by A4, A5, TARSKI:def 1, XBOOLE_0:def 5;

        end;

        let x be object;

        assume

         A6: x in (X \ V);

        then not x in V by XBOOLE_0:def 5;

        then (( chi (V,X)) . x) = 0 by A6, FUNCT_3:def 3;

        then

         A7: (( chi (V,X)) . x) in { 0 } by TARSKI:def 1;

        x in X by A6;

        then x in ( dom ( chi (V,X))) by FUNCT_3:def 3;

        hence thesis by A7, FUNCT_1:def 7;

      end;

    end;

    begin

    definition

      let X be non empty set;

      let T be non empty RelStr;

      let f be Element of (T |^ X);

      let x be Element of X;

      :: original: .

      redefine

      func f . x -> Element of T ;

      coherence

      proof

        reconsider p = f as Element of ( product (X --> T)) by YELLOW_1:def 5;

        (p . x) is Element of ((X --> T) . x);

        hence thesis;

      end;

    end

    theorem :: WAYBEL27:14

    

     Th14: for X be non empty set, T be non empty RelStr holds for f,g be Element of (T |^ X) holds f <= g iff for x be Element of X holds (f . x) <= (g . x)

    proof

      let X be non empty set, T be non empty RelStr;

      let f,g be Element of (T |^ X);

      reconsider a = f, b = g as Element of ( product (X --> T)) by YELLOW_1:def 5;

      

       A1: (T |^ X) = ( product (X --> T)) by YELLOW_1:def 5;

      hereby

        assume

         A2: f <= g;

        let x be Element of X;

        ((X --> T) . x) = T;

        hence (f . x) <= (g . x) by A1, A2, WAYBEL_3: 28;

      end;

      assume for x be Element of X holds (f . x) <= (g . x);

      then for x be Element of X holds (a . x) <= (b . x);

      hence thesis by A1, WAYBEL_3: 28;

    end;

    theorem :: WAYBEL27:15

    

     Th15: for X be set holds for L,S be non empty RelStr st the RelStr of L = the RelStr of S holds (L |^ X) = (S |^ X)

    proof

      let X be set;

      let L,S be non empty RelStr such that

       A1: the RelStr of L = the RelStr of S;

      reconsider tXL = (X --> L) as RelStr-yielding ManySortedSet of X;

      reconsider tXS = (X --> S) as RelStr-yielding ManySortedSet of X;

      

       A2: for x be object st x in ( dom ( Carrier tXS)) holds (( Carrier tXS) . x) = (( Carrier tXL) . x)

      proof

        let x be object;

        assume x in ( dom ( Carrier tXS));

        then

         A3: x in X;

        then

         A4: ex R1 be 1-sorted st (tXL . x) = R1 & (( Carrier tXL) . x) = the carrier of R1 by PRALG_1:def 15;

        ex R be 1-sorted st (tXS . x) = R & (( Carrier tXS) . x) = the carrier of R by A3, PRALG_1:def 15;

        

        hence (( Carrier tXS) . x) = the carrier of S by A3, FUNCOP_1: 7

        .= (( Carrier tXL) . x) by A1, A3, A4, FUNCOP_1: 7;

      end;

      

       A5: ( dom ( Carrier tXS)) = X by PARTFUN1:def 2

      .= ( dom ( Carrier tXL)) by PARTFUN1:def 2;

      

       A6: the carrier of (S |^ X) = the carrier of ( product tXS) by YELLOW_1:def 5

      .= ( product ( Carrier tXS)) by YELLOW_1:def 4

      .= ( product ( Carrier tXL)) by A5, A2, FUNCT_1: 2

      .= the carrier of ( product tXL) by YELLOW_1:def 4

      .= the carrier of (L |^ X) by YELLOW_1:def 5;

      

       A7: the InternalRel of (L |^ X) c= the InternalRel of (S |^ X)

      proof

        reconsider tXS = (X --> S) as RelStr-yielding ManySortedSet of X;

        reconsider tXL = (X --> L) as RelStr-yielding ManySortedSet of X;

        let x be object;

        assume

         A8: x in the InternalRel of (L |^ X);

        then

        consider a,b be object such that

         A9: x = [a, b] and

         A10: a in the carrier of (L |^ X) and

         A11: b in the carrier of (L |^ X) by RELSET_1: 2;

        reconsider a, b as Element of (L |^ X) by A10, A11;

        

         A12: (L |^ X) = ( product tXL) by YELLOW_1:def 5;

        then

         A13: the carrier of (L |^ X) = ( product ( Carrier tXL)) by YELLOW_1:def 4;

        a <= b by A8, A9, ORDERS_2:def 5;

        then

        consider f,g be Function such that

         A14: f = a and

         A15: g = b and

         A16: for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = (tXL . i) & xi = (f . i) & yi = (g . i) & xi <= yi by A12, A13, YELLOW_1:def 4;

        reconsider a1 = a, b1 = b as Element of (S |^ X) by A6;

        

         A17: ex f,g be Function st f = a1 & g = b1 & for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = (tXS . i) & xi = (f . i) & yi = (g . i) & xi <= yi

        proof

          take f, g;

          thus f = a1 & g = b1 by A14, A15;

          let i be object;

          assume

           A18: i in X;

          then

          consider R be RelStr, xi,yi be Element of R such that

           A19: R = (tXL . i) and

           A20: xi = (f . i) and

           A21: yi = (g . i) and

           A22: xi <= yi by A16;

          take R1 = S;

          reconsider xi1 = xi, yi1 = yi as Element of R1 by A1, A18, A19, FUNCOP_1: 7;

          take xi1, yi1;

          thus R1 = (tXS . i) by A18, FUNCOP_1: 7;

          thus xi1 = (f . i) & yi1 = (g . i) by A20, A21;

          the InternalRel of R = the InternalRel of L by A18, A19, FUNCOP_1: 7;

          then [xi1, yi1] in the InternalRel of R1 by A1, A22, ORDERS_2:def 5;

          hence thesis by ORDERS_2:def 5;

        end;

        

         A23: (S |^ X) = ( product tXS) by YELLOW_1:def 5;

        then the carrier of (S |^ X) = ( product ( Carrier tXS)) by YELLOW_1:def 4;

        then a1 <= b1 by A17, A23, YELLOW_1:def 4;

        hence thesis by A9, ORDERS_2:def 5;

      end;

      the InternalRel of (S |^ X) c= the InternalRel of (L |^ X)

      proof

        reconsider tXL = (X --> L) as RelStr-yielding ManySortedSet of X;

        reconsider tXS = (X --> S) as RelStr-yielding ManySortedSet of X;

        let x be object;

        assume

         A24: x in the InternalRel of (S |^ X);

        then

        consider a,b be object such that

         A25: x = [a, b] and

         A26: a in the carrier of (S |^ X) and

         A27: b in the carrier of (S |^ X) by RELSET_1: 2;

        reconsider a, b as Element of (S |^ X) by A26, A27;

        

         A28: (S |^ X) = ( product tXS) by YELLOW_1:def 5;

        then

         A29: the carrier of (S |^ X) = ( product ( Carrier tXS)) by YELLOW_1:def 4;

        a <= b by A24, A25, ORDERS_2:def 5;

        then

        consider f,g be Function such that

         A30: f = a and

         A31: g = b and

         A32: for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = (tXS . i) & xi = (f . i) & yi = (g . i) & xi <= yi by A28, A29, YELLOW_1:def 4;

        reconsider a1 = a, b1 = b as Element of (L |^ X) by A6;

        

         A33: ex f,g be Function st f = a1 & g = b1 & for i be object st i in X holds ex R be RelStr, xi,yi be Element of R st R = (tXL . i) & xi = (f . i) & yi = (g . i) & xi <= yi

        proof

          take f, g;

          thus f = a1 & g = b1 by A30, A31;

          let i be object;

          assume

           A34: i in X;

          then

          consider R be RelStr, xi,yi be Element of R such that

           A35: R = (tXS . i) and

           A36: xi = (f . i) and

           A37: yi = (g . i) and

           A38: xi <= yi by A32;

          take R1 = L;

          reconsider xi1 = xi, yi1 = yi as Element of R1 by A1, A34, A35, FUNCOP_1: 7;

          take xi1, yi1;

          thus R1 = (tXL . i) by A34, FUNCOP_1: 7;

          thus xi1 = (f . i) & yi1 = (g . i) by A36, A37;

          the InternalRel of R = the InternalRel of S by A34, A35, FUNCOP_1: 7;

          then [xi1, yi1] in the InternalRel of R1 by A1, A38, ORDERS_2:def 5;

          hence thesis by ORDERS_2:def 5;

        end;

        

         A39: (L |^ X) = ( product tXL) by YELLOW_1:def 5;

        then the carrier of (L |^ X) = ( product ( Carrier tXL)) by YELLOW_1:def 4;

        then a1 <= b1 by A33, A39, YELLOW_1:def 4;

        hence thesis by A25, ORDERS_2:def 5;

      end;

      hence thesis by A7, A6, XBOOLE_0:def 10;

    end;

    theorem :: WAYBEL27:16

    for S1,S2,T1,T2 be non empty TopSpace st the TopStruct of S1 = the TopStruct of S2 & the TopStruct of T1 = the TopStruct of T2 holds ( oContMaps (S1,T1)) = ( oContMaps (S2,T2))

    proof

      let S1,S2,T1,T2 be non empty TopSpace;

      assume that

       A1: the TopStruct of S1 = the TopStruct of S2 and

       A2: the TopStruct of T1 = the TopStruct of T2;

      

       A3: ( oContMaps (S2,T2)) = ( ContMaps (S2,( Omega T2))) by WAYBEL26:def 1;

      ( Omega T1) = ( Omega T2) by A2, WAYBEL25: 13;

      then

      reconsider oCM2 = ( oContMaps (S2,T2)) as full SubRelStr of (( Omega T1) |^ the carrier of S1) by A3, A1, WAYBEL24:def 3;

      ( oContMaps (S1,T1)) = ( ContMaps (S1,( Omega T1))) by WAYBEL26:def 1;

      then

      reconsider oCM1 = ( oContMaps (S1,T1)) as full SubRelStr of (( Omega T1) |^ the carrier of S1) by WAYBEL24:def 3;

      the carrier of oCM1 = the carrier of oCM2

      proof

        thus the carrier of oCM1 c= the carrier of oCM2

        proof

          let x be object;

          

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

          assume x in the carrier of oCM1;

          then x in the carrier of ( ContMaps (S1,( Omega T1))) by WAYBEL26:def 1;

          then

          consider f be Function of S1, ( Omega T1) such that

           A5: x = f and

           A6: f is continuous by WAYBEL24:def 3;

          

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

          then

          reconsider f1 = f as Function of S2, ( Omega T2) by A4, A1, A2;

          for P1 be Subset of ( Omega T2) st P1 is closed holds (f1 " P1) is closed

          proof

            let P1 be Subset of ( Omega T2);

            reconsider P = P1 as Subset of ( Omega T1) by A2, A7, A4;

            assume P1 is closed;

            then P is closed by A2, A7, A4, TOPS_3: 79;

            then (f " P) is closed by A6, PRE_TOPC:def 6;

            hence thesis by A1, TOPS_3: 79;

          end;

          then f1 is continuous by PRE_TOPC:def 6;

          then x in the carrier of ( ContMaps (S2,( Omega T2))) by A5, WAYBEL24:def 3;

          hence thesis by WAYBEL26:def 1;

        end;

        let x be object;

        

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

        assume x in the carrier of oCM2;

        then x in the carrier of ( ContMaps (S2,( Omega T2))) by WAYBEL26:def 1;

        then

        consider f be Function of S2, ( Omega T2) such that

         A9: x = f and

         A10: f is continuous by WAYBEL24:def 3;

        

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

        then

        reconsider f1 = f as Function of S1, ( Omega T1) by A8, A1, A2;

        for P1 be Subset of ( Omega T1) st P1 is closed holds (f1 " P1) is closed

        proof

          let P1 be Subset of ( Omega T1);

          reconsider P = P1 as Subset of ( Omega T2) by A2, A11, A8;

          assume P1 is closed;

          then P is closed by A2, A11, A8, TOPS_3: 79;

          then (f " P) is closed by A10, PRE_TOPC:def 6;

          hence thesis by A1, TOPS_3: 79;

        end;

        then f1 is continuous by PRE_TOPC:def 6;

        then x in the carrier of ( ContMaps (S1,( Omega T1))) by A9, WAYBEL24:def 3;

        hence thesis by WAYBEL26:def 1;

      end;

      hence thesis by YELLOW_0: 57;

    end;

    theorem :: WAYBEL27:17

    

     Th17: for X be set holds ex f be Function of ( BoolePoset X), (( BoolePoset { 0 }) |^ X) st f is isomorphic & for Y be Subset of X holds (f . Y) = ( chi (Y,X))

    proof

      let Z be set;

      per cases ;

        suppose

         A1: Z = {} ;

        then

         A2: (( BoolePoset { 0 }) |^ Z) = RelStr (# { {} }, ( id { {} }) #) by YELLOW_1: 27;

        

         A3: ( InclPoset ( bool {} )) = RelStr (# ( bool {} ), ( RelIncl ( bool {} )) #) by YELLOW_1:def 1;

        

         A4: ( BoolePoset Z) = ( InclPoset ( bool {} )) by A1, YELLOW_1: 4;

        then

        reconsider f = ( id { {} }) as Function of ( BoolePoset Z), (( BoolePoset { 0 }) |^ Z) by A3, A1, YELLOW_1: 27, ZFMISC_1: 1;

        take f;

        

         A5: ( rng ( id { {} })) = { {} };

        for x,y be Element of ( BoolePoset Z) holds x <= y iff (f . x) <= (f . y) by A4, A3;

        hence f is isomorphic by A2, A5, WAYBEL_0: 66;

        let Y be Subset of Z;

        Y = {} by A1;

        then Y in { {} } by TARSKI:def 1;

        then (f . Y) = {} by A1, FUNCT_1: 18;

        hence thesis by A1;

      end;

        suppose Z <> {} ;

        then

        reconsider Z9 = Z as non empty set;

        (( BoolePoset { 0 }) |^ Z) = ( product (Z9 --> ( BoolePoset { 0 }))) by YELLOW_1:def 5;

        hence thesis by WAYBEL18: 14;

      end;

    end;

    theorem :: WAYBEL27:18

    

     Th18: for X be set holds (( BoolePoset X),(( BoolePoset { 0 }) |^ X)) are_isomorphic

    proof

      let X be set;

      consider f be Function of ( BoolePoset X), (( BoolePoset { 0 }) |^ X) such that

       A1: f is isomorphic and for Y be Subset of X holds (f . Y) = ( chi (Y,X)) by Th17;

      take f;

      thus thesis by A1;

    end;

    theorem :: WAYBEL27:19

    

     Th19: for X,Y be non empty set, T be non empty Poset holds for S1 be full non empty SubRelStr of ((T |^ X) |^ Y) holds for S2 be full non empty SubRelStr of ((T |^ Y) |^ X) holds for F be Function of S1, S2 st F is commuting holds F is monotone

    proof

      let X,Y be non empty set, T be non empty Poset;

      let S1 be full non empty SubRelStr of ((T |^ X) |^ Y);

      let S2 be full non empty SubRelStr of ((T |^ Y) |^ X);

      let F be Function of S1, S2 such that for x be set st x in ( dom F) holds x is Function-yielding Function and

       A1: for f be Function st f in ( dom F) holds (F . f) = ( commute f);

      let f,g be Element of S1;

      

       A2: ( dom F) = the carrier of S1 by FUNCT_2:def 1;

      then

       A3: (F . g) = ( commute g) by A1;

      reconsider Fa = (F . f), Fb = (F . g) as Element of ((T |^ Y) |^ X) by YELLOW_0: 58;

      reconsider a = f, b = g as Element of ((T |^ X) |^ Y) by YELLOW_0: 58;

      

       A4: the carrier of ((T |^ X) |^ Y) = ( Funcs (Y,the carrier of (T |^ X))) by YELLOW_1: 28

      .= ( Funcs (Y,( Funcs (X,the carrier of T)))) by YELLOW_1: 28;

      assume f <= g;

      then

       A5: a <= b by YELLOW_0: 59;

      

       A6: (F . f) = ( commute a) by A2, A1;

      now

        let x be Element of X;

        now

          let y be Element of Y;

          

           A7: ((Fa . x) . y) = ((a . y) . x) by A4, A6, FUNCT_6: 56;

          

           A8: ((Fb . x) . y) = ((b . y) . x) by A4, A3, FUNCT_6: 56;

          (a . y) <= (b . y) by A5, Th14;

          hence ((Fa . x) . y) <= ((Fb . x) . y) by A7, A8, Th14;

        end;

        hence (Fa . x) <= (Fb . x) by Th14;

      end;

      then Fa <= Fb by Th14;

      hence thesis by YELLOW_0: 60;

    end;

    theorem :: WAYBEL27:20

    

     Th20: for X,Y be non empty set, T be non empty Poset holds for S1 be full non empty SubRelStr of ((T |^ Y) |^ X) holds for S2 be full non empty SubRelStr of (T |^ [:X, Y:]) holds for F be Function of S1, S2 st F is uncurrying holds F is monotone

    proof

      let X,Y be non empty set, T be non empty Poset;

      let S1 be full non empty SubRelStr of ((T |^ Y) |^ X);

      let S2 be full non empty SubRelStr of (T |^ [:X, Y:]);

      let F be Function of S1, S2 such that for x be set st x in ( dom F) holds x is Function-yielding Function and

       A1: for f be Function st f in ( dom F) holds (F . f) = ( uncurry f);

      let f,g be Element of S1;

      reconsider a = f, b = g as Element of ((T |^ Y) |^ X) by YELLOW_0: 58;

      

       A2: ( dom F) = the carrier of S1 by FUNCT_2:def 1;

      then

       A3: (F . g) = ( uncurry b) by A1;

      reconsider Fa = (F . f), Fb = (F . g) as Element of (T |^ [:X, Y:]) by YELLOW_0: 58;

      assume f <= g;

      then

       A4: a <= b by YELLOW_0: 59;

      

       A5: the carrier of (T |^ Y) = ( Funcs (Y,the carrier of T)) by YELLOW_1: 28;

      then

       A6: the carrier of ((T |^ Y) |^ X) = ( Funcs (X,( Funcs (Y,the carrier of T)))) by YELLOW_1: 28;

      

       A7: (F . f) = ( uncurry a) by A2, A1;

      now

        let xy be Element of [:X, Y:];

        consider x,y be object such that

         A8: x in X and

         A9: y in Y and

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

        reconsider y as Element of Y by A9;

        reconsider x as Element of X by A8;

        

         A11: (a . x) <= (b . x) by A4, Th14;

        b is Function of X, ( Funcs (Y,the carrier of T)) by A6, FUNCT_2: 66;

        then

         A12: ( dom b) = X by FUNCT_2:def 1;

        a is Function of X, ( Funcs (Y,the carrier of T)) by A6, FUNCT_2: 66;

        then

         A13: ( dom a) = X by FUNCT_2:def 1;

        (b . x) is Function of Y, the carrier of T by A5, FUNCT_2: 66;

        then ( dom (b . x)) = Y by FUNCT_2:def 1;

        then

         A14: (Fb . (x,y)) = ((b . x) . y) by A12, A3, FUNCT_5: 38;

        (a . x) is Function of Y, the carrier of T by A5, FUNCT_2: 66;

        then ( dom (a . x)) = Y by FUNCT_2:def 1;

        then (Fa . (x,y)) = ((a . x) . y) by A13, A7, FUNCT_5: 38;

        hence (Fa . xy) <= (Fb . xy) by A14, A11, A10, Th14;

      end;

      then Fa <= Fb by Th14;

      hence thesis by YELLOW_0: 60;

    end;

    theorem :: WAYBEL27:21

    

     Th21: for X,Y be non empty set, T be non empty Poset holds for S1 be full non empty SubRelStr of ((T |^ Y) |^ X) holds for S2 be full non empty SubRelStr of (T |^ [:X, Y:]) holds for F be Function of S2, S1 st F is currying holds F is monotone

    proof

      let X,Y be non empty set, T be non empty Poset;

      let S1 be full non empty SubRelStr of ((T |^ Y) |^ X);

      let S2 be full non empty SubRelStr of (T |^ [:X, Y:]);

      let F be Function of S2, S1 such that for x be set st x in ( dom F) holds x is Function & ( proj1 x) is Relation and

       A1: for f be Function st f in ( dom F) holds (F . f) = ( curry f);

      let f,g be Element of S2;

      reconsider a = f, b = g as Element of (T |^ [:X, Y:]) by YELLOW_0: 58;

      

       A2: ( dom F) = the carrier of S2 by FUNCT_2:def 1;

      then

       A3: (F . g) = ( curry b) by A1;

      reconsider Fa = (F . f), Fb = (F . g) as Element of ((T |^ Y) |^ X) by YELLOW_0: 58;

      assume f <= g;

      then

       A4: a <= b by YELLOW_0: 59;

      

       A5: the carrier of (T |^ Y) = ( Funcs (Y,the carrier of T)) by YELLOW_1: 28;

      then

       A6: the carrier of ((T |^ Y) |^ X) = ( Funcs (X,( Funcs (Y,the carrier of T)))) by YELLOW_1: 28;

      

       A7: (F . f) = ( curry a) by A2, A1;

      now

        let x be Element of X;

        now

          let y be Element of Y;

          reconsider xy = [x, y] as Element of [:X, Y:];

          (Fa . x) is Function of Y, the carrier of T by A5, FUNCT_2: 66;

          then

           A8: ( dom (Fa . x)) = Y by FUNCT_2:def 1;

          Fa is Function of X, ( Funcs (Y,the carrier of T)) by A6, FUNCT_2: 66;

          then ( dom Fa) = X by FUNCT_2:def 1;

          then ((Fa . x) . y) = (a . (x,y)) by A8, A7, FUNCT_5: 31;

          then

           A9: ((Fa . x) . y) = (a . xy);

          (Fb . x) is Function of Y, the carrier of T by A5, FUNCT_2: 66;

          then

           A10: ( dom (Fb . x)) = Y by FUNCT_2:def 1;

          Fb is Function of X, ( Funcs (Y,the carrier of T)) by A6, FUNCT_2: 66;

          then ( dom Fb) = X by FUNCT_2:def 1;

          then ((Fb . x) . y) = (b . (x,y)) by A10, A3, FUNCT_5: 31;

          hence ((Fa . x) . y) <= ((Fb . x) . y) by A9, A4, Th14;

        end;

        hence (Fa . x) <= (Fb . x) by Th14;

      end;

      then Fa <= Fb by Th14;

      hence thesis by YELLOW_0: 60;

    end;

    begin

    definition

      let S be non empty RelStr;

      let T be non empty reflexive antisymmetric RelStr;

      :: WAYBEL27:def4

      func UPS (S,T) -> strict RelStr means

      : Def4: it is full SubRelStr of (T |^ the carrier of S) & for x be set holds x in the carrier of it iff x is directed-sups-preserving Function of S, T;

      existence

      proof

        defpred P[ object] means $1 is directed-sups-preserving Function of S, T;

        consider X be set such that

         A1: for a be object holds a in X iff a in the carrier of (T |^ the carrier of S) & P[a] from XBOOLE_0:sch 1;

        X c= the carrier of (T |^ the carrier of S) by A1;

        then

        reconsider X as Subset of (T |^ the carrier of S);

        take SX = ( subrelstr X);

        thus SX is full SubRelStr of (T |^ the carrier of S);

        let f be set;

        thus f in the carrier of SX implies f is directed-sups-preserving Function of S, T

        proof

          assume f in the carrier of SX;

          then f in X by YELLOW_0:def 15;

          hence thesis by A1;

        end;

        assume

         A2: f is directed-sups-preserving Function of S, T;

        then f is Element of (T |^ the carrier of S) by WAYBEL24: 19;

        then f in X by A1, A2;

        hence thesis by YELLOW_0:def 15;

      end;

      uniqueness

      proof

        let U1,U2 be strict RelStr;

        assume that

         A3: U1 is full SubRelStr of (T |^ the carrier of S) and

         A4: for x be set holds x in the carrier of U1 iff x is directed-sups-preserving Function of S, T and

         A5: U2 is full SubRelStr of (T |^ the carrier of S) and

         A6: for x be set holds x in the carrier of U2 iff x is directed-sups-preserving Function of S, T;

        the carrier of U1 = the carrier of U2

        proof

          hereby

            let x be object;

            assume x in the carrier of U1;

            then x is directed-sups-preserving Function of S, T by A4;

            hence x in the carrier of U2 by A6;

          end;

          let x be object;

          assume x in the carrier of U2;

          then x is directed-sups-preserving Function of S, T by A6;

          hence thesis by A4;

        end;

        hence thesis by A3, A5, YELLOW_0: 57;

      end;

    end

    registration

      let S be non empty RelStr;

      let T be non empty reflexive antisymmetric RelStr;

      cluster ( UPS (S,T)) -> non empty reflexive antisymmetric constituted-Functions;

      coherence

      proof

        set f = the directed-sups-preserving Function of S, T;

        f in the carrier of ( UPS (S,T)) by Def4;

        then ( UPS (S,T)) is full non empty SubRelStr of (T |^ the carrier of S) by Def4;

        hence thesis;

      end;

    end

    registration

      let S be non empty RelStr;

      let T be non empty Poset;

      cluster ( UPS (S,T)) -> transitive;

      coherence

      proof

        ( UPS (S,T)) is full SubRelStr of (T |^ the carrier of S) by Def4;

        hence thesis;

      end;

    end

    theorem :: WAYBEL27:22

    

     Th22: for S be non empty RelStr holds for T be non empty reflexive antisymmetric RelStr holds the carrier of ( UPS (S,T)) c= ( Funcs (the carrier of S,the carrier of T))

    proof

      let S be non empty RelStr;

      let T be non empty reflexive antisymmetric RelStr;

      ( UPS (S,T)) is SubRelStr of (T |^ the carrier of S) by Def4;

      then the carrier of ( UPS (S,T)) c= the carrier of (T |^ the carrier of S) by YELLOW_0:def 13;

      hence thesis by YELLOW_1: 28;

    end;

    definition

      let S be non empty RelStr;

      let T be non empty reflexive antisymmetric RelStr;

      let f be Element of ( UPS (S,T));

      let s be Element of S;

      :: original: .

      redefine

      func f . s -> Element of T ;

      coherence

      proof

        ( UPS (S,T)) is SubRelStr of (T |^ the carrier of S) by Def4;

        then

        reconsider p = f as Element of (T |^ the carrier of S) by YELLOW_0: 58;

        (p . s) = (p . s);

        hence thesis;

      end;

    end

    theorem :: WAYBEL27:23

    

     Th23: for S be non empty RelStr holds for T be non empty reflexive antisymmetric RelStr holds for f,g be Element of ( UPS (S,T)) holds f <= g iff for s be Element of S holds (f . s) <= (g . s)

    proof

      let S be non empty RelStr;

      let T be non empty reflexive antisymmetric RelStr;

      let f,g be Element of ( UPS (S,T));

      

       A1: ( UPS (S,T)) is full SubRelStr of (T |^ the carrier of S) by Def4;

      then

      reconsider a = f, b = g as Element of (T |^ the carrier of S) by YELLOW_0: 58;

      

       A2: f <= g iff a <= b by A1, YELLOW_0: 59, YELLOW_0: 60;

      hence f <= g implies for s be Element of S holds (f . s) <= (g . s) by Th14;

      assume for s be Element of S holds (f . s) <= (g . s);

      hence thesis by A2, Th14;

    end;

    theorem :: WAYBEL27:24

    

     Th24: for S,T be complete Scott TopLattice holds ( UPS (S,T)) = ( SCMaps (S,T))

    proof

      let S,T be complete Scott TopLattice;

      

       A1: the carrier of ( UPS (S,T)) = the carrier of ( SCMaps (S,T))

      proof

        thus the carrier of ( UPS (S,T)) c= the carrier of ( SCMaps (S,T))

        proof

          let x be object;

          assume x in the carrier of ( UPS (S,T));

          then

          reconsider f = x as directed-sups-preserving Function of S, T by Def4;

          f is continuous;

          hence thesis by WAYBEL17:def 2;

        end;

        let x be object;

        assume

         A2: x in the carrier of ( SCMaps (S,T));

        the carrier of ( SCMaps (S,T)) c= the carrier of ( MonMaps (S,T)) by YELLOW_0:def 13;

        then

        reconsider f = x as Function of S, T by A2, WAYBEL10: 9;

        f is continuous by A2, WAYBEL17:def 2;

        hence thesis by Def4;

      end;

      then

       A3: the carrier of ( UPS (S,T)) c= the carrier of ( MonMaps (S,T)) by YELLOW_0:def 13;

      ( UPS (S,T)) is full SubRelStr of (T |^ the carrier of S) by Def4;

      

      then the InternalRel of ( UPS (S,T)) = (the InternalRel of (T |^ the carrier of S) |_2 the carrier of ( UPS (S,T))) by YELLOW_0:def 14

      .= ((the InternalRel of (T |^ the carrier of S) |_2 the carrier of ( MonMaps (S,T))) |_2 the carrier of ( UPS (S,T))) by A3, WELLORD1: 22

      .= (the InternalRel of ( MonMaps (S,T)) |_2 the carrier of ( SCMaps (S,T))) by A1, YELLOW_0:def 14

      .= the InternalRel of ( SCMaps (S,T)) by YELLOW_0:def 14;

      hence thesis by A1;

    end;

    theorem :: WAYBEL27:25

    

     Th25: for S,S9 be non empty RelStr holds for T,T9 be non empty reflexive antisymmetric RelStr st the RelStr of S = the RelStr of S9 & the RelStr of T = the RelStr of T9 holds ( UPS (S,T)) = ( UPS (S9,T9))

    proof

      let S,S9 be non empty RelStr;

      let T,T9 be non empty reflexive antisymmetric RelStr;

      assume that

       A1: the RelStr of S = the RelStr of S9 and

       A2: the RelStr of T = the RelStr of T9;

      (T |^ the carrier of S) = (T9 |^ the carrier of S9) by A1, A2, Th15;

      then

       A3: ( UPS (S9,T9)) is full SubRelStr of (T |^ the carrier of S) by Def4;

      

       A4: the carrier of ( UPS (S,T)) = the carrier of ( UPS (S9,T9))

      proof

        thus the carrier of ( UPS (S,T)) c= the carrier of ( UPS (S9,T9))

        proof

          let x be object;

          assume x in the carrier of ( UPS (S,T));

          then

          reconsider x1 = x as directed-sups-preserving Function of S, T by Def4;

          reconsider y = x1 as Function of S9, T9 by A1, A2;

          y is directed-sups-preserving

          proof

            let X be Subset of S9;

            reconsider Y = X as Subset of S by A1;

            assume X is non empty directed;

            then Y is non empty directed by A1, WAYBEL_0: 3;

            then x1 preserves_sup_of Y by WAYBEL_0:def 37;

            hence thesis by A1, A2, WAYBEL_0: 65;

          end;

          hence thesis by Def4;

        end;

        let x be object;

        assume x in the carrier of ( UPS (S9,T9));

        then

        reconsider x1 = x as directed-sups-preserving Function of S9, T9 by Def4;

        reconsider y = x1 as Function of S, T by A1, A2;

        y is directed-sups-preserving

        proof

          let X be Subset of S;

          reconsider Y = X as Subset of S9 by A1;

          assume X is non empty directed;

          then Y is non empty directed by A1, WAYBEL_0: 3;

          then x1 preserves_sup_of Y by WAYBEL_0:def 37;

          hence thesis by A1, A2, WAYBEL_0: 65;

        end;

        hence thesis by Def4;

      end;

      ( UPS (S,T)) is full SubRelStr of (T |^ the carrier of S) by Def4;

      hence thesis by A3, A4, YELLOW_0: 57;

    end;

    registration

      let S,T be complete LATTICE;

      cluster ( UPS (S,T)) -> complete;

      coherence

      proof

        set T9 = the Scott TopAugmentation of T;

        set S9 = the Scott TopAugmentation of S;

        reconsider S9, T9 as complete Scott TopLattice;

        

         A1: the RelStr of T = the RelStr of T9 by YELLOW_9:def 4;

         the RelStr of S = the RelStr of S9 by YELLOW_9:def 4;

        

        then ( UPS (S,T)) = ( UPS (S9,T9)) by A1, Th25

        .= ( SCMaps (S9,T9)) by Th24

        .= ( ContMaps (S9,T9)) by WAYBEL24: 38;

        hence thesis;

      end;

    end

    theorem :: WAYBEL27:26

    

     Th26: for S,T be complete LATTICE holds ( UPS (S,T)) is sups-inheriting SubRelStr of (T |^ the carrier of S)

    proof

      let S,T be complete LATTICE;

      set S9 = the Scott TopAugmentation of S;

      set T9 = the Scott TopAugmentation of T;

      

       A1: the RelStr of T = the RelStr of T9 by YELLOW_9:def 4;

      then

       A2: (T9 |^ the carrier of S) = (T |^ the carrier of S) by Th15;

      

       A3: the RelStr of S = the RelStr of S9 by YELLOW_9:def 4;

      

      then ( UPS (S,T)) = ( UPS (S9,T9)) by A1, Th25

      .= ( SCMaps (S9,T9)) by Th24

      .= ( ContMaps (S9,T9)) by WAYBEL24: 38;

      hence thesis by A2, A3, WAYBEL24: 35;

    end;

    theorem :: WAYBEL27:27

    

     Th27: for S,T be complete LATTICE holds for A be Subset of ( UPS (S,T)) holds ( sup A) = ( "\/" (A,(T |^ the carrier of S)))

    proof

      let S,T be complete LATTICE;

      let A be Subset of ( UPS (S,T));

      

       A1: ( UPS (S,T)) is sups-inheriting full SubRelStr of (T |^ the carrier of S) by Def4, Th26;

       ex_sup_of (A,(T |^ the carrier of S)) by YELLOW_0: 17;

      then ( "\/" (A,(T |^ the carrier of S))) in the carrier of ( UPS (S,T)) by A1, YELLOW_0:def 19;

      hence thesis by A1, YELLOW_0: 68;

    end;

    definition

      let S1,S2,T1,T2 be non empty reflexive antisymmetric RelStr;

      let f be Function of S1, S2;

      let g be Function of T1, T2;

      :: WAYBEL27:def5

      func UPS (f,g) -> Function of ( UPS (S2,T1)), ( UPS (S1,T2)) means

      : Def5: for h be directed-sups-preserving Function of S2, T1 holds (it . h) = ((g * h) * f);

      existence

      proof

        defpred P[ set, set] means for h be Function st h = $1 holds $2 = ((g * h) * f);

        

         A3: for x be Element of ( UPS (S2,T1)) holds ex y be Element of ( UPS (S1,T2)) st P[x, y]

        proof

          let x be Element of ( UPS (S2,T1));

          reconsider h = x as directed-sups-preserving Function of S2, T1 by Def4;

          (h * f) is directed-sups-preserving Function of S1, T1 by A1, WAYBEL20: 28;

          then (g * (h * f)) is directed-sups-preserving Function of S1, T2 by A2, WAYBEL20: 28;

          then ((g * h) * f) is directed-sups-preserving Function of S1, T2 by RELAT_1: 36;

          then

          reconsider y = ((g * h) * f) as Element of ( UPS (S1,T2)) by Def4;

          take y;

          thus thesis;

        end;

        consider j be Function of the carrier of ( UPS (S2,T1)), the carrier of ( UPS (S1,T2)) such that

         A4: for x be Element of ( UPS (S2,T1)) holds P[x, (j . x)] from FUNCT_2:sch 3( A3);

        reconsider F = j as Function of ( UPS (S2,T1)), ( UPS (S1,T2));

        take F;

        let h be directed-sups-preserving Function of S2, T1;

        h is Element of ( UPS (S2,T1)) by Def4;

        hence thesis by A4;

      end;

      uniqueness

      proof

        let U1,U2 be Function of ( UPS (S2,T1)), ( UPS (S1,T2));

        assume that

         A5: for h be directed-sups-preserving Function of S2, T1 holds (U1 . h) = ((g * h) * f) and

         A6: for h be directed-sups-preserving Function of S2, T1 holds (U2 . h) = ((g * h) * f);

        for x be object st x in the carrier of ( UPS (S2,T1)) holds (U1 . x) = (U2 . x)

        proof

          let x be object;

          assume x in the carrier of ( UPS (S2,T1));

          then

          reconsider h = x as directed-sups-preserving Function of S2, T1 by Def4;

          

          thus (U1 . x) = ((g * h) * f) by A5

          .= (U2 . x) by A6;

        end;

        hence U1 = U2 by FUNCT_2: 12;

      end;

    end

    theorem :: WAYBEL27:28

    

     Th28: for S1,S2,S3,T1,T2,T3 be non empty Poset holds for f1 be directed-sups-preserving Function of S2, S3 holds for f2 be directed-sups-preserving Function of S1, S2 holds for g1 be directed-sups-preserving Function of T1, T2 holds for g2 be directed-sups-preserving Function of T2, T3 holds (( UPS (f2,g2)) * ( UPS (f1,g1))) = ( UPS ((f1 * f2),(g2 * g1)))

    proof

      let S1,S2,S3,T1,T2,T3 be non empty Poset;

      let f1 be directed-sups-preserving Function of S2, S3;

      let f2 be directed-sups-preserving Function of S1, S2;

      let g1 be directed-sups-preserving Function of T1, T2;

      let g2 be directed-sups-preserving Function of T2, T3;

      reconsider F = (f1 * f2) as directed-sups-preserving Function of S1, S3 by WAYBEL20: 28;

      reconsider G = (g2 * g1) as directed-sups-preserving Function of T1, T3 by WAYBEL20: 28;

      for h be directed-sups-preserving Function of S3, T1 holds ((( UPS (f2,g2)) * ( UPS (f1,g1))) . h) = ((G * h) * F)

      proof

        let h be directed-sups-preserving Function of S3, T1;

        (g1 * h) is directed-sups-preserving Function of S3, T2 by WAYBEL20: 28;

        then

        reconsider ghf = ((g1 * h) * f1) as directed-sups-preserving Function of S2, T2 by WAYBEL20: 28;

        ( dom ( UPS (f1,g1))) = the carrier of ( UPS (S3,T1)) by FUNCT_2:def 1;

        then h in ( dom ( UPS (f1,g1))) by Def4;

        

        then ((( UPS (f2,g2)) * ( UPS (f1,g1))) . h) = (( UPS (f2,g2)) . (( UPS (f1,g1)) . h)) by FUNCT_1: 13

        .= (( UPS (f2,g2)) . ((g1 * h) * f1)) by Def5;

        

        hence ((( UPS (f2,g2)) * ( UPS (f1,g1))) . h) = ((g2 * ghf) * f2) by Def5

        .= (g2 * (((g1 * h) * f1) * f2)) by RELAT_1: 36

        .= (g2 * ((g1 * (h * f1)) * f2)) by RELAT_1: 36

        .= (g2 * (g1 * ((h * f1) * f2))) by RELAT_1: 36

        .= (g2 * (g1 * (h * (f1 * f2)))) by RELAT_1: 36

        .= (g2 * ((g1 * h) * (f1 * f2))) by RELAT_1: 36

        .= ((g2 * (g1 * h)) * (f1 * f2)) by RELAT_1: 36

        .= ((G * h) * F) by RELAT_1: 36;

      end;

      hence thesis by Def5;

    end;

    theorem :: WAYBEL27:29

    

     Th29: for S,T be non empty reflexive antisymmetric RelStr holds ( UPS (( id S),( id T))) = ( id ( UPS (S,T)))

    proof

      let S,T be non empty reflexive antisymmetric RelStr;

      

       A1: for x be object st x in the carrier of ( UPS (S,T)) holds (( UPS (( id S),( id T))) . x) = x

      proof

        let x be object;

        assume x in the carrier of ( UPS (S,T));

        then

        reconsider f = x as directed-sups-preserving Function of S, T by Def4;

        (( UPS (( id S),( id T))) . f) = ((( id T) * f) * ( id S)) by Def5

        .= (f * ( id S)) by FUNCT_2: 17;

        hence thesis by FUNCT_2: 17;

      end;

      ( dom ( UPS (( id S),( id T)))) = the carrier of ( UPS (S,T)) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 17;

    end;

    theorem :: WAYBEL27:30

    

     Th30: for S1,S2,T1,T2 be complete LATTICE holds for f be directed-sups-preserving Function of S1, S2 holds for g be directed-sups-preserving Function of T1, T2 holds ( UPS (f,g)) is directed-sups-preserving

    proof

      let S1,S2,T1,T2 be complete LATTICE;

      let f be directed-sups-preserving Function of S1, S2;

      let g be directed-sups-preserving Function of T1, T2;

      let A be Subset of ( UPS (S2,T1));

      assume A is non empty directed;

      then

      reconsider H = A as directed non empty Subset of ( UPS (S2,T1));

      assume ex_sup_of (A,( UPS (S2,T1)));

      thus ex_sup_of ((( UPS (f,g)) .: A),( UPS (S1,T2))) by YELLOW_0: 17;

      ( UPS (S2,T1)) is full SubRelStr of (T1 |^ the carrier of S2) by Def4;

      then

      reconsider B = H as directed non empty Subset of (T1 |^ the carrier of S2) by YELLOW_2: 7;

      

       A1: ( UPS (S1,T2)) is full SubRelStr of (T2 |^ the carrier of S1) by Def4;

      then

      reconsider fgsA = (( UPS (f,g)) . ( sup H)) as Element of (T2 |^ the carrier of S1) by YELLOW_0: 58;

      the carrier of ( UPS (S1,T2)) c= the carrier of (T2 |^ the carrier of S1) by A1, YELLOW_0:def 13;

      then

      reconsider fgA = (( UPS (f,g)) .: H) as non empty Subset of (T2 |^ the carrier of S1) by XBOOLE_1: 1;

      

       A2: (T2 |^ the carrier of S1) = ( product (the carrier of S1 --> T2)) by YELLOW_1:def 5;

      then

       A3: ( dom ( sup fgA)) = the carrier of S1 by WAYBEL_3: 27;

      

       A4: (T1 |^ the carrier of S2) = ( product (the carrier of S2 --> T1)) by YELLOW_1:def 5;

       A5:

      now

        reconsider BB = B as directed Subset of ( product (the carrier of S2 --> T1)) by A4;

        let s be object;

        

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

        assume s in the carrier of S1;

        then

        reconsider x = s as Element of S1;

        reconsider sH = ( sup H) as directed-sups-preserving Function of S2, T1 by Def4;

        

         A7: ((the carrier of S2 --> T1) . (f . x)) = T1;

        ( dom sH) = the carrier of S2 by FUNCT_2:def 1;

        then (f . x) in ( dom sH);

        then

         A8: x in ( dom (sH * f)) by A6, FUNCT_1: 11;

        

         A9: ( pi (fgA,x)) = (g .: ( pi (A,(f . x))))

        proof

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

          proof

            let a be object;

            

             A10: ( dom g) = the carrier of T1 by FUNCT_2:def 1;

            assume a in ( pi (fgA,x));

            then

            consider F be Function such that

             A11: F in fgA and

             A12: a = (F . x) by CARD_3:def 6;

            consider G be object such that

             A13: G in ( dom ( UPS (f,g))) and

             A14: G in H and

             A15: F = (( UPS (f,g)) . G) by A11, FUNCT_1:def 6;

            reconsider G as directed-sups-preserving Function of S2, T1 by A13, Def4;

            

             A16: (G . (f . x)) in ( pi (A,(f . x))) by A14, CARD_3:def 6;

            

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

            ( dom G) = the carrier of S2 by FUNCT_2:def 1;

            then (f . x) in ( dom G);

            then

             A18: x in ( dom (G * f)) by A17, FUNCT_1: 11;

            a = (((g * G) * f) . x) by A12, A15, Def5

            .= ((g * (G * f)) . x) by RELAT_1: 36

            .= (g . ((G * f) . x)) by A18, FUNCT_1: 13

            .= (g . (G . (f . x))) by A17, FUNCT_1: 13;

            hence thesis by A10, A16, FUNCT_1:def 6;

          end;

          let a be object;

          

           A19: ( dom ( UPS (f,g))) = the carrier of ( UPS (S2,T1)) by FUNCT_2:def 1;

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

          then

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

           A20: F in ( pi (A,(f . x))) and

           A21: a = (g . F) by FUNCT_1:def 6;

          consider G be Function such that

           A22: G in A and

           A23: F = (G . (f . x)) by A20, CARD_3:def 6;

          reconsider G as directed-sups-preserving Function of S2, T1 by A22, Def4;

          ((g * G) * f) = (( UPS (f,g)) . G) by Def5;

          then

           A24: ((g * G) * f) in fgA by A22, A19, FUNCT_1:def 6;

          

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

          ( dom G) = the carrier of S2 by FUNCT_2:def 1;

          then (f . x) in ( dom G);

          then

           A26: x in ( dom (G * f)) by A25, FUNCT_1: 11;

          a = (g . ((G * f) . x)) by A21, A23, A25, FUNCT_1: 13

          .= ((g * (G * f)) . x) by A26, FUNCT_1: 13

          .= (((g * G) * f) . x) by RELAT_1: 36;

          hence thesis by A24, CARD_3:def 6;

        end;

        

         A27: ex_sup_of (( pi (B,(f . x))),T1) by YELLOW_0: 17;

        

         A28: ( pi (BB,(f . x))) is directed by YELLOW16: 35;

        

         A29: g preserves_sup_of ( pi (B,(f . x))) by A28, WAYBEL_0:def 37;

        ((the carrier of S1 --> T2) . x) = T2;

        

        hence (( sup fgA) . s) = ( sup ( pi (fgA,x))) by A2, YELLOW16: 33, YELLOW_0: 17

        .= (g . ( sup ( pi (B,(f . x))))) by A9, A29, A27

        .= (g . (( sup B) . (f . x))) by A4, A7, YELLOW16: 33, YELLOW_0: 17

        .= (g . (sH . (f . x))) by Th27

        .= (g . ((sH * f) . x)) by A6, FUNCT_1: 13

        .= ((g * (sH * f)) . x) by A8, FUNCT_1: 13

        .= (((g * sH) * f) . s) by RELAT_1: 36

        .= (fgsA . s) by Def5;

      end;

      

       A30: ( dom fgsA) = the carrier of S1 by A2, WAYBEL_3: 27;

      

      thus ( sup (( UPS (f,g)) .: A)) = ( sup fgA) by Th27

      .= (( UPS (f,g)) . ( sup A)) by A3, A30, A5;

    end;

    theorem :: WAYBEL27:31

    

     Th31: ( Omega Sierpinski_Space ) is Scott

    proof

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

      then

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

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

      

       A2: the topology of S = the topology of Sierpinski_Space by WAYBEL18: 12;

      

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

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

      

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

      .= S by WAYBEL25: 15;

      hence thesis;

    end;

    theorem :: WAYBEL27:32

    for S be complete Scott TopLattice holds ( oContMaps (S, Sierpinski_Space )) = ( UPS (S,( BoolePoset { 0 })))

    proof

      reconsider B1 = ( BoolePoset { 0 }) as complete LATTICE;

      reconsider OSS = ( Omega Sierpinski_Space ) as Scott complete TopAugmentation of B1 by Th31, WAYBEL26: 4;

      let S be complete Scott TopLattice;

      

       A1: the RelStr of S = the RelStr of S;

       the TopStruct of OSS = the TopStruct of Sierpinski_Space by WAYBEL25:def 2;

      then ( Omega OSS) = OSS by WAYBEL25: 13;

      then

       A2: the RelStr of OSS = the RelStr of B1 by WAYBEL25: 16;

      

      thus ( oContMaps (S, Sierpinski_Space )) = ( ContMaps (S,( Omega Sierpinski_Space ))) by WAYBEL26:def 1

      .= ( SCMaps (S,OSS)) by WAYBEL24: 38

      .= ( UPS (S,OSS)) by Th24

      .= ( UPS (S,( BoolePoset { 0 }))) by A1, A2, Th25;

    end;

    theorem :: WAYBEL27:33

    

     Th33: for S be complete LATTICE holds ex F be Function of ( UPS (S,( BoolePoset { 0 }))), ( InclPoset ( sigma S)) st F is isomorphic & for f be directed-sups-preserving Function of S, ( BoolePoset { 0 }) holds (F . f) = (f " {1})

    proof

      set T = ( BoolePoset { 0 });

      reconsider T9 = ( Omega Sierpinski_Space ) as Scott TopAugmentation of T by Th31, WAYBEL26: 4;

      let S be complete LATTICE;

      set S9 = the Scott TopAugmentation of S;

      

       A1: T = the RelStr of T9 by YELLOW_9:def 4;

      

       A2: the topology of S9 = ( sigma S) by YELLOW_9: 51;

       the RelStr of S = the RelStr of S9 by YELLOW_9:def 4;

      

      then ( UPS (S,T)) = ( UPS (S9,T9)) by A1, Th25

      .= ( SCMaps (S9,T9)) by Th24

      .= ( ContMaps (S9,T9)) by WAYBEL24: 38

      .= ( oContMaps (S9, Sierpinski_Space )) by WAYBEL26:def 1;

      then

      consider G be Function of ( InclPoset ( sigma S)), ( UPS (S,T)) such that

       A3: G is isomorphic and

       A4: for V be open Subset of S9 holds (G . V) = ( chi (V,the carrier of S9)) by A2, WAYBEL26: 5;

      take F = (G " );

      

       A5: ( rng G) = ( [#] ( UPS (S,T))) by A3, WAYBEL_0: 66;

      then G is onto by FUNCT_2:def 3;

      then

       A6: F = (G qua Function " ) by A3, TOPS_2:def 4;

      hence F is isomorphic by A3, WAYBEL_0: 68;

      let f be directed-sups-preserving Function of S, T;

      f in the carrier of ( UPS (S,T)) by Def4;

      then

      consider V be object such that

       A7: V in ( dom G) and

       A8: f = (G . V) by A5, FUNCT_1:def 3;

      ( dom G) = the carrier of ( InclPoset ( sigma S)) by FUNCT_2:def 1

      .= ( sigma S) by YELLOW_1: 1;

      then

      reconsider V as open Subset of S9 by A2, A7, PRE_TOPC:def 2;

      

      thus (F . f) = V by A3, A6, A7, A8, FUNCT_1: 34

      .= (( chi (V,the carrier of S9)) " {1}) by Th13

      .= (f " {1}) by A4, A8;

    end;

    theorem :: WAYBEL27:34

    

     Th34: for S be complete LATTICE holds (( UPS (S,( BoolePoset { 0 }))),( InclPoset ( sigma S))) are_isomorphic

    proof

      let S be complete LATTICE;

      consider F be Function of ( UPS (S,( BoolePoset { 0 }))), ( InclPoset ( sigma S)) such that

       A1: F is isomorphic and for f be directed-sups-preserving Function of S, ( BoolePoset { 0 }) holds (F . f) = (f " {1}) by Th33;

      take F;

      thus thesis by A1;

    end;

    theorem :: WAYBEL27:35

    

     Th35: for S1,S2,T1,T2 be complete LATTICE holds for f be Function of S1, S2, g be Function of T1, T2 st f is isomorphic & g is isomorphic holds ( UPS (f,g)) is isomorphic

    proof

      let S1,S2,T1,T2 be complete LATTICE;

      let f be Function of S1, S2, g be Function of T1, T2;

      assume that

       A1: f is isomorphic and

       A2: g is isomorphic;

      

       A3: g is sups-preserving Function of T1, T2 by A2, WAYBEL13: 20;

      

       A4: f is sups-preserving Function of S1, S2 by A1, WAYBEL13: 20;

      then

       A5: ( UPS (f,g)) is directed-sups-preserving Function of ( UPS (S2,T1)), ( UPS (S1,T2)) by A3, Th30;

      consider g9 be monotone Function of T2, T1 such that

       A6: (g * g9) = ( id T2) and

       A7: (g9 * g) = ( id T1) by A2, YELLOW16: 15;

      g9 is isomorphic by A2, A6, A7, YELLOW16: 15;

      then

       A8: g9 is sups-preserving Function of T2, T1 by WAYBEL13: 20;

      consider f9 be monotone Function of S2, S1 such that

       A9: (f * f9) = ( id S2) and

       A10: (f9 * f) = ( id S1) by A1, YELLOW16: 15;

      f9 is isomorphic by A1, A9, A10, YELLOW16: 15;

      then

       A11: f9 is sups-preserving Function of S2, S1 by WAYBEL13: 20;

      then

       A12: ( UPS (f9,g9)) is directed-sups-preserving Function of ( UPS (S1,T2)), ( UPS (S2,T1)) by A8, Th30;

      

       A13: (( UPS (f9,g9)) * ( UPS (f,g))) = ( UPS (( id S2),( id T1))) by A4, A3, A9, A7, A11, A8, Th28

      .= ( id ( UPS (S2,T1))) by Th29;

      (( UPS (f,g)) * ( UPS (f9,g9))) = ( UPS (( id S1),( id T2))) by A4, A3, A10, A6, A11, A8, Th28

      .= ( id ( UPS (S1,T2))) by Th29;

      hence thesis by A13, A5, A12, YELLOW16: 15;

    end;

    theorem :: WAYBEL27:36

    

     Th36: for S1,S2,T1,T2 be complete LATTICE st (S1,S2) are_isomorphic & (T1,T2) are_isomorphic holds (( UPS (S2,T1)),( UPS (S1,T2))) are_isomorphic

    proof

      let S1,S2,T1,T2 be complete LATTICE;

      given f be Function of S1, S2 such that

       A1: f is isomorphic;

      given g be Function of T1, T2 such that

       A2: g is isomorphic;

      take ( UPS (f,g));

      thus thesis by A1, A2, Th35;

    end;

    theorem :: WAYBEL27:37

    

     Th37: for S,T be complete LATTICE holds for f be directed-sups-preserving projection Function of T, T holds ( Image ( UPS (( id S),f))) = ( UPS (S,( Image f)))

    proof

      let S,T be complete LATTICE;

      let f be directed-sups-preserving projection Function of T, T;

      reconsider If = ( Image f) as complete LATTICE by YELLOW_2: 35;

      

       A1: (If |^ the carrier of S) is full SubRelStr of (T |^ the carrier of S) by YELLOW16: 39;

      ( UPS (S,If)) is full SubRelStr of (( Image f) |^ the carrier of S) by Def4;

      then

      reconsider UPSIf = ( UPS (S,If)) as full SubRelStr of (T |^ the carrier of S) by A1, WAYBEL15: 1;

      ( UPS (S,T)) is full SubRelStr of (T |^ the carrier of S) by Def4;

      then

      reconsider IUPS = ( Image ( UPS (( id S),f))) as full SubRelStr of (T |^ the carrier of S) by WAYBEL15: 1;

      the carrier of UPSIf = the carrier of IUPS

      proof

        thus the carrier of UPSIf c= the carrier of IUPS

        proof

          let x be object;

          

           A2: ( dom ( UPS (( id S),f))) = the carrier of ( UPS (S,T)) by FUNCT_2:def 1;

          assume x in the carrier of UPSIf;

          then

          reconsider h = x as directed-sups-preserving Function of S, If by Def4;

          the carrier of If c= the carrier of T by YELLOW_0:def 13;

          then

           A3: ( rng h) c= the carrier of T;

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

          then

          reconsider g = h as Function of S, T by A3, RELSET_1: 4;

          

           A4: g is directed-sups-preserving

          proof

            let X be Subset of S;

            assume

             A5: X is non empty directed;

            thus g preserves_sup_of X

            proof

              reconsider hX = (h .: X) as non empty directed Subset of If by A5, YELLOW_2: 15;

              assume

               A6: ex_sup_of (X,S);

              h preserves_sup_of X by A5, WAYBEL_0:def 37;

              then

               A7: ( sup hX) = (h . ( sup X)) by A6;

              thus

               A8: ex_sup_of ((g .: X),T) by YELLOW_0: 17;

              If is directed-sups-inheriting non empty full SubRelStr of T by YELLOW_2: 35;

              hence thesis by A7, A8, WAYBEL_0: 7;

            end;

          end;

          then

           A9: g in the carrier of ( UPS (S,T)) by Def4;

          (( UPS (( id S),f)) . g) = ((f * g) * ( id S)) by A4, Def5

          .= (h * ( id S)) by Th10

          .= g by FUNCT_2: 17;

          then x in ( rng ( UPS (( id S),f))) by A9, A2, FUNCT_1:def 3;

          hence thesis by YELLOW_0:def 15;

        end;

        let x be object;

        

         A10: ( rng f) = the carrier of ( subrelstr ( rng f)) by YELLOW_0:def 15;

        assume x in the carrier of IUPS;

        then x in ( rng ( UPS (( id S),f))) by YELLOW_0:def 15;

        then

        consider a be object such that

         A11: a in ( dom ( UPS (( id S),f))) and

         A12: x = (( UPS (( id S),f)) . a) by FUNCT_1:def 3;

        reconsider a as directed-sups-preserving Function of S, T by A11, Def4;

        

         A13: x = ((f * a) * ( id S)) by A12, Def5

        .= (f * a) by FUNCT_2: 17;

        then

        reconsider x0 = x as directed-sups-preserving Function of S, T by WAYBEL15: 11;

        

         A14: ( rng x0) c= the carrier of T;

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

        then

        reconsider x1 = x0 as Function of S, If by A10, A13, A14, FUNCT_2: 2, RELAT_1: 26;

        x1 is directed-sups-preserving

        proof

          let X be Subset of S;

          assume

           A15: X is non empty directed;

          thus x1 preserves_sup_of X

          proof

            reconsider hX = (x0 .: X) as non empty directed Subset of T by A15, YELLOW_2: 15;

            

             A16: If is directed-sups-inheriting non empty full SubRelStr of T by YELLOW_2: 35;

            reconsider gX = (x1 .: X) as non empty directed Subset of If by Th12, A15, YELLOW_2: 15;

            assume

             A17: ex_sup_of (X,S);

            thus ex_sup_of ((x1 .: X),If) by YELLOW_0: 17;

            

             A18: x0 preserves_sup_of X by A15, WAYBEL_0:def 37;

            then ex_sup_of ((x0 .: X),T) by A17;

            then ( sup gX) = ( sup hX) by A16, WAYBEL_0: 7;

            hence thesis by A17, A18;

          end;

        end;

        hence thesis by Def4;

      end;

      hence thesis by YELLOW_0: 57;

    end;

     Lm1:

    now

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

      let f be directed-sups-preserving Function of X, (Y |^ M);

      the carrier of (Y |^ M) = ( Funcs (M,the carrier of Y)) by YELLOW_1: 28;

      then

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

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

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

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

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

      hence ( rng ( commute f)) c= ( Funcs (the carrier of X,the carrier of Y)) & ( dom ( commute f)) = M;

    end;

    theorem :: WAYBEL27:38

    

     Th38: for X be non empty set, S,T be non empty Poset holds for f be directed-sups-preserving Function of S, (T |^ X) holds for i be Element of X holds (( commute f) . i) is directed-sups-preserving Function of S, T

    proof

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

      let f be directed-sups-preserving Function of X, (Y |^ M);

      let i be Element of M;

      

       A1: ((M --> Y) . i) = Y;

      ( dom ( commute f)) = M by Lm1;

      then

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

      

       A3: f in ( Funcs (the carrier of X,( Funcs (M,the carrier of Y)))) by Lm1;

      then f is Function of the carrier of X, ( Funcs (M,the carrier of Y)) by FUNCT_2: 66;

      then

       A4: ( rng f) c= ( Funcs (M,the carrier of Y)) by RELAT_1:def 19;

      ( rng ( commute f)) c= ( Funcs (the carrier of X,the carrier of Y)) by Lm1;

      then

      consider g be Function such that

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

       A6: ( dom g) = the carrier of X and

       A7: ( rng g) c= the carrier of Y by A2, FUNCT_2:def 2;

      reconsider g as Function of X, Y by A6, A7, FUNCT_2: 2;

      

       A8: (Y |^ M) = ( product (M --> Y)) by YELLOW_1:def 5;

      g is directed-sups-preserving

      proof

        let A be Subset of X;

        assume A is non empty directed;

        then

        reconsider B = A as non empty directed Subset of X;

        assume

         A9: ex_sup_of (A,X);

        

         A10: f preserves_sup_of B by WAYBEL_0:def 37;

        then

         A11: ex_sup_of ((f .: B),(Y |^ M)) by A9;

        then ex_sup_of (( pi ((f .: A),i)),Y) by A8, A1, YELLOW16: 31;

        hence ex_sup_of ((g .: A),Y) by A4, A5, Th8;

        

         A12: ( pi ((f .: A),i)) = (g .: A) by A4, A5, Th8;

        ( sup (f .: B)) = (f . ( sup B)) by A9, A10;

        then ( sup ( pi ((f .: A),i))) = ((f . ( sup A)) . i) by A11, A8, A1, YELLOW16: 33;

        hence thesis by A3, A5, A12, FUNCT_6: 56;

      end;

      hence thesis by A5;

    end;

    theorem :: WAYBEL27:39

    

     Th39: for X be non empty set, S,T be non empty Poset holds for f be directed-sups-preserving Function of S, (T |^ X) holds ( commute f) is Function of X, the carrier of ( UPS (S,T))

    proof

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

      let f be directed-sups-preserving Function of X, (Y |^ M);

      

       A1: ( rng ( commute f)) c= the carrier of ( UPS (X,Y))

      proof

        let g be object;

        assume g in ( rng ( commute f));

        then

        consider i be object such that

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

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

        reconsider i as Element of M by A2, Lm1;

        (( commute f) . i) is directed-sups-preserving Function of X, Y by Th38;

        hence thesis by A3, Def4;

      end;

      ( dom ( commute f)) = M by Lm1;

      hence thesis by A1, FUNCT_2: 2;

    end;

    theorem :: WAYBEL27:40

    

     Th40: for X be non empty set, S,T be non empty Poset holds for f be Function of X, the carrier of ( UPS (S,T)) holds ( commute f) is directed-sups-preserving Function of S, (T |^ X)

    proof

      let X be non empty set, S,T be non empty Poset;

      let f be Function of X, the carrier of ( UPS (S,T));

      

       A1: the carrier of (T |^ X) = ( Funcs (X,the carrier of T)) by YELLOW_1: 28;

      

       A2: f in ( Funcs (X,the carrier of ( UPS (S,T)))) by FUNCT_2: 8;

      

       A3: ( Funcs (X,the carrier of ( UPS (S,T)))) c= ( Funcs (X,( Funcs (the carrier of S,the carrier of T)))) by Th22, FUNCT_5: 56;

      then ( commute f) in ( Funcs (the carrier of S,( Funcs (X,the carrier of T)))) by A2, FUNCT_6: 55;

      then

      reconsider g = ( commute f) as Function of S, (T |^ X) by A1, FUNCT_2: 66;

      

       A4: ( rng g) c= ( Funcs (X,the carrier of T)) by A1;

      g is directed-sups-preserving

      proof

        let A be Subset of S;

        assume A is non empty directed;

        then

        reconsider B = A as directed non empty Subset of S;

        

         A5: (T |^ X) = ( product (X --> T)) by YELLOW_1:def 5;

        then

         A6: ( dom (g . ( sup A))) = X by WAYBEL_3: 27;

        assume

         A7: ex_sup_of (A,S);

        now

          let x be Element of X;

          reconsider fx = (f . x) as directed-sups-preserving Function of S, T by Def4;

          

           A8: fx preserves_sup_of B by WAYBEL_0:def 37;

          ( commute g) = f by A3, A2, FUNCT_6: 57;

          then

           A9: (fx .: A) = ( pi ((g .: A),x)) by A4, Th8;

          thus ex_sup_of (( pi ((g .: A),x)),((X --> T) . x)) by A9, A8, A7;

        end;

        hence

         A10: ex_sup_of ((g .: A),(T |^ X)) by A5, YELLOW16: 31;

         A11:

        now

          let x be object;

          assume x in X;

          then

          reconsider a = x as Element of X;

          reconsider fx = (f . a) as directed-sups-preserving Function of S, T by Def4;

          

           A12: ((X --> T) . a) = T;

          ( commute g) = f by A3, A2, FUNCT_6: 57;

          then

           A13: (fx .: A) = ( pi ((g .: A),a)) by A4, Th8;

          fx preserves_sup_of B by WAYBEL_0:def 37;

          then ( sup ( pi ((g .: B),a))) = (fx . ( sup A)) by A13, A7;

          then (fx . ( sup A)) = (( sup (g .: B)) . a) by A5, A10, A12, YELLOW16: 33;

          hence (( sup (g .: A)) . x) = ((g . ( sup A)) . x) by A3, A2, FUNCT_6: 56;

        end;

        ( dom ( sup (g .: A))) = X by A5, WAYBEL_3: 27;

        hence thesis by A11, A6;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL27:41

    

     Th41: for X be non empty set, S,T be non empty Poset holds ex F be Function of ( UPS (S,(T |^ X))), (( UPS (S,T)) |^ X) st F is commuting isomorphic

    proof

      deffunc F( Function) = ( commute $1);

      let X be non empty set, S,T be non empty Poset;

      consider F be ManySortedSet of the carrier of ( UPS (S,(T |^ X))) such that

       A1: for f be Element of ( UPS (S,(T |^ X))) holds (F . f) = F(f) from PBOOLE:sch 5;

      

       A2: ( dom F) = the carrier of ( UPS (S,(T |^ X))) by PARTFUN1:def 2;

      

       A3: ( rng F) c= the carrier of (( UPS (S,T)) |^ X)

      proof

        let g be object;

        assume g in ( rng F);

        then

        consider f be object such that

         A4: f in ( dom F) and

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

        reconsider f as directed-sups-preserving Function of S, (T |^ X) by A4, Def4;

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

        then

        reconsider g as Function of X, the carrier of ( UPS (S,T)) by Th39;

        

         A6: ( rng g) c= the carrier of ( UPS (S,T));

        ( dom g) = X by FUNCT_2:def 1;

        then g in ( Funcs (X,the carrier of ( UPS (S,T)))) by A6, FUNCT_2:def 2;

        hence thesis by YELLOW_1: 28;

      end;

      then

      reconsider F as Function of ( UPS (S,(T |^ X))), (( UPS (S,T)) |^ X) by A2, FUNCT_2: 2;

      take F;

      consider G be ManySortedSet of the carrier of (( UPS (S,T)) |^ X) such that

       A7: for f be Element of (( UPS (S,T)) |^ X) holds (G . f) = F(f) from PBOOLE:sch 5;

      

       A8: ( dom G) = the carrier of (( UPS (S,T)) |^ X) by PARTFUN1:def 2;

      

       A9: ( rng G) c= the carrier of ( UPS (S,(T |^ X)))

      proof

        let g be object;

        assume g in ( rng G);

        then

        consider f be object such that

         A10: f in ( dom G) and

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

        the carrier of (( UPS (S,T)) |^ X) = ( Funcs (X,the carrier of ( UPS (S,T)))) by YELLOW_1: 28;

        then

        reconsider f as Function of X, the carrier of ( UPS (S,T)) by A10, FUNCT_2: 66;

        g = ( commute f) by A7, A10, A11;

        then g is directed-sups-preserving Function of S, (T |^ X) by Th40;

        hence thesis by Def4;

      end;

      then

      reconsider G as Function of (( UPS (S,T)) |^ X), ( UPS (S,(T |^ X))) by A8, FUNCT_2: 2;

      

       A12: G is commuting

      proof

        hereby

          let x be set;

          assume x in ( dom G);

          then x in ( Funcs (X,the carrier of ( UPS (S,T)))) by A8, YELLOW_1: 28;

          then x is Function of X, the carrier of ( UPS (S,T)) by FUNCT_2: 66;

          hence x is Function-yielding Function;

        end;

        thus thesis by A7, A8;

      end;

      

       A13: the carrier of (T |^ X) = ( Funcs (X,the carrier of T)) by YELLOW_1: 28;

      ( UPS (S,T)) is full SubRelStr of (T |^ the carrier of S) by Def4;

      then

       A14: (( UPS (S,T)) |^ X) is full SubRelStr of ((T |^ the carrier of S) |^ X) by YELLOW16: 39;

      

       A15: ( UPS (S,(T |^ X))) is full SubRelStr of ((T |^ X) |^ the carrier of S) by Def4;

      then

       A16: G is monotone by A12, A14, Th19;

      thus

       A17: F is commuting

      proof

        hereby

          let x be set;

          assume x in ( dom F);

          then x is Function of S, (T |^ X) by Def4;

          hence x is Function-yielding Function;

        end;

        thus thesis by A1, A2;

      end;

      then

       A18: F is monotone by A15, A14, Th19;

      the carrier of (( UPS (S,T)) |^ X) = ( Funcs (X,the carrier of ( UPS (S,T)))) by YELLOW_1: 28;

      then the carrier of (( UPS (S,T)) |^ X) c= ( Funcs (X,( Funcs (the carrier of S,the carrier of T)))) by Th22, FUNCT_5: 56;

      then

       A19: (F * G) = ( id (( UPS (S,T)) |^ X)) by A2, A8, A9, A17, A12, Th3;

      the carrier of ( UPS (S,(T |^ X))) c= ( Funcs (the carrier of S,the carrier of (T |^ X))) by Th22;

      then (G * F) = ( id ( UPS (S,(T |^ X)))) by A2, A3, A8, A17, A12, A13, Th3;

      hence thesis by A19, A18, A16, YELLOW16: 15;

    end;

    theorem :: WAYBEL27:42

    

     Th42: for X be non empty set, S,T be non empty Poset holds (( UPS (S,(T |^ X))),(( UPS (S,T)) |^ X)) are_isomorphic

    proof

      let X be non empty set, S,T be non empty Poset;

      consider F be Function of ( UPS (S,(T |^ X))), (( UPS (S,T)) |^ X) such that

       A1: F is commuting isomorphic by Th41;

      take F;

      thus thesis by A1;

    end;

    theorem :: WAYBEL27:43

    for S,T be continuous complete LATTICE holds ( UPS (S,T)) is continuous

    proof

      let S,T be continuous complete LATTICE;

      consider X be non empty set, p be projection Function of ( BoolePoset X), ( BoolePoset X) such that

       A1: p is directed-sups-preserving and

       A2: (T,( Image p)) are_isomorphic by WAYBEL15: 18;

      

       A3: (( id S) * ( id S)) = ( id S) by QUANTAL1:def 9;

      ( Image p) is complete non empty Poset by A2, WAYBEL20: 18;

      then (( UPS (S,T)),( UPS (S,( Image p)))) are_isomorphic by A2, Th36;

      then

       A4: (( UPS (S,T)),( Image ( UPS (( id S),p)))) are_isomorphic by A1, Th37;

      set L = the Scott TopAugmentation of S;

      

       A5: ( InclPoset ( sigma L)) is continuous by WAYBEL14: 36;

      

       A6: (( UPS (S,( BoolePoset { 0 }))),( InclPoset ( sigma S))) are_isomorphic by Th34;

      (p * p) = p by QUANTAL1:def 9;

      then (( UPS (( id S),p)) * ( UPS (( id S),p))) = ( UPS (( id S),p)) by A3, A1, Th28;

      then ( UPS (( id S),p)) is directed-sups-preserving idempotent Function of ( UPS (S,( BoolePoset X))), ( UPS (S,( BoolePoset X))) by A1, Th30, QUANTAL1:def 9;

      then

       A7: ( UPS (( id S),p)) is directed-sups-preserving projection Function of ( UPS (S,( BoolePoset X))), ( UPS (S,( BoolePoset X))) by WAYBEL_1:def 13;

      (( BoolePoset X),(( BoolePoset { 0 }) |^ X)) are_isomorphic by Th18;

      then

       A8: (( UPS (S,( BoolePoset X))),( UPS (S,(( BoolePoset { 0 }) |^ X)))) are_isomorphic by Th36;

       the RelStr of L = the RelStr of S by YELLOW_9:def 4;

      then ( InclPoset ( sigma S)) is continuous by A5, YELLOW_9: 52;

      then ( UPS (S,( BoolePoset { 0 }))) is continuous complete by A6, WAYBEL15: 9, WAYBEL_1: 6;

      then for x be Element of X holds ((X --> ( UPS (S,( BoolePoset { 0 })))) . x) is continuous complete LATTICE;

      then (X -POS_prod (X --> ( UPS (S,( BoolePoset { 0 }))))) is continuous by WAYBEL20: 33;

      then

       A9: (( UPS (S,( BoolePoset { 0 }))) |^ X) is continuous by YELLOW_1:def 5;

      (( UPS (S,(( BoolePoset { 0 }) |^ X))),(( UPS (S,( BoolePoset { 0 }))) |^ X)) are_isomorphic by Th42;

      then (( UPS (S,( BoolePoset X))),(( UPS (S,( BoolePoset { 0 }))) |^ X)) are_isomorphic by A8, WAYBEL_1: 7;

      then ( UPS (S,( BoolePoset X))) is continuous LATTICE by A9, WAYBEL15: 9, WAYBEL_1: 6;

      then ( Image ( UPS (( id S),p))) is continuous by A7, WAYBEL15: 15;

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

    end;

    theorem :: WAYBEL27:44

    for S,T be algebraic complete LATTICE holds ( UPS (S,T)) is algebraic

    proof

      let S,T be algebraic complete LATTICE;

      consider X be non empty set, p be closure Function of ( BoolePoset X), ( BoolePoset X) such that

       A1: p is directed-sups-preserving and

       A2: (T,( Image p)) are_isomorphic by WAYBEL13: 35;

      now

        let i be Element of ( UPS (S,( BoolePoset X)));

        reconsider f = i as directed-sups-preserving Function of S, ( BoolePoset X) by Def4;

        

         A3: (( UPS (( id S),p)) . f) = ((p * f) * ( id the carrier of S)) by A1, Def5

        .= (p * f) by FUNCT_2: 17;

         A4:

        now

          let s be Element of S;

          

           A5: ( id ( BoolePoset X)) <= p by WAYBEL_1:def 14;

          

           A6: (( id ( BoolePoset X)) . (i . s)) = (i . s);

          ((p * f) . s) = (p . (f . s)) by FUNCT_2: 15;

          hence (i . s) <= ((( UPS (( id S),p)) . i) . s) by A5, A6, A3, YELLOW_2: 9;

        end;

        thus (( id ( UPS (S,( BoolePoset X)))) . i) <= (( UPS (( id S),p)) . i) by A4, Th23;

      end;

      then

       A7: ( id ( UPS (S,( BoolePoset X)))) <= ( UPS (( id S),p)) by YELLOW_2: 9;

      

       A8: (( id S) * ( id S)) = ( id S) by QUANTAL1:def 9;

      (p * p) = p by QUANTAL1:def 9;

      then (( UPS (( id S),p)) * ( UPS (( id S),p))) = ( UPS (( id S),p)) by A8, A1, Th28;

      then ( UPS (( id S),p)) is directed-sups-preserving idempotent Function of ( UPS (S,( BoolePoset X))), ( UPS (S,( BoolePoset X))) by A1, Th30, QUANTAL1:def 9;

      then ( UPS (( id S),p)) is projection;

      then

      reconsider Sp = ( UPS (( id S),p)) as directed-sups-preserving closure Function of ( UPS (S,( BoolePoset X))), ( UPS (S,( BoolePoset X))) by A7, A1, Th30, WAYBEL_1:def 14;

      ( Image p) is complete non empty Poset by A2, WAYBEL20: 18;

      then (( UPS (S,T)),( UPS (S,( Image p)))) are_isomorphic by A2, Th36;

      then

       A9: (( UPS (S,T)),( Image Sp)) are_isomorphic by A1, Th37;

      (( BoolePoset X),(( BoolePoset { 0 }) |^ X)) are_isomorphic by Th18;

      then

       A10: (( UPS (S,( BoolePoset X))),( UPS (S,(( BoolePoset { 0 }) |^ X)))) are_isomorphic by Th36;

      set L = the Scott TopAugmentation of S;

      

       A11: ( InclPoset ( sigma S)) = ( InclPoset the topology of L) by YELLOW_9: 51;

      

       A12: the RelStr of L = the RelStr of S by YELLOW_9:def 4;

      then L is algebraic by WAYBEL13: 26, WAYBEL13: 32;

      then ex B be Basis of L st B = { ( uparrow x) where x be Element of L : x in the carrier of ( CompactSublatt L) } by WAYBEL14: 42;

      then ( InclPoset ( sigma L)) is algebraic by WAYBEL14: 43;

      then

       A13: ( InclPoset ( sigma S)) is algebraic by A12, YELLOW_9: 52;

      (( UPS (S,( BoolePoset { 0 }))),( InclPoset ( sigma S))) are_isomorphic by Th34;

      then ( UPS (S,( BoolePoset { 0 }))) is algebraic lower-bounded by A13, A11, WAYBEL13: 32, WAYBEL_1: 6;

      then (X -POS_prod (X --> ( UPS (S,( BoolePoset { 0 }))))) is lower-bounded algebraic;

      then

       A14: (( UPS (S,( BoolePoset { 0 }))) |^ X) is algebraic lower-bounded by YELLOW_1:def 5;

      (( UPS (S,(( BoolePoset { 0 }) |^ X))),(( UPS (S,( BoolePoset { 0 }))) |^ X)) are_isomorphic by Th42;

      then (( UPS (S,( BoolePoset X))),(( UPS (S,( BoolePoset { 0 }))) |^ X)) are_isomorphic by A10, WAYBEL_1: 7;

      then ( UPS (S,( BoolePoset X))) is algebraic lower-bounded LATTICE by A14, WAYBEL13: 32, WAYBEL_1: 6;

      then

       A15: ( Image Sp) is algebraic by WAYBEL_8: 24;

      ( Image Sp) is complete LATTICE by YELLOW_2: 30;

      hence thesis by A9, A15, WAYBEL13: 32, WAYBEL_1: 6;

    end;

    theorem :: WAYBEL27:45

    

     Th45: for R,S,T be complete LATTICE holds for f be directed-sups-preserving Function of R, ( UPS (S,T)) holds ( uncurry f) is directed-sups-preserving Function of [:R, S:], T

    proof

      let R,S,T be complete LATTICE;

      let f be directed-sups-preserving Function of R, ( UPS (S,T));

      

       A1: f in ( Funcs (the carrier of R,the carrier of ( UPS (S,T)))) by FUNCT_2: 8;

      ( Funcs (the carrier of R,the carrier of ( UPS (S,T)))) c= ( Funcs (the carrier of R,( Funcs (the carrier of S,the carrier of T)))) by Th22, FUNCT_5: 56;

      then ( uncurry f) in ( Funcs ( [:the carrier of R, the carrier of S:],the carrier of T)) by A1, FUNCT_6: 11;

      then ( uncurry f) in ( Funcs (the carrier of [:R, S:],the carrier of T)) by YELLOW_3:def 2;

      then

      reconsider g = ( uncurry f) as Function of [:R, S:], T by FUNCT_2: 66;

      

       A2: the carrier of ( UPS (S,T)) c= ( Funcs (the carrier of S,the carrier of T)) by Th22;

      now

        reconsider ST = ( UPS (S,T)) as full sups-inheriting non empty SubRelStr of (T |^ the carrier of S) by Def4, Th26;

        let a be Element of R, b be Element of S;

        reconsider f9 = f as directed-sups-preserving Function of R, ST;

        ( incl (ST,(T |^ the carrier of S))) is directed-sups-preserving by WAYBEL21: 10;

        then

         A3: (( incl (ST,(T |^ the carrier of S))) * f9) is directed-sups-preserving by WAYBEL20: 28;

        the carrier of ST c= the carrier of (T |^ the carrier of S) by YELLOW_0:def 13;

        then ( incl (ST,(T |^ the carrier of S))) = ( id the carrier of ST) by YELLOW_9:def 1;

        then f is directed-sups-preserving Function of R, (T |^ the carrier of S) by A3, FUNCT_2: 17;

        then

         A4: (( commute f) . b) is directed-sups-preserving Function of R, T by Th38;

        ( rng f) c= ( Funcs (the carrier of S,the carrier of T)) by A2;

        then ( curry g) = f by FUNCT_5: 48;

        then ( Proj (g,a)) = (f . a) by WAYBEL24:def 1;

        hence ( Proj (g,a)) is directed-sups-preserving by Def4;

        ( Proj (g,b)) = (( curry' g) . b) by WAYBEL24:def 2;

        hence ( Proj (g,b)) is directed-sups-preserving by A4, FUNCT_6:def 10;

      end;

      hence thesis by WAYBEL24: 18;

    end;

    theorem :: WAYBEL27:46

    

     Th46: for R,S,T be complete LATTICE holds for f be directed-sups-preserving Function of [:R, S:], T holds ( curry f) is directed-sups-preserving Function of R, ( UPS (S,T))

    proof

      let R,S,T be complete LATTICE;

      

       A1: [:the carrier of R, the carrier of S:] = the carrier of [:R, S:] by YELLOW_3:def 2;

      let f be directed-sups-preserving Function of [:R, S:], T;

      

       A2: the carrier of ( UPS ( [:R, S:],T)) c= ( Funcs (the carrier of [:R, S:],the carrier of T)) by Th22;

      f in the carrier of ( UPS ( [:R, S:],T)) by Def4;

      then ( curry f) in ( Funcs (the carrier of R,( Funcs (the carrier of S,the carrier of T)))) by A2, A1, FUNCT_6: 10;

      then

       A3: ( curry f) is Function of the carrier of R, ( Funcs (the carrier of S,the carrier of T)) by FUNCT_2: 66;

      then

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

      ( rng ( curry f)) c= the carrier of ( UPS (S,T))

      proof

        let y be object;

        assume y in ( rng ( curry f));

        then

        consider x be object such that

         A5: x in ( dom ( curry f)) and

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

        reconsider x as Element of R by A3, A5, FUNCT_2:def 1;

        ( Proj (f,x)) is directed-sups-preserving by WAYBEL24: 16;

        then y is directed-sups-preserving Function of S, T by A6, WAYBEL24:def 1;

        hence thesis by Def4;

      end;

      then

      reconsider g = ( curry f) as Function of R, ( UPS (S,T)) by A4, FUNCT_2: 2;

      

       A7: ( UPS (S,T)) is full SubRelStr of (T |^ the carrier of S) by Def4;

      

       A8: ( dom f) = the carrier of [:R, S:] by FUNCT_2:def 1;

      g is directed-sups-preserving

      proof

        let A be Subset of R;

        assume A is non empty directed;

        then

        reconsider B = A as directed non empty Subset of R;

        reconsider gsA = (g . ( sup A)) as Element of (T |^ the carrier of S) by A7, YELLOW_0: 58;

        assume ex_sup_of (A,R);

        thus ex_sup_of ((g .: A),( UPS (S,T))) by YELLOW_0: 17;

        

         A9: for s be Element of S holds ((the carrier of S --> T) . s) is complete LATTICE;

        the carrier of ( UPS (S,T)) c= the carrier of (T |^ the carrier of S) by A7, YELLOW_0:def 13;

        then (g .: B) c= the carrier of (T |^ the carrier of S);

        then

        reconsider gA = (g .: A) as non empty Subset of (T |^ the carrier of S);

        

         A10: (T |^ the carrier of S) = ( product (the carrier of S --> T)) by YELLOW_1:def 5;

        then

         A11: ( dom gsA) = the carrier of S by WAYBEL_3: 27;

        

         A12: ( dom gsA) = the carrier of S by A10, WAYBEL_3: 27;

         A13:

        now

          let x be object;

          assume x in the carrier of S;

          then

          reconsider s = x as Element of S;

          reconsider s1 = {s} as directed non empty Subset of S by WAYBEL_0: 5;

          reconsider As = [:B, s1:] as non empty directed Subset of [:R, S:];

          

           A14: f preserves_sup_of As by WAYBEL_0:def 37;

          

           A15: ex_sup_of (As, [:R, S:]) by YELLOW_0: 17;

          ((the carrier of S --> T) . s) = T;

          

          hence (( sup gA) . x) = ( sup ( pi (gA,s))) by A9, A10, WAYBEL_3: 32

          .= ( sup (f .: As)) by A8, Th9

          .= (f . ( sup As)) by A14, A15

          .= (f . [( sup ( proj1 As)), ( sup ( proj2 As))]) by YELLOW_3: 46

          .= (f . [( sup A), ( sup ( proj2 As))]) by FUNCT_5: 9

          .= (f . [( sup A), ( sup {s})]) by FUNCT_5: 9

          .= (f . (( sup A),s)) by YELLOW_0: 39

          .= (gsA . x) by A4, A12, FUNCT_5: 31;

        end;

        ( dom ( sup gA)) = the carrier of S by A10, WAYBEL_3: 27;

        then ( sup gA) = gsA by A13, A11;

        hence thesis by Th27;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL27:47

    for R,S,T be complete LATTICE holds ex f be Function of ( UPS (R,( UPS (S,T)))), ( UPS ( [:R, S:],T)) st f is uncurrying isomorphic

    proof

      deffunc F( Function) = ( uncurry $1);

      let R,S,T be complete LATTICE;

      consider F be ManySortedSet of the carrier of ( UPS (R,( UPS (S,T)))) such that

       A1: for f be Element of ( UPS (R,( UPS (S,T)))) holds (F . f) = F(f) from PBOOLE:sch 5;

      

       A2: ( dom F) = the carrier of ( UPS (R,( UPS (S,T)))) by PARTFUN1:def 2;

      

       A3: ( rng F) c= the carrier of ( UPS ( [:R, S:],T))

      proof

        let g be object;

        assume g in ( rng F);

        then

        consider f be object such that

         A4: f in ( dom F) and

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

        reconsider f as directed-sups-preserving Function of R, ( UPS (S,T)) by A4, Def4;

        g = ( uncurry f) by A1, A4, A5;

        then g is directed-sups-preserving Function of [:R, S:], T by Th45;

        hence thesis by Def4;

      end;

      then

      reconsider F as Function of ( UPS (R,( UPS (S,T)))), ( UPS ( [:R, S:],T)) by A2, FUNCT_2: 2;

      take F;

      thus

       A6: F is uncurrying

      proof

        hereby

          let x be set;

          assume x in ( dom F);

          then x is Function of R, ( UPS (S,T)) by Def4;

          hence x is Function-yielding Function;

        end;

        thus thesis by A1, A2;

      end;

      deffunc F( Function) = ( curry $1);

      consider G be ManySortedSet of the carrier of ( UPS ( [:R, S:],T)) such that

       A7: for f be Element of ( UPS ( [:R, S:],T)) holds (G . f) = F(f) from PBOOLE:sch 5;

      

       A8: ( dom G) = the carrier of ( UPS ( [:R, S:],T)) by PARTFUN1:def 2;

      

       A9: ( rng G) c= the carrier of ( UPS (R,( UPS (S,T))))

      proof

        let g be object;

        assume g in ( rng G);

        then

        consider f be object such that

         A10: f in ( dom G) and

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

        reconsider f as directed-sups-preserving Function of [:R, S:], T by A10, Def4;

        g = ( curry f) by A7, A10, A11;

        then g is directed-sups-preserving Function of R, ( UPS (S,T)) by Th46;

        hence thesis by Def4;

      end;

      then

      reconsider G as Function of ( UPS ( [:R, S:],T)), ( UPS (R,( UPS (S,T)))) by A8, FUNCT_2: 2;

      ( UPS (S,T)) is full SubRelStr of (T |^ the carrier of S) by Def4;

      then

       A12: (( UPS (S,T)) |^ the carrier of R) is full SubRelStr of ((T |^ the carrier of S) |^ the carrier of R) by YELLOW16: 39;

      ( UPS (R,( UPS (S,T)))) is full SubRelStr of (( UPS (S,T)) |^ the carrier of R) by Def4;

      then

       A13: ( UPS (R,( UPS (S,T)))) is full non empty SubRelStr of ((T |^ the carrier of S) |^ the carrier of R) by A12, YELLOW16: 26;

      the carrier of [:R, S:] = [:the carrier of R, the carrier of S:] by YELLOW_3:def 2;

      then

       A14: ( UPS ( [:R, S:],T)) is full non empty SubRelStr of (T |^ [:the carrier of R, the carrier of S:]) by Def4;

      then

       A15: F is monotone by A6, A13, Th20;

      

       A16: G is currying

      proof

        hereby

          let x be set;

          assume x in ( dom G);

          then

          reconsider f = x as Function of [:R, S:], T by Def4;

          ( proj1 f) = the carrier of [:R, S:] by FUNCT_2:def 1

          .= [:the carrier of R, the carrier of S:] by YELLOW_3:def 2;

          hence x is Function & ( proj1 x) is Relation;

        end;

        thus thesis by A7, A8;

      end;

      then

       A17: G is monotone by A13, A14, Th21;

      the carrier of ((T |^ the carrier of S) |^ the carrier of R) = ( Funcs (the carrier of R,the carrier of (T |^ the carrier of S))) by YELLOW_1: 28

      .= ( Funcs (the carrier of R,( Funcs (the carrier of S,the carrier of T)))) by YELLOW_1: 28;

      then the carrier of ( UPS (R,( UPS (S,T)))) c= ( Funcs (the carrier of R,( Funcs (the carrier of S,the carrier of T)))) by A13, YELLOW_0:def 13;

      then

       A18: (G * F) = ( id ( UPS (R,( UPS (S,T))))) by A2, A3, A8, A6, A16, Th4;

      the carrier of (T |^ [:the carrier of R, the carrier of S:]) = ( Funcs ( [:the carrier of R, the carrier of S:],the carrier of T)) by YELLOW_1: 28;

      then the carrier of ( UPS ( [:R, S:],T)) c= ( Funcs ( [:the carrier of R, the carrier of S:],the carrier of T)) by A14, YELLOW_0:def 13;

      then (F * G) = ( id ( UPS ( [:R, S:],T))) by A2, A8, A9, A6, A16, Th5;

      hence thesis by A18, A15, A17, YELLOW16: 15;

    end;