waybel24.miz



    begin

    theorem :: WAYBEL24:1

    for S,T be up-complete Scott TopLattice holds for M be Subset of ( SCMaps (S,T)) holds ( "\/" (M,( SCMaps (S,T)))) is continuous Function of S, T

    proof

      let S,T be up-complete Scott TopLattice;

      let M be Subset of ( SCMaps (S,T));

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

      then ( "\/" (M,( SCMaps (S,T)))) in the carrier of ( MonMaps (S,T));

      hence thesis by WAYBEL10: 9, WAYBEL17:def 2;

    end;

    registration

      let S be non empty RelStr, T be non empty reflexive RelStr;

      cluster constant -> monotone for Function of S, T;

      coherence

      proof

        let f be Function of S, T;

        assume

         A1: f is constant;

        for x,y be Element of S st x <= y holds (f . x) <= (f . y)

        proof

          let x,y be Element of S;

          assume x <= y;

          y in the carrier of S;

          then

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

          x in the carrier of S;

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

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

        end;

        hence thesis by WAYBEL_1:def 2;

      end;

    end

    registration

      let S be non empty RelStr, T be reflexive non empty RelStr, a be Element of T;

      cluster (S --> a) -> monotone;

      coherence

      proof

        set f = (S --> a);

        for x,y be Element of S st x <= y holds (f . x) <= (f . y)

        proof

          let x,y be Element of S;

          assume x <= y;

          (f . x) = ((the carrier of S --> a) . x)

          .= a by FUNCOP_1: 7

          .= ((the carrier of S --> a) . y) by FUNCOP_1: 7

          .= (f . y);

          hence thesis;

        end;

        hence thesis by WAYBEL_1:def 2;

      end;

    end

    theorem :: WAYBEL24:2

    for S be non empty RelStr, T be lower-bounded antisymmetric reflexive non empty RelStr holds ( Bottom ( MonMaps (S,T))) = (S --> ( Bottom T))

    proof

      let S be non empty RelStr, T be lower-bounded antisymmetric reflexive non empty RelStr;

      set L = ( MonMaps (S,T));

      reconsider f = (S --> ( Bottom T)) as Element of L by WAYBEL10: 9;

      reconsider f9 = f as Function of S, T;

      

       A1: for b be Element of L st b is_>=_than {} holds f <= b

      proof

        let b be Element of L;

        assume b is_>=_than {} ;

        reconsider b9 = b as Function of S, T by WAYBEL10: 9;

        reconsider b99 = b9, f99 = f as Element of (T |^ the carrier of S) by YELLOW_0: 58;

        for x be Element of S holds (f9 . x) <= (b9 . x)

        proof

          let x be Element of S;

          (f9 . x) = ((the carrier of S --> ( Bottom T)) . x)

          .= ( Bottom T) by FUNCOP_1: 7;

          hence thesis by YELLOW_0: 44;

        end;

        then f9 <= b9 by YELLOW_2: 9;

        then f99 <= b99 by WAYBEL10: 11;

        hence thesis by YELLOW_0: 60;

      end;

      f is_>=_than {} ;

      then f = ( "\/" ( {} ,L)) by A1, YELLOW_0: 30;

      hence thesis by YELLOW_0:def 11;

    end;

    theorem :: WAYBEL24:3

    for S be non empty RelStr, T be upper-bounded antisymmetric reflexive non empty RelStr holds ( Top ( MonMaps (S,T))) = (S --> ( Top T))

    proof

      let S be non empty RelStr, T be upper-bounded antisymmetric reflexive non empty RelStr;

      set L = ( MonMaps (S,T));

      reconsider f = (S --> ( Top T)) as Element of L by WAYBEL10: 9;

      reconsider f9 = f as Function of S, T;

      

       A1: for b be Element of L st b is_<=_than {} holds f >= b

      proof

        let b be Element of L;

        assume b is_<=_than {} ;

        reconsider b9 = b as Function of S, T by WAYBEL10: 9;

        reconsider b99 = b9, f99 = f as Element of (T |^ the carrier of S) by YELLOW_0: 58;

        for x be Element of S holds (f9 . x) >= (b9 . x)

        proof

          let x be Element of S;

          (f9 . x) = ((the carrier of S --> ( Top T)) . x)

          .= ( Top T) by FUNCOP_1: 7;

          hence thesis by YELLOW_0: 45;

        end;

        then f9 >= b9 by YELLOW_2: 9;

        then f99 >= b99 by WAYBEL10: 11;

        hence thesis by YELLOW_0: 60;

      end;

      f is_<=_than {} ;

      then f = ( "/\" ( {} ,L)) by A1, YELLOW_0: 31;

      hence thesis by YELLOW_0:def 12;

    end;

    scheme :: WAYBEL24:sch1

    FuncFraenkelSL { B,C() -> non empty RelStr , A( set) -> Element of C() , f() -> Function , P[ set] } :

(f() .: { A(x) where x be Element of B() : P[x] }) = { (f() . A(x)) where x be Element of B() : P[x] }

      provided

       A1: the carrier of C() c= ( dom f());

      set f = f();

      thus (f .: { A(x) where x be Element of B() : P[x] }) c= { (f . A(x)) where x be Element of B() : P[x] }

      proof

        let y be object;

        assume y in (f .: { A(x) where x be Element of B() : P[x] });

        then

        consider z be object such that z in ( dom f) and

         A2: z in { A(x) where x be Element of B() : P[x] } and

         A3: y = (f . z) by FUNCT_1:def 6;

        ex x be Element of B() st z = A(x) & P[x] by A2;

        hence thesis by A3;

      end;

      let y be object;

      assume y in { (f . A(x)) where x be Element of B() : P[x] };

      then

      consider x be Element of B() such that

       A4: y = (f . A(x)) and

       A5: P[x];

      A(x) in the carrier of C() & A(x) in { A(z) where z be Element of B() : P[z] } by A5;

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

    end;

    scheme :: WAYBEL24:sch2

    Fraenkel6A { B() -> LATTICE , F( set) -> set , P[ set], Q[ set] } :

{ F(v1) where v1 be Element of B() : P[v1] } = { F(v2) where v2 be Element of B() : Q[v2] }

      provided

       A1: for v be Element of B() holds P[v] iff Q[v];

      thus { F(v1) where v1 be Element of B() : P[v1] } c= { F(v2) where v2 be Element of B() : Q[v2] }

      proof

        let a be object;

        assume a in { F(v1) where v1 be Element of B() : P[v1] };

        then

        consider V1 be Element of B() such that

         A2: a = F(V1) and

         A3: P[V1];

        Q[V1] by A1, A3;

        hence thesis by A2;

      end;

      thus { F(v2) where v2 be Element of B() : Q[v2] } c= { F(v1) where v1 be Element of B() : P[v1] }

      proof

        let a be object;

        assume a in { F(v1) where v1 be Element of B() : Q[v1] };

        then

        consider V1 be Element of B() such that

         A4: a = F(V1) and

         A5: Q[V1];

        P[V1] by A1, A5;

        hence thesis by A4;

      end;

    end;

    theorem :: WAYBEL24:4

    

     Th4: for S,T be complete LATTICE, f be monotone Function of S, T holds for x be Element of S holds (f . x) = ( sup (f .: ( downarrow x)))

    proof

      let S,T be complete LATTICE, f be monotone Function of S, T;

      let x be Element of S;

      

       A1: for b be Element of T st b is_>=_than (f .: ( downarrow x)) holds (f . x) <= b

      proof

        let b be Element of T;

        x <= x;

        then ( dom f) = the carrier of S & x in ( downarrow x) by FUNCT_2:def 1, WAYBEL_0: 17;

        then

         A2: (f . x) in (f .: ( downarrow x)) by FUNCT_1:def 6;

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

        hence thesis by A2;

      end;

       ex_sup_of (( downarrow x),S) & ( sup ( downarrow x)) = x by WAYBEL_0: 34;

      then ( downarrow x) is_<=_than x by YELLOW_0: 30;

      then (f .: ( downarrow x)) is_<=_than (f . x) by YELLOW_2: 14;

      hence thesis by A1, YELLOW_0: 30;

    end;

    theorem :: WAYBEL24:5

    for S,T be complete lower-bounded LATTICE, f be monotone Function of S, T holds for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w <= x },T))

    proof

      let S,T be complete lower-bounded LATTICE;

      let f be monotone Function of S, T;

      let x be Element of S;

      deffunc A( Element of S) = $1;

      defpred P[ Element of S] means $1 <= x;

      defpred R[ Element of S] means ex y1 be Element of S st $1 <= y1 & y1 in {x};

      

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

      

       A2: (f .: { A(w) where w be Element of S : P[w] }) = { (f . A(w)) where w be Element of S : P[w] } from FuncFraenkelSL( A1);

      

       A3: for x2 be Element of S holds P[x2] iff R[x2]

      proof

        let x2 be Element of S;

        hereby

          

           A4: x in {x} by TARSKI:def 1;

          assume x2 <= x;

          hence ex y1 be Element of S st x2 <= y1 & y1 in {x} by A4;

        end;

        given y1 be Element of S such that

         A5: x2 <= y1 & y1 in {x};

        thus thesis by A5, TARSKI:def 1;

      end;

      { A(w) where w be Element of S : P[w] } = { A(x1) where x1 be Element of S : R[x1] } from Fraenkel6A( A3);

      then

       A6: ( downarrow x) = { w where w be Element of S : w <= x } by WAYBEL_0: 14;

      ( sup (f .: ( downarrow x))) = (f . x) by Th4

      .= (f . ( sup ( downarrow x))) by WAYBEL_0: 34;

      hence thesis by A2, A6, WAYBEL_0: 34;

    end;

    theorem :: WAYBEL24:6

    

     Th6: for S be RelStr, T be non empty RelStr, F be Subset of (T |^ the carrier of S) holds ( sup F) is Function of S, T

    proof

      let S be RelStr, T be non empty RelStr;

      let F be Subset of (T |^ the carrier of S);

      set f = ( sup F);

      f in the carrier of (T |^ the carrier of S);

      then f in ( Funcs (the carrier of S,the carrier of T)) by YELLOW_1: 28;

      then ex f9 be Function st f9 = f & ( dom f9) = the carrier of S & ( rng f9) c= the carrier of T by FUNCT_2:def 2;

      hence thesis by FUNCT_2:def 1, RELSET_1: 4;

    end;

    begin

    definition

      let X1,X2,Y be non empty RelStr;

      let f be Function of [:X1, X2:], Y;

      let x be Element of X1;

      :: WAYBEL24:def1

      func Proj (f,x) -> Function of X2, Y equals (( curry f) . x);

      correctness

      proof

         [:the carrier of X1, the carrier of X2:] = the carrier of [:X1, X2:] by YELLOW_3:def 2;

        then ( curry f) is Function of the carrier of X1, ( Funcs (the carrier of X2,the carrier of Y)) by FUNCT_5: 67;

        hence thesis by FUNCT_2: 5, FUNCT_2: 66;

      end;

    end

    reserve X1,X2,Y for non empty RelStr,

f for Function of [:X1, X2:], Y,

x for Element of X1,

y for Element of X2;

    theorem :: WAYBEL24:7

    

     Th7: for y be Element of X2 holds (( Proj (f,x)) . y) = (f . (x,y))

    proof

      let y be Element of X2;

      ( dom f) = the carrier of [:X1, X2:] by FUNCT_2:def 1

      .= [:the carrier of X1, the carrier of X2:] by YELLOW_3:def 2;

      then [x, y] in ( dom f) by ZFMISC_1: 87;

      hence thesis by FUNCT_5: 20;

    end;

    definition

      let X1,X2,Y be non empty RelStr;

      let f be Function of [:X1, X2:], Y;

      let y be Element of X2;

      :: WAYBEL24:def2

      func Proj (f,y) -> Function of X1, Y equals (( curry' f) . y);

      correctness

      proof

         [:the carrier of X1, the carrier of X2:] = the carrier of [:X1, X2:] by YELLOW_3:def 2;

        then ( curry' f) is Function of the carrier of X2, ( Funcs (the carrier of X1,the carrier of Y)) by FUNCT_5: 68;

        hence thesis by FUNCT_2: 5, FUNCT_2: 66;

      end;

    end

    theorem :: WAYBEL24:8

    

     Th8: for x be Element of X1 holds (( Proj (f,y)) . x) = (f . (x,y))

    proof

      let x be Element of X1;

      ( dom f) = the carrier of [:X1, X2:] by FUNCT_2:def 1

      .= [:the carrier of X1, the carrier of X2:] by YELLOW_3:def 2;

      then [x, y] in ( dom f) by ZFMISC_1: 87;

      hence thesis by FUNCT_5: 22;

    end;

    theorem :: WAYBEL24:9

    

     Th9: for R,S,T be non empty RelStr, f be Function of [:R, S:], T, a be Element of R, b be Element of S holds (( Proj (f,a)) . b) = (( Proj (f,b)) . a)

    proof

      let R,S,T be non empty RelStr, f be Function of [:R, S:], T, a be Element of R, b be Element of S;

      (( Proj (f,a)) . b) = (f . (a,b)) by Th7

      .= (( Proj (f,b)) . a) by Th8;

      hence thesis;

    end;

    registration

      let S be non empty RelStr, T be non empty reflexive RelStr;

      cluster antitone for Function of S, T;

      existence

      proof

        set c = the Element of T;

        take f = (S --> c);

        let x,y be Element of S;

        assume [x, y] in the InternalRel of S;

        let a,b be Element of T;

        assume that

         A1: a = (f . x) and

         A2: b = (f . y);

        a = c by A1, FUNCOP_1: 7;

        hence b <= a by A2, FUNCOP_1: 7;

      end;

    end

    theorem :: WAYBEL24:10

    

     Th10: for R,S,T be non empty reflexive RelStr, f be Function of [:R, S:], T, a be Element of R, b be Element of S st f is monotone holds ( Proj (f,a)) is monotone & ( Proj (f,b)) is monotone

    proof

      let R,S,T be non empty reflexive RelStr, f be Function of [:R, S:], T;

      let a be Element of R, b be Element of S;

      reconsider a as Element of R;

      reconsider b as Element of S;

      set g = ( Proj (f,b)), h = ( Proj (f,a));

      assume

       A1: f is monotone;

       A2:

      now

        let x,y be Element of R;

        

         A3: b <= b;

        

         A4: (g . x) = (f . (x,b)) & (g . y) = (f . (y,b)) by Th8;

        assume x <= y;

        then [x, b] <= [y, b] by A3, YELLOW_3: 11;

        hence (g . x) <= (g . y) by A1, A4, WAYBEL_1:def 2;

      end;

      now

        let x,y be Element of S;

        

         A5: a <= a;

        

         A6: (h . x) = (f . (a,x)) & (h . y) = (f . (a,y)) by Th7;

        assume x <= y;

        then [a, x] <= [a, y] by A5, YELLOW_3: 11;

        hence (h . x) <= (h . y) by A1, A6, WAYBEL_1:def 2;

      end;

      hence thesis by A2, WAYBEL_1:def 2;

    end;

    theorem :: WAYBEL24:11

    

     Th11: for R,S,T be non empty reflexive RelStr, f be Function of [:R, S:], T, a be Element of R, b be Element of S st f is antitone holds ( Proj (f,a)) is antitone & ( Proj (f,b)) is antitone

    proof

      let R,S,T be non empty reflexive RelStr, f be Function of [:R, S:], T;

      let a be Element of R, b be Element of S;

      reconsider a9 = a as Element of R;

      set g = ( Proj (f,b)), h = ( Proj (f,a));

      assume

       A1: f is antitone;

       A2:

      now

        reconsider b9 = b as Element of S;

        let x,y be Element of R;

        

         A3: b9 <= b9;

        

         A4: (g . x) = (f . (x,b)) & (g . y) = (f . (y,b)) by Th8;

        assume x <= y;

        then [x, b9] <= [y, b9] by A3, YELLOW_3: 11;

        hence (g . x) >= (g . y) by A1, A4;

      end;

      now

        let x,y be Element of S;

        

         A5: a9 <= a9;

        

         A6: (h . x) = (f . (a,x)) & (h . y) = (f . (a,y)) by Th7;

        assume x <= y;

        then [a9, x] <= [a9, y] by A5, YELLOW_3: 11;

        hence (h . x) >= (h . y) by A1, A6;

      end;

      hence thesis by A2;

    end;

    registration

      let R,S,T be non empty reflexive RelStr;

      let f be monotone Function of [:R, S:], T;

      let a be Element of R;

      cluster ( Proj (f,a)) -> monotone;

      coherence by Th10;

    end

    registration

      let R,S,T be non empty reflexive RelStr;

      let f be monotone Function of [:R, S:], T;

      let b be Element of S;

      cluster ( Proj (f,b)) -> monotone;

      coherence by Th10;

    end

    registration

      let R,S,T be non empty reflexive RelStr;

      let f be antitone Function of [:R, S:], T;

      let a be Element of R;

      cluster ( Proj (f,a)) -> antitone;

      coherence by Th11;

    end

    registration

      let R,S,T be non empty reflexive RelStr;

      let f be antitone Function of [:R, S:], T;

      let b be Element of S;

      cluster ( Proj (f,b)) -> antitone;

      coherence by Th11;

    end

    theorem :: WAYBEL24:12

    

     Th12: for R,S,T be LATTICE, f be Function of [:R, S:], T st (for a be Element of R, b be Element of S holds ( Proj (f,a)) is monotone & ( Proj (f,b)) is monotone) holds f is monotone

    proof

      let R,S,T be LATTICE, f be Function of [:R, S:], T;

      assume

       A1: for a be Element of R, b be Element of S holds ( Proj (f,a)) is monotone & ( Proj (f,b)) is monotone;

      now

        let x,y be Element of [:R, S:];

        assume

         A2: x <= y;

        then

         A3: (x `1 ) <= (y `1 ) by YELLOW_3: 12;

        

         A4: (x `2 ) <= (y `2 ) by A2, YELLOW_3: 12;

        

         A5: (f . ((x `1 ),(y `2 ))) = (( Proj (f,(x `1 ))) . (y `2 )) by Th7;

        ( Proj (f,(x `1 ))) is monotone & (f . ((x `1 ),(x `2 ))) = (( Proj (f,(x `1 ))) . (x `2 )) by A1, Th7;

        then

         A6: (f . [(x `1 ), (x `2 )]) <= (f . [(x `1 ), (y `2 )]) by A4, A5, WAYBEL_1:def 2;

        

         A7: (f . ((y `1 ),(y `2 ))) = (( Proj (f,(y `2 ))) . (y `1 )) by Th8;

        ( Proj (f,(y `2 ))) is monotone & (f . ((x `1 ),(y `2 ))) = (( Proj (f,(y `2 ))) . (x `1 )) by A1, Th8;

        then (f . [(x `1 ), (y `2 )]) <= (f . [(y `1 ), (y `2 )]) by A3, A7, WAYBEL_1:def 2;

        then

         A8: (f . [(x `1 ), (x `2 )]) <= (f . [(y `1 ), (y `2 )]) by A6, YELLOW_0:def 2;

        

         A9: [:the carrier of R, the carrier of S:] = the carrier of [:R, S:] by YELLOW_3:def 2;

        then (f . [(y `1 ), (y `2 )]) = (f . y) by MCART_1: 21;

        hence (f . x) <= (f . y) by A8, A9, MCART_1: 21;

      end;

      hence thesis by WAYBEL_1:def 2;

    end;

    theorem :: WAYBEL24:13

    for R,S,T be LATTICE, f be Function of [:R, S:], T st (for a be Element of R, b be Element of S holds ( Proj (f,a)) is antitone & ( Proj (f,b)) is antitone) holds f is antitone

    proof

      let R,S,T be LATTICE, f be Function of [:R, S:], T;

      assume

       A1: for a be Element of R, b be Element of S holds ( Proj (f,a)) is antitone & ( Proj (f,b)) is antitone;

      now

        let x,y be Element of [:R, S:];

        assume

         A2: x <= y;

        then

         A3: (x `1 ) <= (y `1 ) by YELLOW_3: 12;

        

         A4: (x `2 ) <= (y `2 ) by A2, YELLOW_3: 12;

        

         A5: (f . ((x `1 ),(y `2 ))) = (( Proj (f,(x `1 ))) . (y `2 )) by Th7;

        ( Proj (f,(x `1 ))) is antitone & (f . ((x `1 ),(x `2 ))) = (( Proj (f,(x `1 ))) . (x `2 )) by A1, Th7;

        then

         A6: (f . [(x `1 ), (x `2 )]) >= (f . [(x `1 ), (y `2 )]) by A4, A5;

        

         A7: (f . ((y `1 ),(y `2 ))) = (( Proj (f,(y `2 ))) . (y `1 )) by Th8;

        ( Proj (f,(y `2 ))) is antitone & (f . ((x `1 ),(y `2 ))) = (( Proj (f,(y `2 ))) . (x `1 )) by A1, Th8;

        then (f . [(x `1 ), (y `2 )]) >= (f . [(y `1 ), (y `2 )]) by A3, A7;

        then

         A8: (f . [(x `1 ), (x `2 )]) >= (f . [(y `1 ), (y `2 )]) by A6, YELLOW_0:def 2;

        

         A9: [:the carrier of R, the carrier of S:] = the carrier of [:R, S:] by YELLOW_3:def 2;

        then (f . [(y `1 ), (y `2 )]) = (f . y) by MCART_1: 21;

        hence (f . x) >= (f . y) by A8, A9, MCART_1: 21;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL24:14

    

     Th14: for R,S,T be LATTICE, f be Function of [:R, S:], T, b be Element of S, X be Subset of R holds (( Proj (f,b)) .: X) = (f .: [:X, {b}:])

    proof

      let R,S,T be LATTICE, f be Function of [:R, S:], T, b be Element of S, X be Subset of R;

      

       A1: (( Proj (f,b)) .: X) c= (f .: [:X, {b}:])

      proof

        let c be object;

        assume c in (( Proj (f,b)) .: X);

        then

        consider k be object such that

         A2: k in ( dom ( Proj (f,b))) and

         A3: k in X and

         A4: c = (( Proj (f,b)) . k) by FUNCT_1:def 6;

        b in {b} by TARSKI:def 1;

        then

         A5: [k, b] in [:X, {b}:] by A3, ZFMISC_1: 87;

         [:the carrier of R, the carrier of S:] = the carrier of [:R, S:] by YELLOW_3:def 2;

        then ( dom f) = [:the carrier of R, the carrier of S:] by FUNCT_2:def 1;

        then

         A6: [k, b] in ( dom f) by A2, ZFMISC_1: 87;

        c = (f . (k,b)) by A2, A4, Th8;

        hence thesis by A5, A6, FUNCT_1:def 6;

      end;

      (f .: [:X, {b}:]) c= (( Proj (f,b)) .: X)

      proof

        let c be object;

        assume c in (f .: [:X, {b}:]);

        then

        consider k be object such that k in ( dom f) and

         A7: k in [:X, {b}:] and

         A8: c = (f . k) by FUNCT_1:def 6;

        consider k1,k2 be object such that

         A9: k1 in X and

         A10: k2 in {b} and

         A11: k = [k1, k2] by A7, ZFMISC_1:def 2;

        

         A12: k2 = b by A10, TARSKI:def 1;

        c = (f . (k1,k2)) by A8, A11;

        then ( dom ( Proj (f,b))) = the carrier of R & c = (( Proj (f,b)) . k1) by A9, A12, Th8, FUNCT_2:def 1;

        hence thesis by A9, FUNCT_1:def 6;

      end;

      hence thesis by A1;

    end;

    theorem :: WAYBEL24:15

    

     Th15: for R,S,T be LATTICE, f be Function of [:R, S:], T, b be Element of R, X be Subset of S holds (( Proj (f,b)) .: X) = (f .: [: {b}, X:])

    proof

      let R,S,T be LATTICE, f be Function of [:R, S:], T, b be Element of R, X be Subset of S;

      

       A1: (( Proj (f,b)) .: X) c= (f .: [: {b}, X:])

      proof

        let c be object;

        assume c in (( Proj (f,b)) .: X);

        then

        consider k be object such that

         A2: k in ( dom ( Proj (f,b))) and

         A3: k in X and

         A4: c = (( Proj (f,b)) . k) by FUNCT_1:def 6;

        b in {b} by TARSKI:def 1;

        then

         A5: [b, k] in [: {b}, X:] by A3, ZFMISC_1: 87;

         [:the carrier of R, the carrier of S:] = the carrier of [:R, S:] by YELLOW_3:def 2;

        then ( dom f) = [:the carrier of R, the carrier of S:] by FUNCT_2:def 1;

        then

         A6: [b, k] in ( dom f) by A2, ZFMISC_1: 87;

        c = (f . (b,k)) by A2, A4, Th7;

        hence thesis by A5, A6, FUNCT_1:def 6;

      end;

      (f .: [: {b}, X:]) c= (( Proj (f,b)) .: X)

      proof

        let c be object;

        assume c in (f .: [: {b}, X:]);

        then

        consider k be object such that k in ( dom f) and

         A7: k in [: {b}, X:] and

         A8: c = (f . k) by FUNCT_1:def 6;

        consider k1,k2 be object such that

         A9: k1 in {b} and

         A10: k2 in X and

         A11: k = [k1, k2] by A7, ZFMISC_1:def 2;

        

         A12: k1 = b by A9, TARSKI:def 1;

        c = (f . (k1,k2)) by A8, A11;

        then ( dom ( Proj (f,b))) = the carrier of S & c = (( Proj (f,b)) . k2) by A10, A12, Th7, FUNCT_2:def 1;

        hence thesis by A10, FUNCT_1:def 6;

      end;

      hence thesis by A1;

    end;

    theorem :: WAYBEL24:16

    for R,S,T be LATTICE, f be Function of [:R, S:], T, a be Element of R, b be Element of S st f is directed-sups-preserving holds ( Proj (f,a)) is directed-sups-preserving & ( Proj (f,b)) is directed-sups-preserving

    proof

      let R,S,T be LATTICE, f be Function of [:R, S:], T, a be Element of R, b be Element of S;

      assume

       A1: f is directed-sups-preserving;

      

       A2: for X be Subset of S st X is non empty directed holds ( Proj (f,a)) preserves_sup_of X

      proof

        reconsider Y9 = {a} as non empty directed Subset of R by WAYBEL_0: 5;

        let X be Subset of S;

        assume X is non empty directed;

        then

        reconsider X9 = X as non empty directed Subset of S;

        ( Proj (f,a)) preserves_sup_of X

        proof

          

           A3: ( sup Y9) = a by YELLOW_0: 39;

          

           A4: f preserves_sup_of [:Y9, X9:] by A1;

          

           A5: (( Proj (f,a)) .: X) = (f .: [:Y9, X9:]) by Th15;

          

           A6: ex_sup_of (Y9,R) by YELLOW_0: 38;

          assume

           A7: ex_sup_of (X,S);

          then

           A8: ex_sup_of ( [:Y9, X9:], [:R, S:]) by A6, YELLOW_3: 39;

          ( sup (( Proj (f,a)) .: X)) = ( sup (f .: [:Y9, X9:])) by Th15

          .= (f . ( sup [:Y9, X9:])) by A8, A4

          .= (f . (( sup Y9),( sup X9))) by A7, A6, YELLOW_3: 43

          .= (( Proj (f,a)) . ( sup X)) by A3, Th7;

          hence thesis by A8, A4, A5;

        end;

        hence thesis;

      end;

      for X be Subset of R st X is non empty directed holds ( Proj (f,b)) preserves_sup_of X

      proof

        reconsider Y9 = {b} as non empty directed Subset of S by WAYBEL_0: 5;

        let X be Subset of R;

        assume X is non empty directed;

        then

        reconsider X9 = X as non empty directed Subset of R;

        ( Proj (f,b)) preserves_sup_of X

        proof

          

           A9: ( sup Y9) = b by YELLOW_0: 39;

          

           A10: f preserves_sup_of [:X9, Y9:] by A1;

          

           A11: (( Proj (f,b)) .: X) = (f .: [:X9, Y9:]) by Th14;

          

           A12: ex_sup_of (Y9,S) by YELLOW_0: 38;

          assume

           A13: ex_sup_of (X,R);

          then

           A14: ex_sup_of ( [:X9, Y9:], [:R, S:]) by A12, YELLOW_3: 39;

          ( sup (( Proj (f,b)) .: X)) = ( sup (f .: [:X9, Y9:])) by Th14

          .= (f . ( sup [:X9, Y9:])) by A14, A10

          .= (f . (( sup X9),( sup Y9))) by A13, A12, YELLOW_3: 43

          .= (( Proj (f,b)) . ( sup X)) by A9, Th8;

          hence thesis by A14, A10, A11;

        end;

        hence thesis;

      end;

      hence thesis by A2;

    end;

    theorem :: WAYBEL24:17

    

     Th17: for R,S,T be LATTICE, f be monotone Function of [:R, S:], T, a be Element of R, b be Element of S, X be directed Subset of [:R, S:] st ex_sup_of ((f .: X),T) & a in ( proj1 X) & b in ( proj2 X) holds (f . [a, b]) <= ( sup (f .: X))

    proof

      let R,S,T be LATTICE, f be monotone Function of [:R, S:], T, a be Element of R, b be Element of S, X be directed Subset of [:R, S:];

      assume that

       A1: ex_sup_of ((f .: X),T) and

       A2: a in ( proj1 X) and

       A3: b in ( proj2 X);

      consider d be object such that

       A4: [d, b] in X by A3, XTUPLE_0:def 13;

      d in ( proj1 X) by A4, XTUPLE_0:def 12;

      then

      reconsider d as Element of R;

      consider c be object such that

       A5: [a, c] in X by A2, XTUPLE_0:def 12;

      c in ( proj2 X) by A5, XTUPLE_0:def 13;

      then

      reconsider c as Element of S;

      consider z be Element of [:R, S:] such that

       A6: z in X and

       A7: [a, c] <= z & [d, b] <= z by A5, A4, WAYBEL_0:def 1;

      

       A8: (f .: X) is_<=_than ( sup (f .: X)) by A1, YELLOW_0: 30;

      ( [a, c] "\/" [d, b]) <= (z "\/" z) by A7, YELLOW_3: 3;

      then ( [a, c] "\/" [d, b]) <= z by YELLOW_5: 1;

      then [(a "\/" d), (c "\/" b)] <= z by YELLOW10: 16;

      then

       A9: (f . [(a "\/" d), (c "\/" b)]) <= (f . z) by WAYBEL_1:def 2;

      ( dom f) = the carrier of [:R, S:] by FUNCT_2:def 1;

      then (f . z) in (f .: X) by A6, FUNCT_1:def 6;

      then

       A10: (f . z) <= ( sup (f .: X)) by A8;

      a <= (a "\/" d) & b <= (c "\/" b) by YELLOW_0: 22;

      then [a, b] <= [(a "\/" d), (c "\/" b)] by YELLOW_3: 11;

      then (f . [a, b]) <= (f . [(a "\/" d), (c "\/" b)]) by WAYBEL_1:def 2;

      then (f . [a, b]) <= (f . z) by A9, YELLOW_0:def 2;

      hence thesis by A10, YELLOW_0:def 2;

    end;

    theorem :: WAYBEL24:18

    for R,S,T be complete LATTICE, f be Function of [:R, S:], T st (for a be Element of R, b be Element of S holds ( Proj (f,a)) is directed-sups-preserving & ( Proj (f,b)) is directed-sups-preserving) holds f is directed-sups-preserving

    proof

      let R,S,T be complete LATTICE, f be Function of [:R, S:], T;

      assume

       A1: for a be Element of R, b be Element of S holds ( Proj (f,a)) is directed-sups-preserving & ( Proj (f,b)) is directed-sups-preserving;

      for X be Subset of [:R, S:] st X is non empty directed holds f preserves_sup_of X

      proof

        let X be Subset of [:R, S:];

        assume X is non empty directed;

        then

        reconsider X as non empty directed Subset of [:R, S:];

        for a be Element of R, b be Element of S holds ( Proj (f,a)) is monotone & ( Proj (f,b)) is monotone by A1, WAYBEL17: 3;

        then

         A2: f is monotone by Th12;

        f preserves_sup_of X

        proof

          ( proj1 X) is directed non empty & ( Proj (f,( "\/" (( proj2 X),S)))) is directed-sups-preserving by A1, YELLOW_3: 21, YELLOW_3: 22;

          then

           A3: ( Proj (f,( "\/" (( proj2 X),S)))) preserves_sup_of ( proj1 X);

          

           A4: ex_sup_of ((( Proj (f,( sup ( proj2 X)))) .: ( proj1 X)),T) by YELLOW_0: 17;

          assume

           A5: ex_sup_of (X, [:R, S:]);

          then

           A6: ex_sup_of (( proj1 X),R) by YELLOW_3: 41;

          

           A7: ex_sup_of (( proj2 X),S) by A5, YELLOW_3: 41;

          for b be Element of T st b in (( Proj (f,( sup ( proj2 X)))) .: ( proj1 X)) holds b <= ( sup (f .: X))

          proof

            let b be Element of T;

            assume b in (( Proj (f,( sup ( proj2 X)))) .: ( proj1 X));

            then

            consider b1 be object such that

             A8: b1 in ( dom ( Proj (f,( sup ( proj2 X))))) and

             A9: b1 in ( proj1 X) and

             A10: b = (( Proj (f,( sup ( proj2 X)))) . b1) by FUNCT_1:def 6;

            reconsider b1 as Element of R by A8;

            

             A11: (( Proj (f,b1)) .: ( proj2 X)) is_<=_than ( sup (f .: X))

            proof

              let k be Element of T;

              assume k in (( Proj (f,b1)) .: ( proj2 X));

              then

              consider k1 be object such that

               A12: k1 in ( dom ( Proj (f,b1))) and

               A13: k1 in ( proj2 X) and

               A14: k = (( Proj (f,b1)) . k1) by FUNCT_1:def 6;

              reconsider k1 as Element of S by A12;

              k = (f . (b1,k1)) by A14, Th7;

              hence thesis by A2, A9, A13, Th17, YELLOW_0: 17;

            end;

            ( proj2 X) is non empty directed & ( Proj (f,b1)) is directed-sups-preserving by A1, YELLOW_3: 21, YELLOW_3: 22;

            then

             A15: ( Proj (f,b1)) preserves_sup_of ( proj2 X);

            

             A16: ex_sup_of ((( Proj (f,b1)) .: ( proj2 X)),T) by YELLOW_0: 17;

            b = (( Proj (f,b1)) . ( sup ( proj2 X))) by A10, Th9

            .= ( sup (( Proj (f,b1)) .: ( proj2 X))) by A7, A15;

            hence thesis by A16, A11, YELLOW_0:def 9;

          end;

          then

           A17: (( Proj (f,( sup ( proj2 X)))) .: ( proj1 X)) is_<=_than ( sup (f .: X));

          

           A18: ( sup (f .: X)) <= (f . ( sup X)) by A2, WAYBEL17: 16;

          (f . ( sup X)) = (f . (( sup ( proj1 X)),( sup ( proj2 X)))) by YELLOW_3: 46

          .= (( Proj (f,( sup ( proj2 X)))) . ( sup ( proj1 X))) by Th8

          .= ( sup (( Proj (f,( sup ( proj2 X)))) .: ( proj1 X))) by A6, A3;

          then (f . ( sup X)) <= ( sup (f .: X)) by A17, A4, YELLOW_0:def 9;

          hence thesis by A18, YELLOW_0: 17, YELLOW_0:def 3;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL24:19

    

     Th19: for S be set, T be non empty RelStr, f be set holds f is Element of (T |^ S) iff f is Function of S, the carrier of T

    proof

      let S be set, T be non empty RelStr, f be set;

      hereby

        assume f is Element of (T |^ S);

        then f in the carrier of (T |^ S);

        then f in ( Funcs (S,the carrier of T)) by YELLOW_1: 28;

        then ex a be Function st a = f & ( dom a) = S & ( rng a) c= the carrier of T by FUNCT_2:def 2;

        hence f is Function of S, the carrier of T by FUNCT_2:def 1, RELSET_1: 4;

      end;

      assume f is Function of S, the carrier of T;

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

      hence thesis by YELLOW_1: 28;

    end;

    begin

    definition

      let S be TopStruct, T be non empty TopRelStr;

      :: WAYBEL24:def3

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

      : Def3: it is full SubRelStr of (T |^ the carrier of S) & for x be set holds x in the carrier of it iff ex f be Function of S, T st x = f & f is continuous;

      existence

      proof

        defpred P[ object] means ex f be Function of S, T st $1 = f & f is continuous;

        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;

        hereby

          assume f in the carrier of SX;

          then f in X by YELLOW_0:def 15;

          then

          consider f9 be Function of S, T such that

           A2: f9 = f & f9 is continuous by A1;

          take f9;

          thus f9 = f & f9 is continuous by A2;

        end;

        given f9 be Function of S, T such that

         A3: f = f9 and

         A4: f9 is continuous;

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

        then f in the carrier of (T |^ the carrier of S) by YELLOW_1: 28;

        then f in X by A1, A3, A4;

        hence thesis by YELLOW_0:def 15;

      end;

      uniqueness

      proof

        let A1,A2 be strict RelStr;

        assume that

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

         A6: for x be set holds x in the carrier of A1 iff ex f be Function of S, T st x = f & f is continuous and

         A7: A2 is full SubRelStr of (T |^ the carrier of S) and

         A8: for x be set holds x in the carrier of A2 iff ex f be Function of S, T st x = f & f is continuous;

        the carrier of A1 = the carrier of A2

        proof

          hereby

            let x be object;

            assume x in the carrier of A1;

            then ex f be Function of S, T st x = f & f is continuous by A6;

            hence x in the carrier of A2 by A8;

          end;

          let x be object;

          assume x in the carrier of A2;

          then ex f be Function of S, T st x = f & f is continuous by A8;

          hence thesis by A6;

        end;

        hence thesis by A5, A7, YELLOW_0: 57;

      end;

    end

    registration

      let S be non empty TopSpace, T be non empty TopSpace-like TopRelStr;

      cluster ( ContMaps (S,T)) -> non empty;

      coherence

      proof

        set f = the continuous Function of S, T;

        f in the carrier of ( ContMaps (S,T)) by Def3;

        hence thesis;

      end;

    end

    registration

      let S be non empty TopSpace, T be non empty TopSpace-like TopRelStr;

      cluster ( ContMaps (S,T)) -> constituted-Functions;

      coherence

      proof

        let a be Element of ( ContMaps (S,T));

        ex a9 be Function of S, T st a9 = a & a9 is continuous by Def3;

        hence thesis;

      end;

    end

    theorem :: WAYBEL24:20

    

     Th20: for S be non empty TopSpace, T be non empty reflexive TopSpace-like TopRelStr, x,y be Element of ( ContMaps (S,T)) holds x <= y iff for i be Element of S holds [(x . i), (y . i)] in the InternalRel of T

    proof

      let S be non empty TopSpace, T be non empty reflexive TopSpace-like TopRelStr, x,y be Element of ( ContMaps (S,T));

      

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

      then

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

      reconsider xa = x9, ya = y9 as Function of S, T by Th19;

      hereby

        assume

         A2: x <= y;

        let i be Element of S;

        x9 <= y9 by A1, A2, YELLOW_0: 59;

        then xa <= ya by WAYBEL10: 11;

        then ex a,b be Element of T st a = (xa . i) & b = (ya . i) & a <= b by YELLOW_2:def 1;

        hence [(x . i), (y . i)] in the InternalRel of T;

      end;

      assume

       A3: for i be Element of S holds [(x . i), (y . i)] in the InternalRel of T;

      now

        let j be set;

        assume j in the carrier of S;

        then

        reconsider i = j as Element of S;

        reconsider a = (xa . i), b = (ya . i) as Element of T;

        take a, b;

        thus a = (xa . j) & b = (ya . j);

         [a, b] in the InternalRel of T by A3;

        hence a <= b;

      end;

      then xa <= ya by YELLOW_2:def 1;

      then x9 <= y9 by WAYBEL10: 11;

      hence thesis by A1, YELLOW_0: 60;

    end;

    theorem :: WAYBEL24:21

    

     Th21: for S be non empty TopSpace, T be non empty reflexive TopSpace-like TopRelStr, x be set holds x is continuous Function of S, T iff x is Element of ( ContMaps (S,T))

    proof

      let S be non empty TopSpace, T be non empty reflexive TopSpace-like TopRelStr, x be set;

      thus x is continuous Function of S, T implies x is Element of ( ContMaps (S,T)) by Def3;

      assume x is Element of ( ContMaps (S,T));

      then ex f be Function of S, T st x = f & f is continuous by Def3;

      hence thesis;

    end;

    registration

      let S be non empty TopSpace, T be non empty reflexive TopSpace-like TopRelStr;

      cluster ( ContMaps (S,T)) -> reflexive;

      coherence

      proof

        reconsider CS = ( ContMaps (S,T)) as full SubRelStr of (T |^ the carrier of S) by Def3;

        CS is reflexive;

        hence thesis;

      end;

    end

    registration

      let S be non empty TopSpace, T be non empty transitive TopSpace-like TopRelStr;

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

      coherence

      proof

        reconsider CS = ( ContMaps (S,T)) as full SubRelStr of (T |^ the carrier of S) by Def3;

        CS is transitive;

        hence thesis;

      end;

    end

    registration

      let S be non empty TopSpace, T be non empty antisymmetric TopSpace-like TopRelStr;

      cluster ( ContMaps (S,T)) -> antisymmetric;

      coherence

      proof

        reconsider CS = ( ContMaps (S,T)) as full SubRelStr of (T |^ the carrier of S) by Def3;

        CS is antisymmetric;

        hence thesis;

      end;

    end

    registration

      let S be set, T be non empty RelStr;

      cluster (T |^ S) -> constituted-Functions;

      coherence by Th19;

    end

    theorem :: WAYBEL24:22

    for S be non empty 1-sorted, T be complete LATTICE holds for f,g,h be Function of S, T, i be Element of S st h = ( "\/" ( {f, g},(T |^ the carrier of S))) holds (h . i) = ( sup {(f . i), (g . i)})

    proof

      let S be non empty 1-sorted, T be complete LATTICE;

      let f,g,h be Function of S, T, i be Element of S;

      reconsider f9 = f, g9 = g as Element of (T |^ the carrier of S) by Th19;

      reconsider SYT = (the carrier of S --> T) as non-Empty RelStr-yielding ManySortedSet of the carrier of S;

      reconsider SYT as non-Empty reflexive-yielding RelStr-yielding ManySortedSet of the carrier of S;

      

       A1: for i be Element of S holds (SYT . i) is complete LATTICE by FUNCOP_1: 7;

      reconsider f9, g9 as Element of ( product SYT) by YELLOW_1:def 5;

      reconsider DU = {f9, g9} as Subset of ( product SYT);

      assume h = ( "\/" ( {f, g},(T |^ the carrier of S)));

      

      then (h . i) = (( sup DU) . i) by YELLOW_1:def 5

      .= ( "\/" (( pi ( {f, g},i)),(SYT . i))) by A1, WAYBEL_3: 32

      .= ( "\/" (( pi ( {f, g},i)),T)) by FUNCOP_1: 7

      .= ( sup {(f . i), (g . i)}) by CARD_3: 15;

      hence thesis;

    end;

    theorem :: WAYBEL24:23

    

     Th23: for I be non empty set holds for J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i be Element of I holds (J . i) is complete LATTICE holds for X be Subset of ( product J), i be Element of I holds (( inf X) . i) = ( inf ( pi (X,i)))

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;

      assume

       A1: for i be Element of I holds (J . i) is complete LATTICE;

      then

      reconsider L = ( product J) as complete LATTICE by WAYBEL_3: 31;

      let X be Subset of ( product J), i be Element of I;

      

       A2: L is complete;

      then

       A3: ( inf X) is_<=_than X by YELLOW_0: 33;

      

       A4: (( inf X) . i) is_<=_than ( pi (X,i))

      proof

        let a be Element of (J . i);

        assume a in ( pi (X,i));

        then

        consider f be Function such that

         A5: f in X and

         A6: a = (f . i) by CARD_3:def 6;

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

        ( inf X) <= f by A3, A5;

        hence thesis by A6, WAYBEL_3: 28;

      end;

       A7:

      now

        let a be Element of (J . i);

        set f = (( inf X) +* (i,a));

        

         A8: ( dom f) = ( dom ( inf X)) by FUNCT_7: 30;

        

         A9: ( dom ( inf X)) = I by WAYBEL_3: 27;

        now

          let j be Element of I;

          j = i or j <> i;

          then (f . j) = (( inf X) . j) or (f . j) = a & j = i by A9, FUNCT_7: 31, FUNCT_7: 32;

          hence (f . j) is Element of (J . j);

        end;

        then

        reconsider f as Element of ( product J) by A8, WAYBEL_3: 27;

        assume

         A10: a is_<=_than ( pi (X,i));

        f is_<=_than X

        proof

          let g be Element of ( product J);

          assume g in X;

          then

           A11: g >= ( inf X) & (g . i) in ( pi (X,i)) by A2, CARD_3:def 6, YELLOW_2: 22;

          now

            let j be Element of I;

            j = i or j <> i;

            then (f . j) = (( inf X) . j) or (f . j) = a & j = i by A9, FUNCT_7: 31, FUNCT_7: 32;

            hence (f . j) <= (g . j) by A10, A11, WAYBEL_3: 28;

          end;

          hence f <= g by WAYBEL_3: 28;

        end;

        then

         A12: f <= ( inf X) by A2, YELLOW_0: 33;

        (f . i) = a by A9, FUNCT_7: 31;

        hence (( inf X) . i) >= a by A12, WAYBEL_3: 28;

      end;

      (J . i) is complete LATTICE by A1;

      hence thesis by A4, A7, YELLOW_0: 33;

    end;

    theorem :: WAYBEL24:24

    for S be non empty 1-sorted, T be complete LATTICE holds for f,g,h be Function of S, T, i be Element of S st h = ( "/\" ( {f, g},(T |^ the carrier of S))) holds (h . i) = ( inf {(f . i), (g . i)})

    proof

      let S be non empty 1-sorted, T be complete LATTICE;

      let f,g,h be Function of S, T, i be Element of S;

      reconsider f9 = f, g9 = g as Element of (T |^ the carrier of S) by Th19;

      reconsider SYT = (the carrier of S --> T) as non-Empty RelStr-yielding ManySortedSet of the carrier of S;

      reconsider SYT as non-Empty reflexive-yielding RelStr-yielding ManySortedSet of the carrier of S;

      

       A1: for i be Element of S holds (SYT . i) is complete LATTICE by FUNCOP_1: 7;

      reconsider f9, g9 as Element of ( product SYT) by YELLOW_1:def 5;

      reconsider DU = {f9, g9} as Subset of ( product SYT);

      assume h = ( "/\" ( {f, g},(T |^ the carrier of S)));

      

      then (h . i) = (( inf DU) . i) by YELLOW_1:def 5

      .= ( "/\" (( pi ( {f, g},i)),(SYT . i))) by A1, Th23

      .= ( "/\" (( pi ( {f, g},i)),T)) by FUNCOP_1: 7

      .= ( inf {(f . i), (g . i)}) by CARD_3: 15;

      hence thesis;

    end;

    theorem :: WAYBEL24:25

    

     Th25: for S be non empty RelStr, T be complete LATTICE holds for F be non empty Subset of (T |^ the carrier of S), i be Element of S holds (( sup F) . i) = ( "\/" ({ (f . i) where f be Element of (T |^ the carrier of S) : f in F },T))

    proof

      let S be non empty RelStr, T be complete LATTICE;

      let F be non empty Subset of (T |^ the carrier of S), i be Element of S;

      reconsider SYT = (the carrier of S --> T) as non-Empty RelStr-yielding ManySortedSet of the carrier of S;

      reconsider SYT as non-Empty reflexive-yielding RelStr-yielding ManySortedSet of the carrier of S;

      reconsider X = F as Subset of ( product SYT) by YELLOW_1:def 5;

      

       A1: ( pi (X,i)) = { (f . i) where f be Element of (T |^ the carrier of S) : f in F }

      proof

        thus ( pi (X,i)) c= { (f . i) where f be Element of (T |^ the carrier of S) : f in F }

        proof

          let a be object;

          assume a in ( pi (X,i));

          then ex g be Function st g in X & a = (g . i) by CARD_3:def 6;

          hence thesis;

        end;

        thus { (f . i) where f be Element of (T |^ the carrier of S) : f in F } c= ( pi (X,i))

        proof

          let a be object;

          assume a in { (f . i) where f be Element of (T |^ the carrier of S) : f in F };

          then ex g be Element of (T |^ the carrier of S) st a = (g . i) & g in F;

          hence thesis by CARD_3:def 6;

        end;

      end;

      (T |^ the carrier of S) = ( product SYT) & for i be Element of S holds (SYT . i) is complete LATTICE by FUNCOP_1: 7, YELLOW_1:def 5;

      

      then (( sup F) . i) = ( "\/" (( pi (X,i)),(SYT . i))) by WAYBEL_3: 32

      .= ( "\/" ({ (f . i) where f be Element of (T |^ the carrier of S) : f in F },T)) by A1, FUNCOP_1: 7;

      hence thesis;

    end;

    theorem :: WAYBEL24:26

    

     Th26: for S,T be complete TopLattice holds for F be non empty Subset of ( ContMaps (S,T)), i be Element of S holds (( "\/" (F,(T |^ the carrier of S))) . i) = ( "\/" ({ (f . i) where f be Element of (T |^ the carrier of S) : f in F },T))

    proof

      let S,T be complete TopLattice;

      let F be non empty Subset of ( ContMaps (S,T)), i be Element of S;

      reconsider SYT = (the carrier of S --> T) as non-Empty RelStr-yielding ManySortedSet of the carrier of S;

      reconsider SYT as non-Empty reflexive-yielding RelStr-yielding ManySortedSet of the carrier of S;

      ( ContMaps (S,T)) is full SubRelStr of (T |^ the carrier of S) by Def3;

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

      then

       A1: F c= the carrier of (T |^ the carrier of S);

      then

      reconsider X = F as Subset of ( product SYT) by YELLOW_1:def 5;

      

       A2: ( pi (X,i)) = { (f . i) where f be Element of (T |^ the carrier of S) : f in F }

      proof

        thus ( pi (X,i)) c= { (f . i) where f be Element of (T |^ the carrier of S) : f in F }

        proof

          let a be object;

          assume a in ( pi (X,i));

          then ex g be Function st g in X & a = (g . i) by CARD_3:def 6;

          hence thesis by A1;

        end;

        thus { (f . i) where f be Element of (T |^ the carrier of S) : f in F } c= ( pi (X,i))

        proof

          let a be object;

          assume a in { (f . i) where f be Element of (T |^ the carrier of S) : f in F };

          then ex g be Element of (T |^ the carrier of S) st a = (g . i) & g in F;

          hence thesis by CARD_3:def 6;

        end;

      end;

      (T |^ the carrier of S) = ( product SYT) & for i be Element of S holds (SYT . i) is complete LATTICE by FUNCOP_1: 7, YELLOW_1:def 5;

      

      then (( "\/" (F,(T |^ the carrier of S))) . i) = ( "\/" (( pi (X,i)),(SYT . i))) by WAYBEL_3: 32

      .= ( "\/" ({ (f . i) where f be Element of (T |^ the carrier of S) : f in F },T)) by A2, FUNCOP_1: 7;

      hence thesis;

    end;

    reserve S for non empty RelStr,

T for complete LATTICE;

    theorem :: WAYBEL24:27

    

     Th27: for F be non empty Subset of (T |^ the carrier of S), D be non empty Subset of S holds (( sup F) .: D) = { ( "\/" ({ (f . i) where f be Element of (T |^ the carrier of S) : f in F },T)) where i be Element of S : i in D }

    proof

      let F be non empty Subset of (T |^ the carrier of S), D be non empty Subset of S;

      thus (( sup F) .: D) c= { ( "\/" ({ (f . i) where f be Element of (T |^ the carrier of S) : f in F },T)) where i be Element of S : i in D }

      proof

        let a be object;

        assume a in (( sup F) .: D);

        then

        consider x be object such that x in ( dom ( sup F)) and

         A1: x in D and

         A2: a = (( sup F) . x) by FUNCT_1:def 6;

        reconsider x9 = x as Element of S by A1;

        a = ( "\/" ({ (f . x9) where f be Element of (T |^ the carrier of S) : f in F },T)) by A2, Th25;

        hence thesis by A1;

      end;

      thus { ( "\/" ({ (f . i) where f be Element of (T |^ the carrier of S) : f in F },T)) where i be Element of S : i in D } c= (( sup F) .: D)

      proof

        ( sup F) is Function of S, T by Th6;

        then

         A3: ( dom ( sup F)) = the carrier of S by FUNCT_2:def 1;

        let a be object;

        assume a in { ( "\/" ({ (f . i) where f be Element of (T |^ the carrier of S) : f in F },T)) where i be Element of S : i in D };

        then

        consider i1 be Element of S such that

         A4: a = ( "\/" ({ (f . i1) where f be Element of (T |^ the carrier of S) : f in F },T)) & i1 in D;

        a = (( sup F) . i1) by A4, Th25;

        hence thesis by A4, A3, FUNCT_1:def 6;

      end;

    end;

    theorem :: WAYBEL24:28

    

     Th28: for S,T be complete Scott TopLattice, F be non empty Subset of ( ContMaps (S,T)), D be non empty Subset of S holds (( "\/" (F,(T |^ the carrier of S))) .: D) = { ( "\/" ({ (f . i) where f be Element of (T |^ the carrier of S) : f in F },T)) where i be Element of S : i in D }

    proof

      let S,T be complete Scott TopLattice, F be non empty Subset of ( ContMaps (S,T)), D be non empty Subset of S;

      thus (( "\/" (F,(T |^ the carrier of S))) .: D) c= { ( "\/" ({ (f . i) where f be Element of (T |^ the carrier of S) : f in F },T)) where i be Element of S : i in D }

      proof

        let a be object;

        assume a in (( "\/" (F,(T |^ the carrier of S))) .: D);

        then

        consider x be object such that x in ( dom ( "\/" (F,(T |^ the carrier of S)))) and

         A1: x in D and

         A2: a = (( "\/" (F,(T |^ the carrier of S))) . x) by FUNCT_1:def 6;

        reconsider x9 = x as Element of S by A1;

        a = ( "\/" ({ (f . x9) where f be Element of (T |^ the carrier of S) : f in F },T)) by A2, Th26;

        hence thesis by A1;

      end;

      thus { ( "\/" ({ (f . i) where f be Element of (T |^ the carrier of S) : f in F },T)) where i be Element of S : i in D } c= (( "\/" (F,(T |^ the carrier of S))) .: D)

      proof

        ( "\/" (F,(T |^ the carrier of S))) is Function of S, T by Th19;

        then

         A3: ( dom ( "\/" (F,(T |^ the carrier of S)))) = the carrier of S by FUNCT_2:def 1;

        let a be object;

        assume a in { ( "\/" ({ (f . i) where f be Element of (T |^ the carrier of S) : f in F },T)) where i be Element of S : i in D };

        then

        consider i1 be Element of S such that

         A4: a = ( "\/" ({ (f . i1) where f be Element of (T |^ the carrier of S) : f in F },T)) & i1 in D;

        a = (( "\/" (F,(T |^ the carrier of S))) . i1) by A4, Th26;

        hence thesis by A4, A3, FUNCT_1:def 6;

      end;

    end;

    scheme :: WAYBEL24:sch3

    FraenkelF9RS { B() -> non empty TopRelStr , F( set) -> set , G( set) -> set , P[ set] } :

{ F(v1) where v1 be Element of B() : P[v1] } = { G(v2) where v2 be Element of B() : P[v2] }

      provided

       A1: for v be Element of B() st P[v] holds F(v) = G(v);

      set X = { F(v1) where v1 be Element of B() : P[v1] }, Y = { G(v2) where v2 be Element of B() : P[v2] };

      

       A2: Y c= X

      proof

        let x be object;

        assume x in Y;

        then

        consider v1 be Element of B() such that

         A3: x = G(v1) and

         A4: P[v1];

        x = F(v1) by A1, A3, A4;

        hence thesis by A4;

      end;

      X c= Y

      proof

        let x be object;

        assume x in X;

        then

        consider v1 be Element of B() such that

         A5: x = F(v1) and

         A6: P[v1];

        x = G(v1) by A1, A5, A6;

        hence thesis by A6;

      end;

      hence thesis by A2;

    end;

    scheme :: WAYBEL24:sch4

    FraenkelF9RSS { B() -> non empty RelStr , F( set) -> set , G( set) -> set , P[ set] } :

{ F(v1) where v1 be Element of B() : P[v1] } = { G(v2) where v2 be Element of B() : P[v2] }

      provided

       A1: for v be Element of B() st P[v] holds F(v) = G(v);

      set X = { F(v1) where v1 be Element of B() : P[v1] }, Y = { G(v2) where v2 be Element of B() : P[v2] };

      

       A2: Y c= X

      proof

        let x be object;

        assume x in Y;

        then

        consider v1 be Element of B() such that

         A3: x = G(v1) and

         A4: P[v1];

        x = F(v1) by A1, A3, A4;

        hence thesis by A4;

      end;

      X c= Y

      proof

        let x be object;

        assume x in X;

        then

        consider v1 be Element of B() such that

         A5: x = F(v1) and

         A6: P[v1];

        x = G(v1) by A1, A5, A6;

        hence thesis by A6;

      end;

      hence thesis by A2;

    end;

    scheme :: WAYBEL24:sch5

    FuncFraenkelS { B,C() -> non empty TopRelStr , A( set) -> Element of C() , f() -> Function , P[ set] } :

(f() .: { A(x) where x be Element of B() : P[x] }) = { (f() . A(x)) where x be Element of B() : P[x] }

      provided

       A1: the carrier of C() c= ( dom f());

      set f = f();

      thus (f .: { A(x) where x be Element of B() : P[x] }) c= { (f . A(x)) where x be Element of B() : P[x] }

      proof

        let y be object;

        assume y in (f .: { A(x) where x be Element of B() : P[x] });

        then

        consider z be object such that z in ( dom f) and

         A2: z in { A(x) where x be Element of B() : P[x] } and

         A3: y = (f . z) by FUNCT_1:def 6;

        ex x be Element of B() st z = A(x) & P[x] by A2;

        hence thesis by A3;

      end;

      let y be object;

      assume y in { (f . A(x)) where x be Element of B() : P[x] };

      then

      consider x be Element of B() such that

       A4: y = (f . A(x)) and

       A5: P[x];

      A(x) in the carrier of C() & A(x) in { A(z) where z be Element of B() : P[z] } by A5;

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

    end;

    

     Lm1: for S be non empty RelStr, D be non empty Subset of S holds D = { i where i be Element of S : i in D }

    proof

      let S be non empty RelStr, D be non empty Subset of S;

      thus D c= { i where i be Element of S : i in D };

      thus { i where i be Element of S : i in D } c= D

      proof

        let a be object;

        assume a in { i where i be Element of S : i in D };

        then ex j be Element of S st j = a & j in D;

        hence thesis;

      end;

    end;

    theorem :: WAYBEL24:29

    

     Th29: for S,T be complete Scott TopLattice, F be non empty Subset of ( ContMaps (S,T)) holds ( "\/" (F,(T |^ the carrier of S))) is monotone Function of S, T

    proof

      let S,T be complete Scott TopLattice, F be non empty Subset of ( ContMaps (S,T));

      ( ContMaps (S,T)) is full SubRelStr of (T |^ the carrier of S) by Def3;

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

      then

      reconsider F9 = F as Subset of (T |^ the carrier of S) by XBOOLE_1: 1;

      reconsider sF = ( sup F9) as Function of S, T by Th6;

      now

        let x,y be Element of S;

        set G1 = { (f . x) where f be Element of (T |^ the carrier of S) : f in F9 };

        assume

         A1: x <= y;

        

         A2: G1 is_<=_than (sF . y)

        proof

          let a be Element of T;

          assume a in { (f . x) where f be Element of (T |^ the carrier of S) : f in F9 };

          then

          consider f9 be Element of (T |^ the carrier of S) such that

           A3: a = (f9 . x) and

           A4: f9 in F9;

          reconsider f1 = f9 as continuous Function of S, T by A4, Th21;

          reconsider f1 as monotone Function of S, T;

          f9 <= ( sup F9) by A4, YELLOW_2: 22;

          then f1 <= sF by WAYBEL10: 11;

          then

           A5: (f1 . y) <= (sF . y) by YELLOW_2: 9;

          (f1 . x) <= (f1 . y) by A1, WAYBEL_1:def 2;

          hence thesis by A3, A5, YELLOW_0:def 2;

        end;

        (sF . x) = ( "\/" (G1,T)) by Th25;

        hence (sF . x) <= (sF . y) by A2, YELLOW_0: 32;

      end;

      hence thesis by WAYBEL_1:def 2;

    end;

    theorem :: WAYBEL24:30

    

     Th30: for S,T be complete Scott TopLattice, F be non empty Subset of ( ContMaps (S,T)), D be directed non empty Subset of S holds ( "\/" ({ ( "\/" ({ (g . i) where i be Element of S : i in D },T)) where g be Element of (T |^ the carrier of S) : g in F },T)) = ( "\/" ({ ( "\/" ({ (g9 . i9) where g9 be Element of (T |^ the carrier of S) : g9 in F },T)) where i9 be Element of S : i9 in D },T))

    proof

      let S,T be complete Scott TopLattice, F be non empty Subset of ( ContMaps (S,T)), D be directed non empty Subset of S;

      reconsider sF = ( "\/" (F,(T |^ the carrier of S))) as Function of S, T by Th19;

      set F9 = F;

      set L = ( "\/" ({ ( "\/" ({ (g . i) where i be Element of S : i in D },T)) where g be Element of (T |^ the carrier of S) : g in F },T));

      set P = ( "\/" ({ ( "\/" ({ (g9 . i9) where g9 be Element of (T |^ the carrier of S) : g9 in F },T)) where i9 be Element of S : i9 in D },T));

      set L1 = { ( "\/" ({ (g . i) where i be Element of S : i in D },T)) where g be Element of (T |^ the carrier of S) : g in F };

      set P1 = { ( "\/" ({ (g2 . i3) where g2 be Element of (T |^ the carrier of S) : g2 in F },T)) where i3 be Element of S : i3 in D };

      reconsider L, P as Element of T;

      defpred Q[ set] means $1 in F9;

      deffunc A( Element of S) = $1;

      defpred P[ set] means $1 in D;

      deffunc F( Element of (T |^ the carrier of S)) = ( "\/" ({ ($1 . i4) where i4 be Element of S : i4 in D },T));

      deffunc G( Element of (T |^ the carrier of S)) = ($1 . ( sup D));

      

       A1: P = ( sup (sF .: D)) by Th28;

      L1 is_<=_than P

      proof

        let b be Element of T;

        assume b in L1;

        then

        consider g9 be Element of (T |^ the carrier of S) such that

         A2: b = ( "\/" ({ (g9 . i) where i be Element of S : i in D },T)) and

         A3: g9 in F;

        reconsider g1 = g9 as continuous Function of S, T by A3, Th21;

        g9 <= ( "\/" (F,(T |^ the carrier of S))) by A3, YELLOW_2: 22;

        then

         A4: g1 <= sF by WAYBEL10: 11;

        

         A5: (g1 .: D) is_<=_than ( sup (sF .: D))

        proof

          let a be Element of T;

          assume a in (g1 .: D);

          then

          consider x be object such that

           A6: x in ( dom g1) and

           A7: x in D and

           A8: a = (g1 . x) by FUNCT_1:def 6;

          reconsider x9 = x as Element of S by A6;

          x in the carrier of S by A6;

          then x9 in ( dom sF) by FUNCT_2:def 1;

          then (sF . x9) in (sF .: D) by A7, FUNCT_1:def 6;

          then

           A9: (sF . x9) <= ( sup (sF .: D)) by YELLOW_2: 22;

          (g1 . x9) <= (sF . x9) by A4, YELLOW_2: 9;

          hence thesis by A8, A9, YELLOW_0:def 2;

        end;

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

        then

         A10: the carrier of S c= ( dom g9);

        (g9 .: { A(i2) where i2 be Element of S : P[i2] }) = { (g9 . A(i)) where i be Element of S : P[i] } from FuncFraenkelS( A10);

        then b = ( "\/" ((g9 .: D),T)) by A2, Lm1;

        hence thesis by A1, A5, YELLOW_0: 32;

      end;

      then

       A11: L <= P by YELLOW_0: 32;

      

       A12: for g8 be Element of (T |^ the carrier of S) st Q[g8] holds F(g8) = G(g8)

      proof

        let g1 be Element of (T |^ the carrier of S);

        assume g1 in F9;

        then

        reconsider g9 = g1 as continuous Function of S, T by Th21;

        

         A13: g9 preserves_sup_of D & ex_sup_of (D,S) by WAYBEL_0:def 37, YELLOW_0: 17;

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

        then

         A14: the carrier of S c= ( dom g1);

        (g1 .: { A(i2) where i2 be Element of S : P[i2] }) = { (g1 . A(i)) where i be Element of S : P[i] } from FuncFraenkelS( A14);

        

        then ( "\/" ({ (g1 . i) where i be Element of S : i in D },T)) = ( sup (g9 .: D)) by Lm1

        .= (g1 . ( sup D)) by A13;

        hence thesis;

      end;

      { F(g3) where g3 be Element of (T |^ the carrier of S) : Q[g3] } = { G(g4) where g4 be Element of (T |^ the carrier of S) : Q[g4] } from FraenkelF9RSS( A12);

      then

       A15: L = (sF . ( sup D)) by Th26;

      P1 is_<=_than L

      proof

        let b be Element of T;

        assume b in P1;

        then

        consider i9 be Element of S such that

         A16: b = ( "\/" ({ (g9 . i9) where g9 be Element of (T |^ the carrier of S) : g9 in F },T)) and

         A17: i9 in D;

        i9 in the carrier of S;

        then

         A18: i9 in ( dom sF) by FUNCT_2:def 1;

        b = (sF . i9) by A16, Th26;

        then b in (sF .: D) by A17, A18, FUNCT_1:def 6;

        then

         A19: b <= ( sup (sF .: D)) by YELLOW_2: 22;

        sF is monotone by Th29;

        then ( sup (sF .: D)) <= L by A15, WAYBEL17: 15;

        hence thesis by A19, YELLOW_0:def 2;

      end;

      then P <= L by YELLOW_0: 32;

      hence thesis by A11, YELLOW_0:def 3;

    end;

    theorem :: WAYBEL24:31

    

     Th31: for S,T be complete Scott TopLattice, F be non empty Subset of ( ContMaps (S,T)), D be directed non empty Subset of S holds ( "\/" ((( "\/" (F,(T |^ the carrier of S))) .: D),T)) = (( "\/" (F,(T |^ the carrier of S))) . ( sup D))

    proof

      let S,T be complete Scott TopLattice, F be non empty Subset of ( ContMaps (S,T)), D be directed non empty Subset of S;

      ( ContMaps (S,T)) is full SubRelStr of (T |^ the carrier of S) by Def3;

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

      then

      reconsider F9 = F as non empty Subset of (T |^ the carrier of S) by XBOOLE_1: 1;

      reconsider sF = ( sup F9) as Function of S, T by Th19;

      set L = ( "\/" ({ ( "\/" ({ (g . i) where i be Element of S : i in D },T)) where g be Element of (T |^ the carrier of S) : g in F },T));

      set P = ( "\/" ({ ( "\/" ({ (g9 . i9) where g9 be Element of (T |^ the carrier of S) : g9 in F },T)) where i9 be Element of S : i9 in D },T));

      deffunc F( Element of (T |^ the carrier of S)) = ( "\/" ({ ($1 . i4) where i4 be Element of S : i4 in D },T));

      deffunc G( Element of (T |^ the carrier of S)) = ($1 . ( sup D));

      defpred Q[ set] means $1 in F9;

      

       A1: for g8 be Element of (T |^ the carrier of S) st Q[g8] holds F(g8) = G(g8)

      proof

        deffunc A( Element of S) = $1;

        let g1 be Element of (T |^ the carrier of S);

        assume g1 in F9;

        then

        reconsider g9 = g1 as continuous Function of S, T by Th21;

        defpred P[ set] means $1 in D;

        

         A2: g9 preserves_sup_of D & ex_sup_of (D,S) by WAYBEL_0:def 37, YELLOW_0: 17;

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

        then

         A3: the carrier of S c= ( dom g1);

        (g1 .: { A(i2) where i2 be Element of S : P[i2] }) = { (g1 . A(i)) where i be Element of S : P[i] } from FuncFraenkelS( A3);

        

        then ( "\/" ({ (g1 . i) where i be Element of S : i in D },T)) = ( sup (g9 .: D)) by Lm1

        .= (g1 . ( sup D)) by A2;

        hence thesis;

      end;

      { F(g3) where g3 be Element of (T |^ the carrier of S) : Q[g3] } = { G(g4) where g4 be Element of (T |^ the carrier of S) : Q[g4] } from FraenkelF9RSS( A1);

      then

       A4: L = (sF . ( sup D)) by Th25;

      P = ( sup (sF .: D)) by Th27;

      hence thesis by A4, Th30;

    end;

    theorem :: WAYBEL24:32

    

     Th32: for S,T be complete Scott TopLattice, F be non empty Subset of ( ContMaps (S,T)) holds ( "\/" (F,(T |^ the carrier of S))) in the carrier of ( ContMaps (S,T))

    proof

      let S,T be complete Scott TopLattice, F be non empty Subset of ( ContMaps (S,T));

      reconsider Ex = ( "\/" (F,(T |^ the carrier of S))) as Function of S, T by Th19;

      for X be Subset of S st X is non empty directed holds Ex preserves_sup_of X by YELLOW_0: 17, Th31;

      then Ex is directed-sups-preserving;

      hence thesis by Def3;

    end;

    theorem :: WAYBEL24:33

    

     Th33: for S be non empty RelStr, T be lower-bounded antisymmetric non empty RelStr holds ( Bottom (T |^ the carrier of S)) = (S --> ( Bottom T))

    proof

      let S be non empty RelStr, T be lower-bounded antisymmetric non empty RelStr;

      set L = (T |^ the carrier of S);

      reconsider f = (S --> ( Bottom T)) as Element of L by Th19;

      reconsider f9 = f as Function of S, T;

      

       A1: for b be Element of L st b is_>=_than {} holds f <= b

      proof

        let b be Element of L;

        reconsider b9 = b as Function of S, T by Th19;

        assume b is_>=_than {} ;

        for x be Element of S holds (f9 . x) <= (b9 . x)

        proof

          let x be Element of S;

          (f9 . x) = ((the carrier of S --> ( Bottom T)) . x)

          .= ( Bottom T) by FUNCOP_1: 7;

          hence thesis by YELLOW_0: 44;

        end;

        then f9 <= b9 by YELLOW_2: 9;

        hence thesis by WAYBEL10: 11;

      end;

      f is_>=_than {} ;

      then f = ( "\/" ( {} ,L)) by A1, YELLOW_0: 30;

      hence thesis by YELLOW_0:def 11;

    end;

    theorem :: WAYBEL24:34

    for S be non empty RelStr, T be upper-bounded antisymmetric non empty RelStr holds ( Top (T |^ the carrier of S)) = (S --> ( Top T))

    proof

      let S be non empty RelStr, T be upper-bounded antisymmetric non empty RelStr;

      set L = (T |^ the carrier of S);

      reconsider f = (S --> ( Top T)) as Element of L by Th19;

      reconsider f9 = f as Function of S, T;

      

       A1: for b be Element of L st b is_<=_than {} holds f >= b

      proof

        let b be Element of L;

        reconsider b9 = b as Function of S, T by Th19;

        assume b is_<=_than {} ;

        for x be Element of S holds (f9 . x) >= (b9 . x)

        proof

          let x be Element of S;

          (f9 . x) = ((the carrier of S --> ( Top T)) . x)

          .= ( Top T) by FUNCOP_1: 7;

          hence thesis by YELLOW_0: 45;

        end;

        then f9 >= b9 by YELLOW_2: 9;

        hence thesis by WAYBEL10: 11;

      end;

      f is_<=_than {} ;

      then f = ( "/\" ( {} ,L)) by A1, YELLOW_0: 31;

      hence thesis by YELLOW_0:def 12;

    end;

    registration

      let S be non empty reflexive RelStr, T be complete LATTICE, a be Element of T;

      cluster (S --> a) -> directed-sups-preserving;

      coherence

      proof

        set f = (S --> a);

        for X be Subset of S st X is non empty directed holds f preserves_sup_of X

        proof

          let X be Subset of S;

          assume X is non empty directed;

          then

          reconsider X9 = X as non empty directed Subset of S;

          f preserves_sup_of X

          proof

            assume ex_sup_of (X,S);

            thus ex_sup_of ((f .: X),T) by YELLOW_0: 17;

            

             A1: {a} c= (f .: X)

            proof

              set n = the Element of X9;

              let b be object;

              

               A2: a = ((the carrier of S --> a) . n) by FUNCOP_1: 7

              .= (f . n);

              assume b in {a};

              then

               A3: b = a by TARSKI:def 1;

              ( dom f) = the carrier of S by FUNCOP_1: 13;

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

            end;

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

            then (f .: X) c= {a} by FUNCOP_1: 8;

            

            hence ( sup (f .: X)) = ( sup {a}) by A1, XBOOLE_0:def 10

            .= a by YELLOW_0: 39

            .= ((the carrier of S --> a) . ( sup X)) by FUNCOP_1: 7

            .= (f . ( sup X));

          end;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: WAYBEL24:35

    

     Th35: for S,T be complete Scott TopLattice holds ( ContMaps (S,T)) is sups-inheriting SubRelStr of (T |^ the carrier of S)

    proof

      let S,T be complete Scott TopLattice;

      set L = (T |^ the carrier of S);

      reconsider CS = ( ContMaps (S,T)) as full SubRelStr of L by Def3;

      now

        let X be Subset of CS;

        assume ex_sup_of (X,L);

        per cases ;

          suppose X is non empty;

          hence ( "\/" (X,L)) in the carrier of CS by Th32;

        end;

          suppose X is empty;

          then ( "\/" (X,L)) = ( Bottom L) by YELLOW_0:def 11;

          then ( "\/" (X,L)) = (S --> ( Bottom T)) by Th33;

          hence ( "\/" (X,L)) in the carrier of CS by Def3;

        end;

      end;

      hence thesis by YELLOW_0:def 19;

    end;

    registration

      let S,T be complete Scott TopLattice;

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

      coherence

      proof

        ( ContMaps (S,T)) is sups-inheriting non empty full SubRelStr of (T |^ the carrier of S) by Def3, Th35;

        hence thesis by YELLOW_2: 31;

      end;

    end

    theorem :: WAYBEL24:36

    for S,T be non empty Scott complete TopLattice holds ( Bottom ( ContMaps (S,T))) = (S --> ( Bottom T))

    proof

      let S,T be non empty Scott complete TopLattice;

      set L = ( ContMaps (S,T));

      reconsider f = (S --> ( Bottom T)) as Element of L by Th21;

      reconsider f9 = f as Function of S, T;

      

       A1: for b be Element of L st b is_>=_than {} holds f <= b

      proof

        let b be Element of L;

        reconsider b9 = b as Function of S, T by Th21;

        assume b is_>=_than {} ;

        for i be Element of S holds [(f . i), (b . i)] in the InternalRel of T

        proof

          let i be Element of S;

          (f . i) = ((the carrier of S --> ( Bottom T)) . i)

          .= ( Bottom T) by FUNCOP_1: 7;

          then (f9 . i) <= (b9 . i) by YELLOW_0: 44;

          hence thesis;

        end;

        hence thesis by Th20;

      end;

      f is_>=_than {} ;

      then f = ( "\/" ( {} ,L)) by A1, YELLOW_0: 30;

      hence thesis by YELLOW_0:def 11;

    end;

    theorem :: WAYBEL24:37

    for S,T be non empty Scott complete TopLattice holds ( Top ( ContMaps (S,T))) = (S --> ( Top T))

    proof

      let S,T be non empty Scott complete TopLattice;

      set L = ( ContMaps (S,T));

      reconsider f = (S --> ( Top T)) as Element of L by Th21;

      reconsider f9 = f as Function of S, T;

      

       A1: for b be Element of L st b is_<=_than {} holds f >= b

      proof

        let b be Element of L;

        reconsider b9 = b as Function of S, T by Th21;

        assume b is_<=_than {} ;

        for i be Element of S holds [(b . i), (f . i)] in the InternalRel of T

        proof

          let i be Element of S;

          (f . i) = ((the carrier of S --> ( Top T)) . i)

          .= ( Top T) by FUNCOP_1: 7;

          then (f9 . i) >= (b9 . i) by YELLOW_0: 45;

          hence thesis;

        end;

        hence thesis by Th20;

      end;

      f is_<=_than {} ;

      then f = ( "/\" ( {} ,L)) by A1, YELLOW_0: 31;

      hence thesis by YELLOW_0:def 12;

    end;

    theorem :: WAYBEL24:38

    for S,T be Scott complete TopLattice holds ( SCMaps (S,T)) = ( ContMaps (S,T))

    proof

      let S,T be Scott complete TopLattice;

      reconsider Sm = ( ContMaps (S,T)) as full non empty SubRelStr of (T |^ the carrier of S) by Def3;

      reconsider SC = ( SCMaps (S,T)) as full non empty SubRelStr of (T |^ the carrier of S) by WAYBEL15: 1;

      

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

      

       A2: the carrier of SC c= the carrier of Sm

      proof

        let a be object;

        assume

         A3: a in the carrier of SC;

        then

        reconsider f = a as Function of S, T by A1, WAYBEL10: 9;

        f is continuous Function of S, T by A3, WAYBEL17:def 2;

        then a is Element of Sm by Th21;

        hence thesis;

      end;

      the carrier of Sm c= the carrier of SC

      proof

        let a be object;

        assume a in the carrier of Sm;

        then a is continuous Function of S, T by Th21;

        hence thesis by WAYBEL17:def 2;

      end;

      then the carrier of SC = the carrier of Sm by A2;

      hence thesis by YELLOW_0: 57;

    end;