waybel_5.miz



    begin

    reserve x,y,i for object,

L for up-complete Semilattice;

    

     Lm1: for L be continuous Semilattice holds for x be Element of L holds ( waybelow x) is Ideal of L & x <= ( sup ( waybelow x)) & for I be Ideal of L st x <= ( sup I) holds ( waybelow x) c= I

    proof

      let L be continuous Semilattice;

      let x be Element of L;

      thus ( waybelow x) is Ideal of L;

      thus x <= ( sup ( waybelow x)) by WAYBEL_3:def 5;

      thus for I be Ideal of L st x <= ( sup I) holds ( waybelow x) c= I

      proof

        let I be Ideal of L;

        assume

         A1: x <= ( sup I);

        ( waybelow x) c= I

        proof

          let y be object;

          assume y in ( waybelow x);

          then y in { y9 where y9 be Element of L : y9 << x } by WAYBEL_3:def 3;

          then ex y9 be Element of L st y = y9 & y9 << x;

          hence thesis by A1, WAYBEL_3: 20;

        end;

        hence thesis;

      end;

    end;

    

     Lm2: (for x be Element of L holds ( waybelow x) is Ideal of L & x <= ( sup ( waybelow x)) & for I be Ideal of L st x <= ( sup I) holds ( waybelow x) c= I) implies L is continuous

    proof

      assume

       A1: for x be Element of L holds ( waybelow x) is Ideal of L & x <= ( sup ( waybelow x)) & for I be Ideal of L st x <= ( sup I) holds ( waybelow x) c= I;

      now

        let x be Element of L;

        

         A2: x <= ( sup ( waybelow x)) by A1;

        ( waybelow x) is non empty directed by A1;

        then

         A3: ex_sup_of (( waybelow x),L) by WAYBEL_0: 75;

        ( waybelow x) is_<=_than x by WAYBEL_3: 9;

        then ( sup ( waybelow x)) <= x by A3, YELLOW_0:def 9;

        hence x = ( sup ( waybelow x)) by A2, YELLOW_0:def 3;

      end;

      then

       A4: L is satisfying_axiom_of_approximation by WAYBEL_3:def 5;

      for x be Element of L holds ( waybelow x) is non empty directed by A1;

      hence thesis by A4, WAYBEL_3:def 6;

    end;

    theorem :: WAYBEL_5:1

    L is continuous iff for x be Element of L holds ( waybelow x) is Ideal of L & x <= ( sup ( waybelow x)) & for I be Ideal of L st x <= ( sup I) holds ( waybelow x) c= I by Lm1, Lm2;

    

     Lm3: L is continuous implies for x be Element of L holds ex I be Ideal of L st x <= ( sup I) & for J be Ideal of L st x <= ( sup J) holds I c= J

    proof

      assume

       A1: L is continuous;

      let x be Element of L;

      reconsider I = ( waybelow x) as Ideal of L by A1;

      take I;

      thus thesis by A1, Lm1;

    end;

    

     Lm4: (for x be Element of L holds ex I be Ideal of L st x <= ( sup I) & for J be Ideal of L st x <= ( sup J) holds I c= J) implies L is continuous

    proof

      assume

       A1: for x be Element of L holds ex I be Ideal of L st x <= ( sup I) & for J be Ideal of L st x <= ( sup J) holds I c= J;

      now

        let x be Element of L;

        consider I be Ideal of L such that

         A2: x <= ( sup I) and

         A3: for J be Ideal of L st x <= ( sup J) holds I c= J by A1;

        now

          let y be object;

          assume

           A4: y in I;

          then

          reconsider y9 = y as Element of L;

          for J be Ideal of L st x <= ( sup J) holds y in J

          proof

            let J be Ideal of L;

            assume x <= ( sup J);

            then I c= J by A3;

            hence thesis by A4;

          end;

          then y9 << x by WAYBEL_3: 21;

          hence y in ( waybelow x) by WAYBEL_3: 7;

        end;

        then

         A5: I c= ( waybelow x);

        for y be object st y in ( waybelow x) holds y in I by A2, WAYBEL_3: 7, WAYBEL_3: 20;

        then ( waybelow x) c= I;

        then ( waybelow x) = I by A5, XBOOLE_0:def 10;

        hence ( waybelow x) is Ideal of L & x <= ( sup ( waybelow x)) & for I be Ideal of L st x <= ( sup I) holds ( waybelow x) c= I by A2, A3;

      end;

      hence thesis by Lm2;

    end;

    theorem :: WAYBEL_5:2

    L is continuous iff for x be Element of L holds ex I be Ideal of L st x <= ( sup I) & for J be Ideal of L st x <= ( sup J) holds I c= J by Lm3, Lm4;

    theorem :: WAYBEL_5:3

    for L be continuous lower-bounded sup-Semilattice holds ( SupMap L) is upper_adjoint

    proof

      let L be continuous lower-bounded sup-Semilattice;

      set P = ( InclPoset ( Ids L));

      set r = ( SupMap L);

      deffunc F( Element of L) = ( inf (r " ( uparrow {$1})));

      ex d be Function of L, ( InclPoset ( Ids L)) st for t be Element of L holds (d . t) = F(t) from FUNCT_2:sch 4;

      then

      consider d be Function of L, ( InclPoset ( Ids L)) such that

       A1: for t be Element of L holds (d . t) = ( inf (r " ( uparrow {t})));

      for t be Element of L holds (d . t) is_minimum_of (r " ( uparrow t))

      proof

        let t be Element of L;

        set I = ( inf (r " ( uparrow t)));

        reconsider I9 = I as Ideal of L by YELLOW_2: 41;

        

         A2: (d . t) = ( inf (r " ( uparrow {t}))) by A1

        .= I by WAYBEL_0:def 18;

        I in the carrier of P;

        then I in ( Ids L) by YELLOW_1: 1;

        then

         A3: I in ( dom r) by YELLOW_2: 49;

        consider J be Ideal of L such that

         A4: t <= ( sup J) and

         A5: for K be Ideal of L st t <= ( sup K) holds J c= K by Lm3;

        reconsider J9 = J as Element of P by YELLOW_2: 41;

        

         A6: for K be Element of P st (r " ( uparrow t)) is_>=_than K holds K <= J9

        proof

          J9 in the carrier of P;

          then J9 in ( Ids L) by YELLOW_1: 1;

          then

           A7: J in ( dom r) by YELLOW_2: 49;

          let K be Element of P;

          assume

           A8: (r " ( uparrow t)) is_>=_than K;

          t <= (r . J9) by A4, YELLOW_2:def 3;

          then (r . J) in ( uparrow t) by WAYBEL_0: 18;

          then J in (r " ( uparrow t)) by A7, FUNCT_1:def 7;

          hence thesis by A8;

        end;

        (r " ( uparrow t)) is_>=_than J9

        proof

          let K be Element of P;

          reconsider K9 = K as Ideal of L by YELLOW_2: 41;

          assume K in (r " ( uparrow t));

          then (r . K) in ( uparrow t) by FUNCT_1:def 7;

          then t <= (r . K) by WAYBEL_0: 18;

          then t <= ( sup K9) by YELLOW_2:def 3;

          then J9 c= K9 by A5;

          hence J9 <= K by YELLOW_1: 3;

        end;

        then t <= ( sup I9) by A4, A6, YELLOW_0: 31;

        then t <= (r . I) by YELLOW_2:def 3;

        then (r . I) in ( uparrow t) by WAYBEL_0: 18;

        then ex_inf_of ((r " ( uparrow t)),( InclPoset ( Ids L))) & I in (r " ( uparrow t)) by A3, FUNCT_1:def 7, YELLOW_0: 17;

        hence thesis by A2, WAYBEL_1:def 6;

      end;

      then [r, d] is Galois by WAYBEL_1: 10;

      hence thesis by WAYBEL_1:def 11;

    end;

    theorem :: WAYBEL_5:4

    for L be up-complete lower-bounded LATTICE holds ( SupMap L) is upper_adjoint implies L is continuous

    proof

      let L be up-complete lower-bounded LATTICE;

      set P = ( InclPoset ( Ids L));

      assume

       A1: ( SupMap L) is upper_adjoint;

      for x be Element of L holds ex I be Ideal of L st x <= ( sup I) & for J be Ideal of L st x <= ( sup J) holds I c= J

      proof

        set r = ( SupMap L);

        let x be Element of L;

        set I9 = ( inf (r " ( uparrow x)));

        reconsider I = I9 as Ideal of L by YELLOW_2: 41;

        

         A2: for J be Ideal of L st x <= ( sup J) holds I c= J

        proof

          let J be Ideal of L;

          reconsider J9 = J as Element of P by YELLOW_2: 41;

          assume x <= ( sup J);

          then x <= (r . J9) by YELLOW_2:def 3;

          then J in ( dom r) & (r . J9) in ( uparrow x) by WAYBEL_0: 18, YELLOW_2: 50;

          then J9 in (r " ( uparrow x)) by FUNCT_1:def 7;

          then I9 <= J9 by YELLOW_2: 22;

          hence thesis by YELLOW_1: 3;

        end;

        consider d be Function of L, P such that

         A3: [r, d] is Galois by A1, WAYBEL_1:def 11;

        (d . x) is_minimum_of (r " ( uparrow x)) by A3, WAYBEL_1: 10;

        then I in (r " ( uparrow x)) by WAYBEL_1:def 6;

        then (r . I) in ( uparrow x) by FUNCT_1:def 7;

        then x <= (r . I9) by WAYBEL_0: 18;

        then x <= ( sup I) by YELLOW_2:def 3;

        hence thesis by A2;

      end;

      hence thesis by Lm4;

    end;

    theorem :: WAYBEL_5:5

    for L be complete Semilattice holds ( SupMap L) is infs-preserving sups-preserving implies ( SupMap L) is upper_adjoint

    proof

      let L be complete Semilattice;

      set r = ( SupMap L);

      assume r is infs-preserving sups-preserving;

      then ex d be Function of L, ( InclPoset ( Ids L)) st [r, d] is Galois & for t be Element of L holds (d . t) is_minimum_of (r " ( uparrow t)) by WAYBEL_1: 14;

      hence thesis by WAYBEL_1:def 11;

    end;

    definition

      let J,D be set, K be ManySortedSet of J;

      mode DoubleIndexedSet of K,D is ManySortedFunction of K, (J --> D);

    end

    definition

      let J be set, K be ManySortedSet of J, S be 1-sorted;

      mode DoubleIndexedSet of K,S is DoubleIndexedSet of K, the carrier of S;

    end

    theorem :: WAYBEL_5:6

    

     Th6: for J,D be set, K be ManySortedSet of J holds for F be DoubleIndexedSet of K, D holds for j be set st j in J holds (F . j) is Function of (K . j), D

    proof

      let J,D be set, K be ManySortedSet of J;

      let F be DoubleIndexedSet of K, D;

      let j be set;

      assume

       A1: j in J;

      then ((J --> D) . j) = D by FUNCOP_1: 7;

      hence thesis by A1, PBOOLE:def 15;

    end;

    definition

      let J,D be non empty set, K be ManySortedSet of J;

      let F be DoubleIndexedSet of K, D;

      let j be Element of J;

      :: original: .

      redefine

      func F . j -> Function of (K . j), D ;

      coherence by Th6;

    end

    registration

      let J,D be non empty set, K be non-empty ManySortedSet of J;

      let F be DoubleIndexedSet of K, D;

      let j be Element of J;

      cluster ( rng (F . j)) -> non empty;

      correctness ;

    end

    registration

      let J be set, D be non empty set;

      let K be non-empty ManySortedSet of J;

      cluster -> non-empty for DoubleIndexedSet of K, D;

      correctness

      proof

        let F be DoubleIndexedSet of K, D;

        for j be object st j in ( dom F) holds (F . j) is non empty

        proof

          let j be object;

          set k = the Element of (K . j);

          assume j in ( dom F);

          then

           A1: j in J;

          then (F . j) is Function of (K . j), D by Th6;

          then ( dom (F . j)) = (K . j) by FUNCT_2:def 1;

          then [k, ((F . j) . k)] in (F . j) by A1, FUNCT_1:def 2;

          hence thesis;

        end;

        hence thesis by FUNCT_1:def 9;

      end;

    end

    registration

      let F be Function-yielding Function;

      cluster ( dom ( Frege F)) -> functional;

      coherence ;

    end

    ::$Canceled

    theorem :: WAYBEL_5:8

    

     Th8: for F be Function-yielding Function holds for f be Function st f in ( dom ( Frege F)) holds ( dom f) = ( dom F) & ( dom F) = ( dom (( Frege F) . f))

    proof

      let F be Function-yielding Function;

      let f be Function;

      assume f in ( dom ( Frege F));

      then

       A1: f in ( product ( doms F));

      then ex g be Function st g = f & ( dom g) = ( dom ( doms F)) & for x be object st x in ( dom ( doms F)) holds (g . x) in (( doms F) . x) by CARD_3:def 5;

      hence

       A2: ( dom f) = ( dom F) by FUNCT_6: 59;

      

      thus ( dom (( Frege F) . f)) = ( dom (F .. f)) by A1, PRALG_2:def 2

      .= (( dom F) /\ ( dom f)) by PRALG_1:def 19

      .= ( dom F) by A2;

    end;

    theorem :: WAYBEL_5:9

    

     Th9: for F be Function-yielding Function holds for f be Function st f in ( dom ( Frege F)) holds for i be set st i in ( dom F) holds (f . i) in ( dom (F . i)) & ((( Frege F) . f) . i) = ((F . i) . (f . i)) & ((F . i) . (f . i)) in ( rng (( Frege F) . f))

    proof

      let F be Function-yielding Function;

      let f be Function such that

       A1: f in ( dom ( Frege F));

      

       A2: f in ( product ( doms F)) by A1;

      set G = (( Frege F) . f);

      let i be set such that

       A3: i in ( dom F);

      i in ( dom f) by Th8, A1, A3;

      then i in (( dom F) /\ ( dom f)) by A3, XBOOLE_0:def 4;

      then

       a3: i in ( dom (F .. f)) by PRALG_1:def 19;

      i in ( dom ( doms F)) by A3, FUNCT_6: 59;

      then (f . i) in (( doms F) . i) by A2, CARD_3: 9;

      hence (f . i) in ( dom (F . i)) by A3, FUNCT_6: 22;

      G = (F .. f) by A2, PRALG_2:def 2;

      hence

       A4: (G . i) = ((F . i) . (f . i)) by a3, PRALG_1:def 19;

      ( dom G) = ( dom F) by A1, Th8;

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

    end;

    theorem :: WAYBEL_5:10

    

     Th10: for J,D be set, K be ManySortedSet of J holds for F be DoubleIndexedSet of K, D holds for f be Function st f in ( dom ( Frege F)) holds (( Frege F) . f) is Function of J, D

    proof

      let J,D be set, K be ManySortedSet of J;

      let F be DoubleIndexedSet of K, D;

      let f be Function such that

       A1: f in ( dom ( Frege F));

      set G = (( Frege F) . f);

      

       A2: ( dom G) = ( dom F) by A1, Th8;

      

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

      ( rng G) c= D

      proof

        let y be object;

        assume y in ( rng G);

        then

        consider x be object such that

         A4: x in ( dom G) and

         A5: y = (G . x) by FUNCT_1:def 3;

        (F . x) is Function of (K . x), D by A2, A4, Th6;

        then

         A6: ( rng (F . x)) c= D by RELAT_1:def 19;

        (G . x) = ((F . x) . (f . x)) & (f . x) in ( dom (F . x)) by A1, A2, A4, Th9;

        then y in ( rng (F . x)) by A5, FUNCT_1:def 3;

        hence thesis by A6;

      end;

      hence thesis by A3, A2, FUNCT_2: 2;

    end;

    

     Lm5: for J,D be set, K be ManySortedSet of J holds for F be DoubleIndexedSet of K, D holds for f be Function st f in ( dom ( Frege F)) holds for j be set st j in J holds ((( Frege F) . f) . j) = ((F . j) . (f . j)) & ((F . j) . (f . j)) in ( rng (( Frege F) . f))

    proof

      let J,D be set, K be ManySortedSet of J;

      let F be DoubleIndexedSet of K, D;

      let f be Function such that

       A1: f in ( dom ( Frege F));

      let j be set;

      assume j in J;

      then

       A2: j in ( dom F) by PARTFUN1:def 2;

      hence ((( Frege F) . f) . j) = ((F . j) . (f . j)) by A1, Th9;

      thus thesis by A1, A2, Th9;

    end;

    

     Lm6: for J be set, K be ManySortedSet of J, D be non empty set holds for F be DoubleIndexedSet of K, D holds for f be Function st f in ( dom ( Frege F)) holds for j be set st j in J holds (f . j) in (K . j)

    proof

      let J be set, K be ManySortedSet of J, D be non empty set;

      let F be DoubleIndexedSet of K, D;

      let f be Function such that

       A1: f in ( dom ( Frege F));

      let j be set such that

       A2: j in J;

      

       A3: (F . j) is Function of (K . j), D by A2, Th6;

      ( dom F) = J by PARTFUN1:def 2;

      then (f . j) in ( dom (F . j)) by A1, A2, Th9;

      hence thesis by A3, FUNCT_2:def 1;

    end;

    registration

      let f be non-empty Function-yielding Function;

      cluster ( doms f) -> non-empty;

      correctness

      proof

        for j be object st j in ( dom ( doms f)) holds (( doms f) . j) is non empty

        proof

          let j be object;

          assume that

           A1: j in ( dom ( doms f)) and

           A2: (( doms f) . j) is empty;

          

           A3: j in ( dom f) by A1, FUNCT_6:def 2;

          reconsider fj = (f . j) as Function;

          

           A4: j in ( dom f) by A3;

          then {} = ( dom fj) by A2, FUNCT_6: 22;

          then (f . j) = {} ;

          hence contradiction by A4, FUNCT_1:def 9;

        end;

        hence thesis by FUNCT_1:def 9;

      end;

    end

    definition

      let J,D be set, K be ManySortedSet of J;

      let F be DoubleIndexedSet of K, D;

      :: original: Frege

      redefine

      func Frege F -> DoubleIndexedSet of (( product ( doms F)) --> J), D ;

      coherence

      proof

        set G = ( Frege F);

        set PD = ( product ( doms F));

        set A = (PD --> J), B = (PD --> D);

        for i st i in PD holds (G . i) is Function of (A . i), (B . i)

        proof

          let i;

          assume

           A1: i in PD;

          then

          reconsider f = i as Function;

          

           A2: (B . i) = D by A1, FUNCOP_1: 7;

          i in ( dom G) & (A . i) = J by A1, FUNCOP_1: 7, PARTFUN1:def 2;

          then (G . f) is Function of (A . i), (B . i) by A2, Th10;

          hence thesis;

        end;

        hence thesis by PBOOLE:def 15;

      end;

    end

    definition

      let J,D be non empty set, K be non-empty ManySortedSet of J;

      let F be DoubleIndexedSet of K, D;

      let G be DoubleIndexedSet of (( product ( doms F)) --> J), D;

      let f be Element of ( product ( doms F));

      :: original: .

      redefine

      func G . f -> Function of J, D ;

      coherence

      proof

        thus (G . f) is Function of J, D;

      end;

    end

    definition

      let L be non empty RelStr;

      let F be Function-yielding Function;

      :: WAYBEL_5:def1

      func \// (F,L) -> Function of ( dom F), the carrier of L means

      : Def1: for x st x in ( dom F) holds (it . x) = ( \\/ ((F . x),L));

      existence

      proof

        deffunc F( object) = ( \\/ ((F . $1),L));

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

        then

        consider f be Function such that

         A1: ( dom f) = ( dom F) and

         A2: for x be object st x in ( dom F) holds (f . x) = ( \\/ ((F . x),L));

        ( rng f) c= the carrier of L

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A3: x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

          y = ( \\/ ((F . x),L)) by A1, A2, A3;

          hence thesis;

        end;

        then

        reconsider f as Function of ( dom F), the carrier of L by A1, FUNCT_2: 2;

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be Function of ( dom F), the carrier of L such that

         A4: for x st x in ( dom F) holds (f . x) = ( \\/ ((F . x),L)) and

         A5: for x st x in ( dom F) holds (g . x) = ( \\/ ((F . x),L));

         A6:

        now

          let x be object;

          assume

           A7: x in ( dom F);

          

          hence (f . x) = ( \\/ ((F . x),L)) by A4

          .= (g . x) by A5, A7;

        end;

        ( dom f) = ( dom F) & ( dom g) = ( dom F) by FUNCT_2:def 1;

        hence thesis by A6, FUNCT_1: 2;

      end;

      :: WAYBEL_5:def2

      func /\\ (F,L) -> Function of ( dom F), the carrier of L means

      : Def2: for x st x in ( dom F) holds (it . x) = ( //\ ((F . x),L));

      existence

      proof

        deffunc F( object) = ( //\ ((F . $1),L));

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

        then

        consider f be Function such that

         A8: ( dom f) = ( dom F) and

         A9: for x be object st x in ( dom F) holds (f . x) = ( //\ ((F . x),L));

        ( rng f) c= the carrier of L

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A10: x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

          y = ( //\ ((F . x),L)) by A8, A9, A10;

          hence thesis;

        end;

        then

        reconsider f as Function of ( dom F), the carrier of L by A8, FUNCT_2: 2;

        take f;

        thus thesis by A9;

      end;

      uniqueness

      proof

        let f,g be Function of ( dom F), the carrier of L such that

         A11: for x st x in ( dom F) holds (f . x) = ( //\ ((F . x),L)) and

         A12: for x st x in ( dom F) holds (g . x) = ( //\ ((F . x),L));

         A13:

        now

          let x be object;

          assume

           A14: x in ( dom F);

          

          hence (f . x) = ( //\ ((F . x),L)) by A11

          .= (g . x) by A12, A14;

        end;

        ( dom f) = ( dom F) & ( dom g) = ( dom F) by FUNCT_2:def 1;

        hence thesis by A13, FUNCT_1: 2;

      end;

    end

    notation

      let J be set, K be ManySortedSet of J, L be non empty RelStr;

      let F be DoubleIndexedSet of K, L;

      synonym Sups F for \// (F,L);

      synonym Infs F for /\\ (F,L);

    end

    notation

      let I,J be set, L be non empty RelStr;

      let F be DoubleIndexedSet of (I --> J), L;

      synonym Sups F for \// (F,L);

      synonym Infs F for /\\ (F,L);

    end

    theorem :: WAYBEL_5:11

    

     Th11: for L be non empty RelStr holds for F,G be Function-yielding Function st ( dom F) = ( dom G) & (for x st x in ( dom F) holds ( \\/ ((F . x),L)) = ( \\/ ((G . x),L))) holds ( \// (F,L)) = ( \// (G,L))

    proof

      let L be non empty RelStr;

      let F,G be Function-yielding Function such that

       A1: ( dom F) = ( dom G) and

       A2: for x st x in ( dom F) holds ( \\/ ((F . x),L)) = ( \\/ ((G . x),L));

      

       A3: for x be object st x in ( dom F) holds (( \// (F,L)) . x) = (( \// (G,L)) . x)

      proof

        let x be object;

        assume

         A4: x in ( dom F);

        

        hence (( \// (F,L)) . x) = ( \\/ ((F . x),L)) by Def1

        .= ( \\/ ((G . x),L)) by A2, A4

        .= (( \// (G,L)) . x) by A1, A4, Def1;

      end;

      ( dom ( \// (F,L))) = ( dom F) & ( dom ( \// (G,L))) = ( dom G) by FUNCT_2:def 1;

      hence thesis by A1, A3, FUNCT_1: 2;

    end;

    theorem :: WAYBEL_5:12

    

     Th12: for L be non empty RelStr holds for F,G be Function-yielding Function st ( dom F) = ( dom G) & (for x st x in ( dom F) holds ( //\ ((F . x),L)) = ( //\ ((G . x),L))) holds ( /\\ (F,L)) = ( /\\ (G,L))

    proof

      let L be non empty RelStr;

      let F,G be Function-yielding Function such that

       A1: ( dom F) = ( dom G) and

       A2: for x st x in ( dom F) holds ( //\ ((F . x),L)) = ( //\ ((G . x),L));

      

       A3: for x be object st x in ( dom F) holds (( /\\ (F,L)) . x) = (( /\\ (G,L)) . x)

      proof

        let x be object;

        assume

         A4: x in ( dom F);

        

        hence (( /\\ (F,L)) . x) = ( //\ ((F . x),L)) by Def2

        .= ( //\ ((G . x),L)) by A2, A4

        .= (( /\\ (G,L)) . x) by A1, A4, Def2;

      end;

      ( dom ( /\\ (F,L))) = ( dom F) & ( dom ( /\\ (G,L))) = ( dom G) by FUNCT_2:def 1;

      hence thesis by A1, A3, FUNCT_1: 2;

    end;

    theorem :: WAYBEL_5:13

    

     Th13: for L be non empty RelStr holds for F be Function-yielding Function holds (y in ( rng ( \// (F,L))) iff ex x st x in ( dom F) & y = ( \\/ ((F . x),L))) & (y in ( rng ( /\\ (F,L))) iff ex x st x in ( dom F) & y = ( //\ ((F . x),L)))

    proof

      let L be non empty RelStr;

      let F be Function-yielding Function;

      thus y in ( rng ( \// (F,L))) iff ex x st x in ( dom F) & y = ( \\/ ((F . x),L))

      proof

        hereby

          assume y in ( rng ( \// (F,L)));

          then

          consider x be object such that

           A1: x in ( dom ( \// (F,L))) & y = (( \// (F,L)) . x) by FUNCT_1:def 3;

          take x;

          thus x in ( dom F) & y = ( \\/ ((F . x),L)) by A1, Def1;

        end;

        given x such that

         A2: x in ( dom F) & y = ( \\/ ((F . x),L));

        x in ( dom ( \// (F,L))) & y = (( \// (F,L)) . x) by A2, Def1, FUNCT_2:def 1;

        hence thesis by FUNCT_1:def 3;

      end;

      thus y in ( rng ( /\\ (F,L))) iff ex x st x in ( dom F) & y = ( //\ ((F . x),L))

      proof

        hereby

          assume y in ( rng ( /\\ (F,L)));

          then

          consider x be object such that

           A3: x in ( dom ( /\\ (F,L))) & y = (( /\\ (F,L)) . x) by FUNCT_1:def 3;

          take x;

          thus x in ( dom F) & y = ( //\ ((F . x),L)) by A3, Def2;

        end;

        given x such that

         A4: x in ( dom F) & y = ( //\ ((F . x),L));

        x in ( dom ( /\\ (F,L))) & y = (( /\\ (F,L)) . x) by A4, Def2, FUNCT_2:def 1;

        hence thesis by FUNCT_1:def 3;

      end;

    end;

    theorem :: WAYBEL_5:14

    

     Th14: for L be non empty RelStr holds for J be non empty set, K be ManySortedSet of J holds for F be DoubleIndexedSet of K, L holds (x in ( rng ( Sups F)) iff ex j be Element of J st x = ( Sup (F . j))) & (x in ( rng ( Infs F)) iff ex j be Element of J st x = ( Inf (F . j)))

    proof

      let L be non empty RelStr;

      let J be non empty set, K be ManySortedSet of J;

      let F be DoubleIndexedSet of K, L;

      

       A1: ( dom F) = J by PARTFUN1:def 2;

      thus x in ( rng ( Sups F)) iff ex j be Element of J st x = ( Sup (F . j))

      proof

        hereby

          assume x in ( rng ( Sups F));

          then

          consider j be object such that

           A2: j in ( dom F) and

           A3: x = ( \\/ ((F . j),L)) by Th13;

          reconsider j as Element of J by A2;

          take j;

          thus x = ( Sup (F . j)) by A3;

        end;

        thus thesis by A1, Th13;

      end;

      hereby

        assume x in ( rng ( Infs F));

        then

        consider j be object such that

         A4: j in ( dom F) and

         A5: x = ( //\ ((F . j),L)) by Th13;

        reconsider j as Element of J by A4;

        take j;

        thus x = ( Inf (F . j)) by A5;

      end;

      thus thesis by A1, Th13;

    end;

    registration

      let J be non empty set, K be ManySortedSet of J, L be non empty RelStr;

      let F be DoubleIndexedSet of K, L;

      cluster ( rng ( Sups F)) -> non empty;

      correctness ;

      cluster ( rng ( Infs F)) -> non empty;

      correctness ;

    end

    reserve L for complete LATTICE,

a,b,c for Element of L,

J for non empty set,

K for non-empty ManySortedSet of J;

    

     Lm7: for F be DoubleIndexedSet of K, L holds for f be set holds f is Element of ( product ( doms F)) iff f in ( dom ( Frege F))

    proof

      let F be DoubleIndexedSet of K, L;

      let f be set;

      hereby

        assume f is Element of ( product ( doms F));

        then f in ( product ( doms F));

        hence f in ( dom ( Frege F)) by PARTFUN1:def 2;

      end;

      thus thesis;

    end;

    theorem :: WAYBEL_5:15

    

     Th15: for F be Function-yielding Function holds (for f be Function st f in ( dom ( Frege F)) holds ( //\ ((( Frege F) . f),L)) <= a) implies ( Sup ( /\\ (( Frege F),L))) <= a

    proof

      let F be Function-yielding Function;

      assume

       A1: for f be Function st f in ( dom ( Frege F)) holds ( //\ ((( Frege F) . f),L)) <= a;

      ( rng ( /\\ (( Frege F),L))) is_<=_than a

      proof

        let c;

        assume c in ( rng ( /\\ (( Frege F),L)));

        then

        consider f be object such that

         A2: f in ( dom ( Frege F)) and

         A3: c = ( //\ ((( Frege F) . f),L)) by Th13;

        reconsider f as Function by A2;

        f in ( dom ( Frege F)) by A2;

        hence c <= a by A1, A3;

      end;

      then ( sup ( rng ( /\\ (( Frege F),L)))) <= a by YELLOW_0: 32;

      hence thesis by YELLOW_2:def 5;

    end;

    theorem :: WAYBEL_5:16

    

     Th16: for F be DoubleIndexedSet of K, L holds ( Inf ( Sups F)) >= ( Sup ( Infs ( Frege F)))

    proof

      let F be DoubleIndexedSet of K, L;

      set a = ( Sup ( Infs ( Frege F)));

      

       A1: for j be Element of J holds for f be Element of ( product ( doms F)) holds ( Sup (F . j)) >= ( Inf (( Frege F) . f))

      proof

        let j be Element of J;

        let f be Element of ( product ( doms F));

        

         A2: f in ( dom ( Frege F)) by Lm7;

        then

        reconsider k = (f . j) as Element of (K . j) by Lm6;

        ((F . j) . k) = ((( Frege F) . f) . j) by A2, Lm5;

        then

         A3: ( Inf (( Frege F) . f)) <= ((F . j) . k) by YELLOW_2: 53;

        ((F . j) . k) <= ( Sup (F . j)) by YELLOW_2: 53;

        hence thesis by A3, ORDERS_2: 3;

      end;

      a is_<=_than ( rng ( Sups F))

      proof

        let c;

        assume c in ( rng ( Sups F));

        then

        consider j be Element of J such that

         A4: c = ( Sup (F . j)) by Th14;

        for f be Function st f in ( dom ( Frege F)) holds ( //\ ((( Frege F) . f),L)) <= c by A1, A4;

        hence a <= c by Th15;

      end;

      then a <= ( inf ( rng ( Sups F))) by YELLOW_0: 33;

      hence thesis by YELLOW_2:def 6;

    end;

    theorem :: WAYBEL_5:17

    

     Th17: (L is continuous & for c st c << a holds c <= b) implies a <= b

    proof

      assume that

       A1: L is continuous and

       A2: for c st c << a holds c <= b;

      for c st c in ( waybelow a) holds c <= b by A2, WAYBEL_3: 7;

      then ( waybelow a) is_<=_than b;

      then ( sup ( waybelow a)) <= b by YELLOW_0: 32;

      hence thesis by A1, WAYBEL_3:def 5;

    end;

    

     Lm8: L is continuous implies for J, K holds for F be DoubleIndexedSet of K, L st for j be Element of J holds ( rng (F . j)) is directed holds ( Inf ( Sups F)) = ( Sup ( Infs ( Frege F)))

    proof

      assume

       A1: L is continuous;

      let J, K;

      let F be DoubleIndexedSet of K, L such that

       A2: for j be Element of J holds ( rng (F . j)) is directed;

      now

        let c;

        assume

         A3: c << ( Inf ( Sups F));

        

         A4: for j be Element of J holds c << ( Sup (F . j))

        proof

          let j be Element of J;

          ( Sup (F . j)) in ( rng ( Sups F)) by Th14;

          then ( inf ( rng ( Sups F))) <= ( Sup (F . j)) by YELLOW_2: 22;

          then ( Inf ( Sups F)) <= ( Sup (F . j)) by YELLOW_2:def 6;

          hence thesis by A3, WAYBEL_3: 2;

        end;

        ex f be Function st f in ( dom ( Frege F)) & for j be Element of J holds ex b st b = ((F . j) . (f . j)) & c <= b

        proof

          defpred P[ object, object] means $1 in J & $2 in (K . $1) & ex b st b = ((F . $1) . $2) & c <= b;

          

           A5: for j be Element of J holds ex k be Element of (K . j) st c <= ((F . j) . k)

          proof

            let j be Element of J;

            

             A6: ( Sup (F . j)) <= ( sup ( rng (F . j))) by YELLOW_2:def 5;

            ( rng (F . j)) is non empty directed Subset of L & c << ( Sup (F . j)) by A2, A4;

            then

            consider d be Element of L such that

             A7: d in ( rng (F . j)) and

             A8: c <= d by A6, WAYBEL_3:def 1;

            consider k be object such that

             A9: k in ( dom (F . j)) and

             A10: d = ((F . j) . k) by A7, FUNCT_1:def 3;

            reconsider k as Element of (K . j) by A9;

            take k;

            thus thesis by A8, A10;

          end;

          

           A11: for j be object st j in J holds ex k be object st k in ( union ( rng K)) & P[j, k]

          proof

            let j be object;

            assume j in J;

            then

            reconsider j9 = j as Element of J;

            consider k be Element of (K . j9) such that

             A12: c <= ((F . j9) . k) by A5;

            take k;

            j9 in J;

            then j9 in ( dom K) by PARTFUN1:def 2;

            then (K . j9) in ( rng K) by FUNCT_1:def 3;

            hence k in ( union ( rng K)) by TARSKI:def 4;

            thus thesis by A12;

          end;

          consider f be Function such that

           A13: ( dom f) = J and ( rng f) c= ( union ( rng K)) and

           A14: for j be object st j in J holds P[j, (f . j)] from FUNCT_1:sch 6( A11);

           A15:

          now

            let x be object;

            assume x in ( dom ( doms F));

            then

             A16: x in ( dom F) by FUNCT_6: 59;

            then

            reconsider j = x as Element of J;

            (( doms F) . x) = ( dom (F . j)) by A16, FUNCT_6: 22

            .= (K . j) by FUNCT_2:def 1;

            hence (f . x) in (( doms F) . x) by A14;

          end;

          ( dom f) = ( dom F) by A13, PARTFUN1:def 2

          .= ( dom ( doms F)) by FUNCT_6: 59;

          then f in ( product ( doms F)) by A15, CARD_3: 9;

          then

           A17: f in ( dom ( Frege F)) by PARTFUN1:def 2;

          for j be Element of J holds (f . j) in (K . j) & ex b st b = ((F . j) . (f . j)) & c <= b by A14;

          hence thesis by A17;

        end;

        then

        consider f be Function such that

         A18: f in ( dom ( Frege F)) and

         A19: for j be Element of J holds ex b st b = ((F . j) . (f . j)) & c <= b;

        reconsider f as Element of ( product ( doms F)) by A18;

        reconsider G = (( Frege F) . f) as Function of J, the carrier of L;

        now

          let j be Element of J;

          j in J;

          then

           A20: j in ( dom F) by PARTFUN1:def 2;

          ex b st b = ((F . j) . (f . j)) & c <= b by A19;

          hence c <= (G . j) by A18, A20, Th9;

        end;

        then

         A21: c <= ( Inf (( Frege F) . f)) by YELLOW_2: 55;

        set a = ( Inf (( Frege F) . f));

        a in ( rng ( Infs ( Frege F))) by Th14;

        then a <= ( sup ( rng ( Infs ( Frege F)))) by YELLOW_2: 22;

        then a <= ( Sup ( Infs ( Frege F))) by YELLOW_2:def 5;

        hence c <= ( Sup ( Infs ( Frege F))) by A21, YELLOW_0:def 2;

      end;

      then

       A22: ( Inf ( Sups F)) <= ( Sup ( Infs ( Frege F))) by A1, Th17;

      ( Inf ( Sups F)) >= ( Sup ( Infs ( Frege F))) by Th16;

      hence thesis by A22, YELLOW_0:def 3;

    end;

    theorem :: WAYBEL_5:18

    

     Th18: (for J be non empty set st J in ( the_universe_of the carrier of L) holds for K be non-empty ManySortedSet of J st for j be Element of J holds (K . j) in ( the_universe_of the carrier of L) holds for F be DoubleIndexedSet of K, L st for j be Element of J holds ( rng (F . j)) is directed holds ( Inf ( Sups F)) = ( Sup ( Infs ( Frege F)))) implies L is continuous

    proof

      assume

       A1: for J be non empty set st J in ( the_universe_of the carrier of L) holds for K be non-empty ManySortedSet of J st for j be Element of J holds (K . j) in ( the_universe_of the carrier of L) holds for F be DoubleIndexedSet of K, L st (for j be Element of J holds ( rng (F . j)) is directed) holds ( Inf ( Sups F)) = ( Sup ( Infs ( Frege F)));

      now

        set UN = ( the_universe_of the carrier of L);

        let x be Element of L;

        set J = { j where j be directed non empty Subset of L : x <= ( sup j) };

        

         A2: UN = ( Tarski-Class ( the_transitive-closure_of the carrier of L)) by YELLOW_6:def 1;

        reconsider UN as universal set;

        

         A3: J c= ( bool the carrier of L)

        proof

          let u be object;

          assume u in J;

          then ex j be directed non empty Subset of L st u = j & x <= ( sup j);

          hence thesis;

        end;

        the carrier of L c= ( the_transitive-closure_of the carrier of L) & ( the_transitive-closure_of the carrier of L) in UN by A2, CLASSES1: 2, CLASSES1: 52;

        then

         A4: the carrier of L in UN by CLASSES1:def 1;

        then ( bool the carrier of L) in UN by CLASSES2: 59;

        then

         A5: J in UN by A3, CLASSES1:def 1;

        x is_>=_than ( waybelow x) by WAYBEL_3: 9;

        then

         A6: x >= ( sup ( waybelow x)) by YELLOW_0: 32;

         {x} is directed non empty Subset of L & x <= ( sup {x}) by WAYBEL_0: 5, YELLOW_0: 39;

        then

         A7: {x} in J;

        then

        reconsider J as non empty set;

        set K = ( id J);

        reconsider K as ManySortedSet of J;

        

         A8: for j be Element of J holds (K . j) in UN

        proof

          let j be Element of J;

          (K . j) in J;

          hence thesis by A4, A3, CLASSES1:def 1;

        end;

        reconsider j = {x} as Element of J by A7;

        

         A9: for j be Element of J holds j is directed non empty Subset of L

        proof

          let j be Element of J;

          j in J;

          then ex j9 be directed non empty Subset of L st j9 = j & x <= ( sup j9);

          hence thesis;

        end;

        for i be object st i in J holds (K . i) is non empty

        proof

          let i be object;

          assume i in J;

          then

          reconsider i9 = i as Element of J;

          (K . i) = i9;

          hence thesis by A9;

        end;

        then

        reconsider K as non-empty ManySortedSet of J by PBOOLE:def 13;

        deffunc F( object) = ( id (K . $1));

        ex F be Function st ( dom F) = J & for j be object st j in J holds (F . j) = F(j) from FUNCT_1:sch 3;

        then

        consider F be Function such that

         A10: ( dom F) = J and

         A11: for j be object st j in J holds (F . j) = ( id (K . j));

        reconsider F as ManySortedSet of J by A10, PARTFUN1:def 2, RELAT_1:def 18;

        for j be object st j in ( dom F) holds (F . j) is Function

        proof

          let j be object;

          assume j in ( dom F);

          then (F . j) = ( id (K . j)) by A11;

          hence thesis;

        end;

        then

        reconsider F as ManySortedFunction of J by FUNCOP_1:def 6;

        for j be object st j in J holds (F . j) is Function of (K . j), ((J --> the carrier of L) . j)

        proof

          let j be object;

          assume j in J;

          then

          reconsider j as Element of J;

          

           A12: (K . j) is Subset of L by A9;

          

           A13: (F . j) = ( id (K . j)) by A11;

          then ( rng (F . j)) c= (K . j);

          then ( rng (F . j)) c= the carrier of L by A12, XBOOLE_1: 1;

          then

           A14: ( rng (F . j)) c= ((J --> the carrier of L) . j);

          ( dom (F . j)) = (K . j) by A13;

          hence thesis by A14, FUNCT_2: 2;

        end;

        then

        reconsider F as DoubleIndexedSet of K, L by PBOOLE:def 15;

        

         A15: for j be Element of J, k be Element of (K . j) holds ((F . j) . k) = k

        proof

          let j be Element of J;

          let k be Element of (K . j);

          (F . j) = ( id (K . j)) by A11;

          hence thesis;

        end;

        

         A16: for j be Element of J holds ( rng (F . j)) = j

        proof

          let j be Element of J;

          now

            let y be object;

            assume y in ( rng (F . j));

            then

            consider x be object such that

             A17: x in ( dom (F . j)) and

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

            x in (K . j) by A17;

            then x in j;

            hence y in j by A15, A18;

          end;

          then

           A19: ( rng (F . j)) c= j;

          now

            let x be object;

            assume x in j;

            then x in (K . j);

            then ((F . j) . x) = x & x in ( dom (F . j)) by A15, FUNCT_2:def 1;

            hence x in ( rng (F . j)) by FUNCT_1:def 3;

          end;

          then j c= ( rng (F . j));

          hence thesis by A19, XBOOLE_0:def 10;

        end;

        

         A20: for j be Element of J holds ( rng (F . j)) is directed

        proof

          let j be Element of J;

          ( rng (F . j)) = j by A16;

          hence thesis by A9;

        end;

        for f be Function st f in ( dom ( Frege F)) holds ( //\ ((( Frege F) . f),L)) <= ( sup ( waybelow x))

        proof

          let f be Function such that

           A21: f in ( dom ( Frege F));

          set a = ( //\ ((( Frege F) . f),L));

          for D be non empty directed Subset of L st x <= ( sup D) holds ex d be Element of L st d in D & a <= d

          proof

            

             A22: for j be Element of J holds (f . j) in (K . j)

            proof

              let j be Element of J;

              j in J;

              then j in ( dom F) by PARTFUN1:def 2;

              then (f . j) in ( dom (F . j)) by A21, Th9;

              hence thesis;

            end;

            

             A23: ( dom f) = ( dom F) by A21, Th8

            .= J by PARTFUN1:def 2;

            now

              let y be object;

              assume y in ( rng f);

              then

              consider j be object such that

               A24: j in ( dom f) and

               A25: y = (f . j) by FUNCT_1:def 3;

              reconsider j as Element of J by A23, A24;

              y in (K . j) by A22, A25;

              then

               A26: y in j;

              j is Subset of L by A9;

              hence y in the carrier of L by A26;

            end;

            then ( rng f) c= the carrier of L;

            then

            reconsider f as Function of J, the carrier of L by A23, FUNCT_2: 2;

            let D be non empty directed Subset of L;

            assume x <= ( sup D);

            then D in J;

            then

            reconsider D9 = D as Element of J;

            

             A27: ( Inf f) <= (f . D9) by YELLOW_2: 53;

            (f . D9) in (K . D9) by A22;

            then

             A28: (f . D9) in D9;

             A29:

            now

              let j be object;

              assume

               A30: j in ( dom f);

              then

              reconsider j9 = j as Element of J;

              

               A31: (f . j9) is Element of (K . j9) by A22;

              j in ( dom F) by A21, A30, Th8;

              

              hence ((( Frege F) . f) . j) = ((F . j9) . (f . j9)) by A21, Th9

              .= (f . j) by A15, A31;

            end;

            ( dom f) = ( dom F) by A21, Th8

            .= ( dom (( Frege F) . f)) by A21, Th8;

            then a <= (f . D9) by A27, A29, FUNCT_1: 2;

            hence thesis by A28;

          end;

          then a << x by WAYBEL_3:def 1;

          then a in ( waybelow x) by WAYBEL_3: 7;

          hence thesis by YELLOW_2: 22;

        end;

        then

         A32: ( Sup ( Infs ( Frege F))) <= ( sup ( waybelow x)) by Th15;

        x is_<=_than ( rng ( Sups F))

        proof

          let b be Element of L;

          assume b in ( rng ( Sups F));

          then

          consider j be Element of J such that

           A33: b = ( Sup (F . j)) by Th14;

          j in J;

          then

          consider j9 be directed non empty Subset of L such that

           A34: j9 = j and

           A35: x <= ( sup j9);

          b = ( sup ( rng (F . j))) by A33, YELLOW_2:def 5

          .= ( sup j9) by A16, A34;

          hence x <= b by A35;

        end;

        then x <= ( inf ( rng ( Sups F))) by YELLOW_0: 33;

        then

         A36: x <= ( Inf ( Sups F)) by YELLOW_2:def 6;

        ( Sup (F . j)) = ( sup ( rng (F . j))) by YELLOW_2:def 5

        .= ( sup {x}) by A16

        .= x by YELLOW_0: 39;

        then x in ( rng ( Sups F)) by Th14;

        then ( inf ( rng ( Sups F))) <= x by YELLOW_2: 22;

        then ( Inf ( Sups F)) <= x by YELLOW_2:def 6;

        

        then x = ( Inf ( Sups F)) by A36, ORDERS_2: 2

        .= ( Sup ( Infs ( Frege F))) by A1, A5, A8, A20;

        hence x = ( sup ( waybelow x)) by A32, A6, ORDERS_2: 2;

      end;

      then L is up-complete satisfying_axiom_of_approximation by WAYBEL_3:def 5;

      hence thesis;

    end;

    

     Lm9: (for J, K holds for F be DoubleIndexedSet of K, L st for j be Element of J holds ( rng (F . j)) is directed holds ( Inf ( Sups F)) = ( Sup ( Infs ( Frege F)))) implies L is continuous

    proof

      assume for J, K holds for F be DoubleIndexedSet of K, L st for j be Element of J holds ( rng (F . j)) is directed holds ( Inf ( Sups F)) = ( Sup ( Infs ( Frege F)));

      then for J be non empty set st J in ( the_universe_of the carrier of L) holds for K be non-empty ManySortedSet of J st for j be Element of J holds (K . j) in ( the_universe_of the carrier of L) holds for F be DoubleIndexedSet of K, L st (for j be Element of J holds ( rng (F . j)) is directed) holds ( Inf ( Sups F)) = ( Sup ( Infs ( Frege F)));

      hence thesis by Th18;

    end;

    theorem :: WAYBEL_5:19

    L is continuous iff for J, K holds for F be DoubleIndexedSet of K, L st for j be Element of J holds ( rng (F . j)) is directed holds ( Inf ( Sups F)) = ( Sup ( Infs ( Frege F))) by Lm8, Lm9;

    definition

      let J,K,D be non empty set;

      let F be Function of [:J, K:], D;

      :: original: curry

      redefine

      func curry F -> DoubleIndexedSet of (J --> K), D ;

      coherence

      proof

        reconsider F9 = F as ManySortedSet of [:J, K:];

        

         A1: ( dom F) = [:J, K:] by FUNCT_2:def 1;

        for j be object st j in J holds (( curry F9) . j) is Function of ((J --> K) . j), ((J --> D) . j)

        proof

          let j be object;

          assume

           A2: j in J;

          then

          consider g be Function such that

           A3: (( curry F9) . j) = g and

           A4: ( dom g) = K and

           A5: ( rng g) c= ( rng F9) and for k be object st k in K holds (g . k) = (F9 . (j,k)) by A1, FUNCT_5: 29;

          J = ( dom ( curry F)) by A1, FUNCT_5: 24;

          then

          reconsider G = (( curry F9) . j) as Function;

          ( rng F) c= D;

          then ( rng g) c= D by A5;

          then

          reconsider g as Function of K, D by A4, FUNCT_2:def 1, RELSET_1: 4;

          

           A6: G = g by A3;

          ((J --> K) . j) = K by A2, FUNCOP_1: 7;

          hence thesis by A2, A6, FUNCOP_1: 7;

        end;

        hence thesis by PBOOLE:def 15;

      end;

    end

    reserve J,K,D for non empty set,

j for Element of J,

k for Element of K;

    theorem :: WAYBEL_5:20

    

     Th20: for F be Function of [:J, K:], D holds ( dom ( curry F)) = J & ( dom (( curry F) . j)) = K & (F . (j,k)) = ((( curry F) . j) . k)

    proof

      let F be Function of [:J, K:], D;

      

      thus ( dom ( curry F)) = ( proj1 ( dom F)) by FUNCT_5:def 1

      .= ( proj1 [:J, K:]) by FUNCT_2:def 1

      .= J by FUNCT_5: 9;

      ( dom F) = [:J, K:] by FUNCT_2:def 1;

      then ex g be Function st (( curry F) . j) = g & ( dom g) = K & ( rng g) c= ( rng F) & for i be object st i in K holds (g . i) = (F . (j,i)) by FUNCT_5: 29;

      hence ( dom (( curry F) . j)) = K;

       [j, k] in [:J, K:];

      then [j, k] in ( dom F) by FUNCT_2:def 1;

      hence thesis by FUNCT_5: 20;

    end;

    

     Lm10: (for J, K holds for F be Function of [:J, K:], the carrier of L st for j be Element of J holds ( rng (( curry F) . j)) is directed holds ( Inf ( Sups ( curry F))) = ( Sup ( Infs ( Frege ( curry F))))) implies L is continuous

    proof

      assume

       A1: for J, K holds for F be Function of [:J, K:], the carrier of L st for j be Element of J holds ( rng (( curry F) . j)) is directed holds ( Inf ( Sups ( curry F))) = ( Sup ( Infs ( Frege ( curry F))));

      for J holds for K be non-empty ManySortedSet of J holds for F be DoubleIndexedSet of K, L st for j be Element of J holds ( rng (F . j)) is directed holds ( Inf ( Sups F)) = ( Sup ( Infs ( Frege F)))

      proof

        let J;

        let K be non-empty ManySortedSet of J;

        let F be DoubleIndexedSet of K, L;

        set j = the Element of J;

        set k = the Element of (K . j);

        defpred P[ set, set, set] means $1 in J & (($2 in (K . $1) & $3 = ((F . $1) . $2)) or ( not $2 in (K . $1) & $3 = ( Bottom L)));

        

         A2: ( dom ( doms F)) = ( dom F) by FUNCT_6: 59;

        j in J;

        then j in ( dom K) by PARTFUN1:def 2;

        then k in (K . j) & (K . j) in ( rng K) by FUNCT_1:def 3;

        then

        reconsider K9 = ( union ( rng K)) as non empty set by TARSKI:def 4;

        

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

        

         A4: for j be Element of J holds for k9 be Element of K9 holds ex z be Element of L st P[j, k9, z]

        proof

          let j be Element of J;

          let k9 be Element of K9;

          per cases ;

            suppose k9 in (K . j);

            then

            reconsider k = k9 as Element of (K . j);

            take ((F . j) . k);

            thus thesis;

          end;

            suppose

             A5: not k9 in (K . j);

            take ( Bottom L);

            thus thesis by A5;

          end;

        end;

        ex G be Function of [:J, K9:], the carrier of L st for j be Element of J holds for k be Element of K9 holds P[j, k, (G . (j,k))] from BINOP_1:sch 3( A4);

        then

        consider G be Function of [:J, K9:], the carrier of L such that

         A6: for j be Element of J holds for k be Element of K9 holds P[j, k, (G . (j,k))];

        

         A7: for j be Element of J holds (K . j) c= K9

        proof

          let j be Element of J;

          hereby

            let k be object;

            j in J;

            then j in ( dom K) by PARTFUN1:def 2;

            then

             A8: (K . j) in ( rng K) by FUNCT_1:def 3;

            assume k in (K . j);

            hence k in K9 by A8, TARSKI:def 4;

          end;

        end;

        

         A9: for j be Element of J holds ( rng (F . j)) c= ( rng (( curry G) . j))

        proof

          let j be Element of J;

          hereby

            let y be object;

            assume y in ( rng (F . j));

            then

            consider k be object such that

             A10: k in ( dom (F . j)) and

             A11: y = ((F . j) . k) by FUNCT_1:def 3;

            

             A12: k in (K . j) by A10;

            (K . j) c= K9 by A7;

            then

            reconsider k as Element of K9 by A12;

             [j, k] in [:J, K9:];

            then

             A13: [j, k] in ( dom G) by FUNCT_2:def 1;

            k in K9 & ( dom (( curry G) . j)) = ((J --> K9) . j) by FUNCT_2:def 1;

            then

             A14: k in ( dom (( curry G) . j));

            y = (G . (j,k)) by A6, A10, A11

            .= ((( curry G) . j) . k) by A13, FUNCT_5: 20;

            hence y in ( rng (( curry G) . j)) by A14, FUNCT_1:def 3;

          end;

        end;

        

         A15: for j be object st j in ( dom F) holds ( \\/ ((F . j),L)) = ( \\/ ((( curry G) . j),L))

        proof

          let j9 be object;

          assume j9 in ( dom F);

          then

          reconsider j = j9 as Element of J;

          reconsider H = (( curry G) . j) as Function of ((J --> K9) . j), the carrier of L;

          reconsider H as Function of K9, the carrier of L;

          for k be Element of K9 holds (H . k) <= ( Sup (F . j))

          proof

            let k be Element of K9;

            per cases ;

              suppose

               A16: k in (K . j);

              then

               A17: k in ( dom (F . j)) by FUNCT_2:def 1;

              ((F . j) . k) = (G . (j,k)) by A6, A16

              .= (H . k) by Th20;

              then (H . k) in ( rng (F . j)) by A17, FUNCT_1:def 3;

              then (H . k) <= ( sup ( rng (F . j))) by YELLOW_2: 22;

              hence thesis by YELLOW_2:def 5;

            end;

              suppose not k in (K . j);

              

              then ( Bottom L) = (G . (j,k)) by A6

              .= (H . k) by Th20;

              hence thesis by YELLOW_0: 44;

            end;

          end;

          then

           A18: ( Sup H) <= ( Sup (F . j)) by YELLOW_2: 54;

           ex_sup_of (( rng (F . j)),L) & ex_sup_of (( rng (( curry G) . j)),L) by YELLOW_0: 17;

          then ( sup ( rng (F . j))) <= ( sup ( rng (( curry G) . j))) by A9, YELLOW_0: 34;

          then ( Sup (F . j)) <= ( sup ( rng H)) by YELLOW_2:def 5;

          then ( Sup (F . j)) <= ( Sup H) by YELLOW_2:def 5;

          hence thesis by A18, ORDERS_2: 2;

        end;

        

         A19: ( dom ( doms ( curry G))) = ( dom ( curry G)) by FUNCT_6: 59;

        

         A20: ( dom ( curry G)) = J by Th20;

        ( product ( doms F)) c= ( product ( doms ( curry G)))

        proof

          let x be object;

          assume x in ( product ( doms F));

          then

          consider g be Function such that

           A21: x = g and

           A22: ( dom g) = ( dom ( doms F)) and

           A23: for j be object st j in ( dom ( doms F)) holds (g . j) in (( doms F) . j) by CARD_3:def 5;

          

           A24: for j be object st j in ( dom ( doms ( curry G))) holds (g . j) in (( doms ( curry G)) . j)

          proof

            let j be object;

            assume

             A25: j in ( dom ( doms ( curry G)));

            then

            reconsider j9 = j as Element of J by A19;

            j in J by A19, A25;

            then

             A26: (g . j) in (( doms F) . j) by A2, A3, A23;

            

             A27: (( doms F) . j) = ( dom (F . j9)) by A3, FUNCT_6: 22

            .= (K . j9) by FUNCT_2:def 1;

            

             A28: (K . j9) c= K9 by A7;

            (( doms ( curry G)) . j) = ( dom (( curry G) . j9)) by A20, FUNCT_6: 22

            .= K9 by Th20;

            hence thesis by A26, A27, A28;

          end;

          ( dom g) = ( dom ( doms ( curry G))) by A2, A3, A19, A22, Th20;

          hence thesis by A21, A24, CARD_3:def 5;

        end;

        then ( dom ( Frege F)) c= ( product ( doms ( curry G)));

        then

         A29: ( dom ( Frege F)) c= ( dom ( Frege ( curry G))) by PARTFUN1:def 2;

        

         A30: for f be object st f in ( dom ( Frege F)) holds ( //\ ((( Frege F) . f),L)) = ( //\ ((( Frege ( curry G)) . f),L))

        proof

          let f9 be object;

          assume

           A31: f9 in ( dom ( Frege F));

          then

          reconsider f = f9 as Element of ( product ( doms F));

          

           A32: ( dom (( Frege F) . f)) = ( dom F) by A31, Th8

          .= J by PARTFUN1:def 2;

          

           A33: for j be object st j in J holds ((( Frege F) . f) . j) = ((( Frege ( curry G)) . f) . j)

          proof

            let j9 be object;

            assume j9 in J;

            then

            reconsider j = j9 as Element of J;

            

             A34: (f . j) in (K . j) by A31, Lm6;

            (K . j) c= K9 by A7;

            then

            reconsider fj = (f . j) as Element of K9 by A34;

            ((( Frege F) . f) . j) = ((F . j) . fj) by A31, Lm5

            .= (G . (j,fj)) by A6, A34

            .= ((( curry G) . j) . (f . j)) by Th20

            .= ((( Frege ( curry G)) . f) . j) by A29, A31, Lm5;

            hence thesis;

          end;

          ( dom (( Frege ( curry G)) . f)) = ( dom ( curry G)) by A29, A31, Th8

          .= ( proj1 ( dom G)) by FUNCT_5:def 1

          .= ( proj1 [:J, K9:]) by FUNCT_2:def 1

          .= J by FUNCT_5: 9;

          hence thesis by A32, A33, FUNCT_1: 2;

        end;

        

         A35: ( Sup ( Infs ( Frege ( curry G)))) = ( Sup ( Infs ( Frege F)))

        proof

          per cases ;

            suppose

             A36: for j be Element of J holds (K . j) = K9;

            for j be object st j in J holds (( doms F) . j) = (( doms ( curry G)) . j)

            proof

              let j be object;

              assume j in J;

              then

              reconsider j9 = j as Element of J;

              

               A37: (( doms F) . j) = ( dom (F . j9)) by A3, FUNCT_6: 22

              .= (K . j9) by FUNCT_2:def 1;

              (( doms ( curry G)) . j) = ( dom (( curry G) . j9)) by A20, FUNCT_6: 22

              .= K9 by Th20;

              hence thesis by A36, A37;

            end;

            then ( doms F) = ( doms ( curry G)) by A2, A3, A19, A20, FUNCT_1: 2;

            then ( dom ( Frege F)) = ( product ( doms ( curry G))) by PARTFUN1:def 2;

            then ( dom ( Frege F)) = ( dom ( Frege ( curry G))) by PARTFUN1:def 2;

            hence thesis by A30, Th12;

          end;

            suppose ex j be Element of J st (K . j) <> K9;

            then

            consider j be Element of J such that

             A38: (K . j) <> K9;

            (K . j) c= K9 by A7;

            then not K9 c= (K . j) by A38, XBOOLE_0:def 10;

            then

            consider k be object such that

             A39: k in K9 and

             A40: not k in (K . j);

            reconsider k as Element of K9 by A39;

            

             A41: (( rng ( Infs ( Frege F))) \/ {( Bottom L)}) c= ( rng ( Infs ( Frege ( curry G))))

            proof

              let x be object;

              assume

               A42: x in (( rng ( Infs ( Frege F))) \/ {( Bottom L)});

              per cases by A42, XBOOLE_0:def 3;

                suppose x in ( rng ( Infs ( Frege F)));

                then

                consider f be object such that

                 A43: f in ( dom ( Frege F)) and

                 A44: x = ( //\ ((( Frege F) . f),L)) by Th13;

                x = ( //\ ((( Frege ( curry G)) . f),L)) by A30, A43, A44;

                hence thesis by A29, A43, Th13;

              end;

                suppose

                 A45: x in {( Bottom L)};

                then

                reconsider x9 = x as Element of L;

                set f = (J --> k);

                

                 A46: for x be object st x in ( dom ( doms ( curry G))) holds (f . x) in (( doms ( curry G)) . x)

                proof

                  let x be object;

                  assume x in ( dom ( doms ( curry G)));

                  then

                  reconsider j = x as Element of J by A19;

                  (( doms ( curry G)) . j) = ( dom (( curry G) . j)) by A20, FUNCT_6: 22

                  .= K9 by Th20;

                  hence thesis;

                end;

                ( dom f) = J

                .= ( dom ( doms ( curry G))) by A19, Th20;

                then f in ( product ( doms ( curry G))) by A46, CARD_3: 9;

                then

                 A48: f in ( dom ( Frege ( curry G))) by PARTFUN1:def 2;

                

                 A49: x = ( Bottom L) by A45, TARSKI:def 1;

                

                then x = (G . (j,k)) by A6, A40

                .= ((( curry G) . j) . k) by Th20

                .= ((( curry G) . j) . (f . j));

                then x in ( rng (( Frege ( curry G)) . f)) by A48, Lm5;

                then x9 >= ( "/\" (( rng (( Frege ( curry G)) . f)),L)) by YELLOW_2: 22;

                then

                 A50: x9 >= ( //\ ((( Frege ( curry G)) . f),L)) by YELLOW_2:def 6;

                x9 <= ( //\ ((( Frege ( curry G)) . f),L)) by A49, YELLOW_0: 44;

                then x9 = ( //\ ((( Frege ( curry G)) . f),L)) by A50, ORDERS_2: 2;

                hence thesis by A48, Th13;

              end;

            end;

            

             A51: ex_sup_of (( rng ( Infs ( Frege F))),L) & ex_sup_of ( {( Bottom L)},L) by YELLOW_0: 17;

            

             A52: ( rng ( Infs ( Frege ( curry G)))) c= (( rng ( Infs ( Frege F))) \/ {( Bottom L)})

            proof

              let x be object;

              assume x in ( rng ( Infs ( Frege ( curry G))));

              then

              consider f be object such that

               A53: f in ( dom ( Frege ( curry G))) and

               A54: x = ( //\ ((( Frege ( curry G)) . f),L)) by Th13;

              reconsider f as Function by A53;

              per cases ;

                suppose

                 A55: for j be Element of J holds (f . j) in (K . j);

                

                 A56: for x be object st x in ( dom ( doms F)) holds (f . x) in (( doms F) . x)

                proof

                  let x be object;

                  assume x in ( dom ( doms F));

                  then

                  reconsider j = x as Element of J by A3, FUNCT_6: 59;

                  (( doms F) . j) = ( dom (F . j)) by A3, FUNCT_6: 22

                  .= (K . j) by FUNCT_2:def 1;

                  hence thesis by A55;

                end;

                ( dom f) = ( dom ( curry G)) by A53, Th8

                .= ( dom ( doms F)) by A2, A3, Th20;

                then f in ( product ( doms F)) by A56, CARD_3: 9;

                then

                 A57: f in ( dom ( Frege F)) by PARTFUN1:def 2;

                then x = ( //\ ((( Frege F) . f),L)) by A30, A54;

                then x in ( rng ( Infs ( Frege F))) by A57, Th13;

                hence thesis by XBOOLE_0:def 3;

              end;

                suppose ex j be Element of J st not (f . j) in (K . j);

                then

                consider j be Element of J such that

                 A58: not (f . j) in (K . j);

                j in J;

                then j in ( dom ( curry G)) by Th20;

                then (f . j) in ( dom (( curry G) . j)) by A53, Th9;

                then

                reconsider k = (f . j) as Element of K9;

                ( Bottom L) = (G . (j,k)) by A6, A58

                .= ((( curry G) . j) . (f . j)) by Th20;

                then ( Bottom L) in ( rng (( Frege ( curry G)) . f)) by A53, Lm5;

                then ( Bottom L) >= ( "/\" (( rng (( Frege ( curry G)) . f)),L)) by YELLOW_2: 22;

                then

                 A59: ( Bottom L) >= ( //\ ((( Frege ( curry G)) . f),L)) by YELLOW_2:def 6;

                ( Bottom L) <= ( //\ ((( Frege ( curry G)) . f),L)) by YELLOW_0: 44;

                then x = ( Bottom L) by A54, A59, ORDERS_2: 2;

                then x in {( Bottom L)} by TARSKI:def 1;

                hence thesis by XBOOLE_0:def 3;

              end;

            end;

            

             A60: ( Bottom L) <= ( Sup ( Infs ( Frege F))) by YELLOW_0: 44;

            ( Sup ( Infs ( Frege ( curry G)))) = ( sup ( rng ( Infs ( Frege ( curry G))))) by YELLOW_2:def 5

            .= ( sup (( rng ( Infs ( Frege F))) \/ {( Bottom L)})) by A52, A41, XBOOLE_0:def 10

            .= (( sup ( rng ( Infs ( Frege F)))) "\/" ( sup {( Bottom L)})) by A51, YELLOW_2: 3

            .= (( sup ( rng ( Infs ( Frege F)))) "\/" ( Bottom L)) by YELLOW_0: 39

            .= (( Sup ( Infs ( Frege F))) "\/" ( Bottom L)) by YELLOW_2:def 5

            .= ( Sup ( Infs ( Frege F))) by A60, YELLOW_0: 24;

            hence thesis;

          end;

        end;

        assume

         A61: for j be Element of J holds ( rng (F . j)) is directed;

        

         A62: for j be Element of J holds ( rng (( curry G) . j)) is directed

        proof

          let j be Element of J;

          set X = ( rng (( curry G) . j));

          for x,y be Element of L st x in X & y in X holds ex z be Element of L st z in X & x <= z & y <= z

          proof

            

             A63: ( rng (F . j)) is directed by A61;

            let x,y be Element of L;

            assume that

             A64: x in X and

             A65: y in X;

            consider b be object such that

             A66: b in ( dom (( curry G) . j)) and

             A67: ((( curry G) . j) . b) = y by A65, FUNCT_1:def 3;

            consider a be object such that

             A68: a in ( dom (( curry G) . j)) and

             A69: ((( curry G) . j) . a) = x by A64, FUNCT_1:def 3;

            reconsider a9 = a, b9 = b as Element of K9 by A68, A66;

            

             A70: x = (G . (j,a9)) by A69, Th20;

            

             A71: y = (G . (j,b9)) by A67, Th20;

            per cases ;

              suppose

               A72: a in (K . j) & b in (K . j);

              then b in ( dom (F . j)) & y = ((F . j) . b9) by A6, A71, FUNCT_2:def 1;

              then

               A73: y in ( rng (F . j)) by FUNCT_1:def 3;

              a in ( dom (F . j)) & x = ((F . j) . a9) by A6, A70, A72, FUNCT_2:def 1;

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

              then

              consider z be Element of L such that

               A74: z in ( rng (F . j)) & x <= z & y <= z by A63, A73, WAYBEL_0:def 1;

              take z;

              ( rng (F . j)) c= X by A9;

              hence thesis by A74;

            end;

              suppose

               A75: a in (K . j) & not b in (K . j);

              take x;

              y = ( Bottom L) by A6, A71, A75;

              hence thesis by A64, YELLOW_0: 44;

            end;

              suppose

               A76: not a in (K . j) & b in (K . j);

              take y;

              x = ( Bottom L) by A6, A70, A76;

              hence thesis by A65, YELLOW_0: 44;

            end;

              suppose

               A77: not a in (K . j) & not b in (K . j);

              take x;

              x = ( Bottom L) by A6, A70, A77;

              hence thesis by A6, A64, A71, A77;

            end;

          end;

          hence thesis by WAYBEL_0:def 1;

        end;

        ( dom F) = J by PARTFUN1:def 2

        .= ( dom ( curry G)) by PARTFUN1:def 2;

        

        hence ( Inf ( Sups F)) = ( Inf ( Sups ( curry G))) by A15, Th11

        .= ( Sup ( Infs ( Frege F))) by A1, A62, A35;

      end;

      hence thesis by Lm9;

    end;

    theorem :: WAYBEL_5:21

    L is continuous iff for J,K be non empty set holds for F be Function of [:J, K:], the carrier of L st for j be Element of J holds ( rng (( curry F) . j)) is directed holds ( Inf ( Sups ( curry F))) = ( Sup ( Infs ( Frege ( curry F)))) by Lm8, Lm10;

    

     Lm11: for f be Function st f in ( Funcs (J,( Fin K))) holds for j holds (f . j) is finite Subset of K

    proof

      let f be Function;

      assume f in ( Funcs (J,( Fin K)));

      then

       A1: ex f9 be Function st f9 = f & ( dom f9) = J & ( rng f9) c= ( Fin K) by FUNCT_2:def 2;

      for j holds (f . j) is finite Subset of K

      proof

        let j;

        (f . j) in ( rng f) by A1, FUNCT_1:def 3;

        hence thesis by A1, FINSUB_1:def 5;

      end;

      hence thesis;

    end;

    

     Lm12: for F be Function of [:J, K:], D holds for f be non-empty ManySortedSet of J st f in ( Funcs (J,( Fin K))) holds for G be DoubleIndexedSet of f, L st for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x)) holds ( rng (G . j)) is finite Subset of ( rng (( curry F) . j))

    proof

      let F be Function of [:J, K:], D;

      let f be non-empty ManySortedSet of J;

      assume f in ( Funcs (J,( Fin K)));

      then

       A1: (f . j) is finite Subset of K by Lm11;

      let G be DoubleIndexedSet of f, L such that

       A2: for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x));

      ( rng (G . j)) c= ( rng (( curry F) . j))

      proof

        let y be object;

        assume y in ( rng (G . j));

        then

        consider k be object such that

         A3: k in ( dom (G . j)) and

         A4: y = ((G . j) . k) by FUNCT_1:def 3;

        

         A5: k in (f . j) by A3;

        then

         A6: k in K by A1;

        reconsider k as Element of K by A1, A5;

        

         A7: k in ( dom (( curry F) . j)) by A6, Th20;

        y = (F . (j,k)) by A2, A3, A4

        .= ((( curry F) . j) . k) by Th20;

        hence thesis by A7, FUNCT_1:def 3;

      end;

      hence thesis by A1;

    end;

    theorem :: WAYBEL_5:22

    

     Th22: for F be Function of [:J, K:], the carrier of L holds for X be Subset of L st X = { a where a be Element of L : ex f be non-empty ManySortedSet of J st f in ( Funcs (J,( Fin K))) & ex G be DoubleIndexedSet of f, L st (for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x))) & a = ( Inf ( Sups G)) } holds ( Inf ( Sups ( curry F))) >= ( sup X)

    proof

      let F be Function of [:J, K:], the carrier of L;

      let X be Subset of L;

      

       A1: for f be non-empty ManySortedSet of J st f in ( Funcs (J,( Fin K))) holds for G be DoubleIndexedSet of f, L st for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x)) holds for j holds ( Sup (( curry F) . j)) >= ( Sup (G . j))

      proof

        let f be non-empty ManySortedSet of J such that

         A2: f in ( Funcs (J,( Fin K)));

        let G be DoubleIndexedSet of f, L such that

         A3: for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x));

        let j;

        

         A4: ex_sup_of (( rng (( curry F) . j)),L) & ex_sup_of (( rng (G . j)),L) by YELLOW_0: 17;

        ( rng (G . j)) is Subset of ( rng (( curry F) . j)) by A2, A3, Lm12;

        then ( sup ( rng (( curry F) . j))) >= ( sup ( rng (G . j))) by A4, YELLOW_0: 34;

        then ( Sup (( curry F) . j)) >= ( sup ( rng (G . j))) by YELLOW_2:def 5;

        hence thesis by YELLOW_2:def 5;

      end;

      

       A5: for f be non-empty ManySortedSet of J st f in ( Funcs (J,( Fin K))) holds for G be DoubleIndexedSet of f, L st for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x)) holds ( Inf ( Sups ( curry F))) >= ( Inf ( Sups G))

      proof

        let f be non-empty ManySortedSet of J such that

         A6: f in ( Funcs (J,( Fin K)));

        let G be DoubleIndexedSet of f, L such that

         A7: for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x));

        ( rng ( Sups ( curry F))) is_>=_than ( Inf ( Sups G))

        proof

          let a;

          assume a in ( rng ( Sups ( curry F)));

          then

          consider j be Element of J such that

           A8: a = ( Sup (( curry F) . j)) by Th14;

          ( Sup (G . j)) in ( rng ( Sups G)) by Th14;

          then ( Sup (G . j)) >= ( inf ( rng ( Sups G))) by YELLOW_2: 22;

          then

           A9: ( Sup (G . j)) >= ( Inf ( Sups G)) by YELLOW_2:def 6;

          ( Sup (( curry F) . j)) >= ( Sup (G . j)) by A1, A6, A7;

          hence thesis by A8, A9, ORDERS_2: 3;

        end;

        then ( inf ( rng ( Sups ( curry F)))) >= ( Inf ( Sups G)) by YELLOW_0: 33;

        hence thesis by YELLOW_2:def 6;

      end;

      assume

       A10: X = { a where a be Element of L : ex f be non-empty ManySortedSet of J st f in ( Funcs (J,( Fin K))) & ex G be DoubleIndexedSet of f, L st (for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x))) & a = ( Inf ( Sups G)) };

      ( Inf ( Sups ( curry F))) is_>=_than X

      proof

        let a;

        assume a in X;

        then ex a9 be Element of L st a9 = a & ex f be non-empty ManySortedSet of J st f in ( Funcs (J,( Fin K))) & ex G be DoubleIndexedSet of f, L st (for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x))) & a9 = ( Inf ( Sups G)) by A10;

        hence thesis by A5;

      end;

      hence thesis by YELLOW_0: 32;

    end;

    

     Lm13: L is continuous implies for J, K holds for F be Function of [:J, K:], the carrier of L holds for X be Subset of L st X = { a where a be Element of L : ex f be non-empty ManySortedSet of J st f in ( Funcs (J,( Fin K))) & ex G be DoubleIndexedSet of f, L st (for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x))) & a = ( Inf ( Sups G)) } holds ( Inf ( Sups ( curry F))) = ( sup X)

    proof

      assume

       A1: L is continuous;

      hereby

        let J, K;

        set FIK = { A where A be Subset of K : A is finite & A <> {} };

        set k = the Element of K;

         {k} in FIK;

        then

        reconsider FIK as non empty set;

        let F be Function of [:J, K:], the carrier of L;

        let X be Subset of L;

        set N = ( Funcs (J,FIK));

        deffunc F( Element of J, Element of N) = ( sup ((( curry F) . $1) .: ($2 . $1)));

        ex H be Function of [:J, N:], the carrier of L st for j be Element of J holds for g be Element of N holds (H . (j,g)) = F(j,g) from BINOP_1:sch 4;

        then

        consider H be Function of [:J, N:], the carrier of L such that

         A2: for j holds for g be Element of N holds (H . (j,g)) = ( sup ((( curry F) . j) .: (g . j)));

        set cF = ( curry F), cH = ( curry H);

        

         A3: for j holds (for Y be finite Subset of ( rng (cF . j)) st Y <> {} holds ex_sup_of (Y,L)) & (for x be Element of L st x in ( rng (cH . j)) holds ex Y be finite Subset of ( rng (cF . j)) st ex_sup_of (Y,L) & x = ( "\/" (Y,L))) & for Y be finite Subset of ( rng (cF . j)) st Y <> {} holds ( "\/" (Y,L)) in ( rng (cH . j))

        proof

          let j;

          set D = ( rng (( curry H) . j)), R = ( rng (( curry F) . j));

          set Hj = (( curry H) . j), Fj = (( curry F) . j);

          thus for Y be finite Subset of R st Y <> {} holds ex_sup_of (Y,L) by YELLOW_0: 17;

          thus for x be Element of L st x in D holds ex Y be finite Subset of R st ex_sup_of (Y,L) & x = ( "\/" (Y,L))

          proof

            let x be Element of L;

            assume x in D;

            then

            consider g be object such that

             A4: g in ( dom Hj) and

             A5: (Hj . g) = x by FUNCT_1:def 3;

            reconsider g as Element of N by A4;

            (g . j) in FIK;

            then ex A be Subset of K st A = (g . j) & A is finite & A <> {} ;

            then

            reconsider Y = (Fj .: (g . j)) as finite Subset of R by RELAT_1: 111;

            take Y;

            x = (H . (j,g)) by A5, Th20

            .= ( sup (Fj .: (g . j))) by A2;

            hence thesis by YELLOW_0: 17;

          end;

          thus for Y be finite Subset of R st Y <> {} holds ( "\/" (Y,L)) in D

          proof

            let Y be finite Subset of R;

            consider Z be set such that

             A6: Z c= ( dom Fj) and

             A7: Z is finite and

             A8: (Fj .: Z) = Y by ORDERS_1: 85;

            

             A9: Z c= K by A6, Th20;

            assume Y <> {} ;

            then Z <> {} by A8;

            then Z in FIK by A7, A9;

            then

             A10: {Z} c= FIK by ZFMISC_1: 31;

            ( dom (J --> Z)) = J & ( rng (J --> Z)) = {Z} by FUNCOP_1: 8;

            then

            reconsider g = (J --> Z) as Element of N by A10, FUNCT_2:def 2;

            

             A11: (g . j) = Z;

            g in N;

            then

             A12: g in ( dom Hj) by Th20;

            (Hj . g) = (H . (j,g)) by Th20

            .= ( "\/" (Y,L)) by A2, A8, A11;

            hence thesis by A12, FUNCT_1:def 3;

          end;

        end;

        for j holds ( rng (( curry H) . j)) is directed

        proof

          let j;

          

           A13: for Y be finite Subset of ( rng (cF . j)) st Y <> {} holds ( "\/" (Y,L)) in ( rng (cH . j)) by A3;

          (for Y be finite Subset of ( rng (cF . j)) st Y <> {} holds ex_sup_of (Y,L)) & for x be Element of L st x in ( rng (cH . j)) holds ex Y be finite Subset of ( rng (cF . j)) st ex_sup_of (Y,L) & x = ( "\/" (Y,L)) by A3;

          hence thesis by A13, WAYBEL_0: 51;

        end;

        then

         A14: ( Inf ( Sups ( curry H))) = ( Sup ( Infs ( Frege ( curry H)))) by A1, Lm8;

        

         A15: for j be object st j in ( dom ( curry F)) holds ( \\/ ((( curry F) . j),L)) = ( \\/ ((( curry H) . j),L))

        proof

          let j9 be object;

          assume j9 in ( dom ( curry F));

          then

          reconsider j = j9 as Element of J;

          

           A16: (for x be Element of L st x in ( rng (cH . j)) holds ex Y be finite Subset of ( rng (cF . j)) st ex_sup_of (Y,L) & x = ( "\/" (Y,L))) & for Y be finite Subset of ( rng (cF . j)) st Y <> {} holds ( "\/" (Y,L)) in ( rng (cH . j)) by A3;

           ex_sup_of (( rng (cF . j)),L) & for Y be finite Subset of ( rng (cF . j)) st Y <> {} holds ex_sup_of (Y,L) by YELLOW_0: 17;

          then ( sup ( rng (cF . j))) = ( sup ( rng (cH . j))) by A16, WAYBEL_0: 54;

          then ( Sup (cF . j)) = ( sup ( rng (cH . j))) by YELLOW_2:def 5;

          hence thesis by YELLOW_2:def 5;

        end;

        assume

         A17: X = { a where a be Element of L : ex f be non-empty ManySortedSet of J st f in ( Funcs (J,( Fin K))) & ex G be DoubleIndexedSet of f, L st (for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x))) & a = ( Inf ( Sups G)) };

        then

         A18: ( Inf ( Sups ( curry F))) >= ( sup X) by Th22;

        

         A19: FIK c= ( Fin K)

        proof

          let x be object;

          assume x in FIK;

          then ex A be Subset of K st x = A & A is finite & A <> {} ;

          hence thesis by FINSUB_1:def 5;

        end;

        

         A20: for h be Function-yielding Function st h in ( product ( doms ( curry H))) holds (for j holds ((( Frege h) . ( id J)) . j) = ((h . j) . j) & (h . j) in N & ((( Frege h) . ( id J)) . j) is finite non empty Subset of K) & (( Frege h) . ( id J)) is non-empty ManySortedSet of J & (( Frege h) . ( id J)) in ( Funcs (J,FIK)) & (( Frege h) . ( id J)) in ( Funcs (J,( Fin K)))

        proof

          let h be Function-yielding Function;

          set f = (( Frege h) . ( id J));

          assume h in ( product ( doms ( curry H)));

          then

           A21: h in ( dom ( Frege ( curry H))) by PARTFUN1:def 2;

          

          then

           A22: ( dom h) = ( dom ( curry H)) by Th8

          .= J by Th20;

          

           A23: for x be object st x in ( dom ( doms h)) holds (( id J) . x) in (( doms h) . x)

          proof

            let x be object;

            assume x in ( dom ( doms h));

            then

            reconsider j = x as Element of J by A22, FUNCT_6: 59;

            (h . j) in ((J --> N) . j) by A21, Lm6;

            then (h . j) in N;

            then ex g be Function st g = (h . j) & ( dom g) = J & ( rng g) c= FIK by FUNCT_2:def 2;

            then (( id J) . j) = j & (( doms h) . j) = J by A22, FUNCT_6: 22;

            hence thesis;

          end;

          ( dom ( id J)) = J & ( dom ( doms h)) = ( dom h) by FUNCT_6: 59;

          then ( id J) in ( product ( doms h)) by A22, A23, CARD_3: 9;

          then

           A24: ( id J) in ( dom ( Frege h)) by PARTFUN1:def 2;

          then

           A25: ( dom f) = J by A22, Th8;

          then

          reconsider f9 = f as ManySortedSet of J by PARTFUN1:def 2, RELAT_1:def 18;

          thus

           A26: for j holds ((( Frege h) . ( id J)) . j) = ((h . j) . j) & (h . j) in N & ((( Frege h) . ( id J)) . j) is finite non empty Subset of K

          proof

            let j;

            

            thus

             A27: ((( Frege h) . ( id J)) . j) = ((h . j) . (( id J) . j)) by A22, A24, Th9

            .= ((h . j) . j);

            (h . j) in ((J --> N) . j) by A21, Lm6;

            hence (h . j) in N;

            then

            consider g be Function such that

             A28: g = (h . j) & ( dom g) = J and

             A29: ( rng g) c= FIK by FUNCT_2:def 2;

            (f . j) in ( rng g) by A27, A28, FUNCT_1:def 3;

            then (f . j) in FIK by A29;

            then ex A be Subset of K st (f . j) = A & A is finite & A <> {} ;

            hence thesis;

          end;

          then for j be object st j in J holds (f9 . j) is non empty;

          hence f is non-empty ManySortedSet of J by PBOOLE:def 13;

          

           A30: ( rng f) c= FIK

          proof

            let y be object;

            assume y in ( rng f);

            then

            consider j be object such that

             A31: j in ( dom f) and

             A32: y = (f . j) by FUNCT_1:def 3;

            (f . j) is finite non empty Subset of K by A26, A25, A31;

            hence thesis by A32;

          end;

          hence f in ( Funcs (J,FIK)) by A25, FUNCT_2:def 2;

          ( rng f) c= ( Fin K) by A19, A30;

          hence thesis by A25, FUNCT_2:def 2;

        end;

        

         A33: for h be Element of ( product ( doms ( curry H))) holds ( Inf (( Frege ( curry H)) . h)) <= ( sup X)

        proof

          defpred P[ object, object, object] means $1 = (F . ($3,$2));

          let h be Element of ( product ( doms ( curry H)));

          h in ( product ( doms ( curry H)));

          then

           A34: h in ( dom ( Frege ( curry H))) by PARTFUN1:def 2;

          for x be object st x in ( dom h) holds (h . x) is Function

          proof

            let x be object;

            assume

             A35: x in ( dom h);

            ( dom h) = ( dom ( curry H)) by A34, Th8

            .= J by Th20;

            then

            reconsider j = x as Element of J by A35;

            (h . j) in ((J --> N) . j) by A34, Lm6;

            then (h . j) in N;

            hence thesis;

          end;

          then

          reconsider h9 = h as Function-yielding Function by FUNCOP_1:def 6;

          reconsider f = (( Frege h9) . ( id J)) as non-empty ManySortedSet of J by A20;

          

           A36: for j be object st j in J holds for x be object st x in (f . j) holds ex y be object st y in ((J --> the carrier of L) . j) & P[y, x, j]

          proof

            let i be object;

            assume i in J;

            then

            reconsider j = i as Element of J;

            let x be object;

            assume

             A37: x in (f . i);

            (f . j) is Subset of K by A20;

            then

            reconsider k = x as Element of K by A37;

            take y = (F . [j, k]);

            thus thesis;

          end;

          ex G be ManySortedFunction of f, (J --> the carrier of L) st for j be object st j in J holds ex g be Function of (f . j), ((J --> the carrier of L) . j) st g = (G . j) & for x be object st x in (f . j) holds P[(g . x), x, j] from MSSUBFAM:sch 1( A36);

          then

          consider G be ManySortedFunction of f, (J --> the carrier of L) such that

           A38: for j be object st j in J holds ex g be Function of (f . j), ((J --> the carrier of L) . j) st g = (G . j) & for x be object st x in (f . j) holds (g . x) = (F . (j,x));

          reconsider G as DoubleIndexedSet of f, L;

          

           A39: for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x))

          proof

            let j, x;

            assume

             A40: x in (f . j);

            ex g be Function of (f . j), ((J --> the carrier of L) . j) st g = (G . j) & for x be object st x in (f . j) holds (g . x) = (F . (j,x)) by A38;

            hence thesis by A40;

          end;

          ( Inf (( Frege ( curry H)) . h)) is_<=_than ( rng ( Sups G))

          proof

            let y be Element of L;

            assume y in ( rng ( Sups G));

            then

            consider j such that

             A41: y = ( Sup (G . j)) by Th14;

            j in J;

            then

             A42: j in ( dom ( curry H)) by Th20;

            

             A43: ((( curry F) . j) .: (f . j)) c= ( rng (G . j))

            proof

              let y be object;

              assume y in ((( curry F) . j) .: (f . j));

              then

              consider x be object such that

               A44: x in ( dom (( curry F) . j)) and

               A45: x in (f . j) and

               A46: y = ((( curry F) . j) . x) by FUNCT_1:def 6;

              reconsider k = x as Element of K by A44;

              

               A47: k in ( dom (G . j)) by A45, FUNCT_2:def 1;

              y = (F . (j,k)) by A46, Th20

              .= ((G . j) . k) by A39, A45;

              hence thesis by A47, FUNCT_1:def 3;

            end;

             ex_sup_of (((( curry F) . j) .: (f . j)),L) & ex_sup_of (( rng (G . j)),L) by YELLOW_0: 17;

            then ( sup ((( curry F) . j) .: (f . j))) <= ( sup ( rng (G . j))) by A43, YELLOW_0: 34;

            then

             A48: ( sup ((( curry F) . j) .: (f . j))) <= ( Sup (G . j)) by YELLOW_2:def 5;

            (h . j) in ((J --> N) . j) by A34, Lm6;

            then

            reconsider hj = (h . j) as Element of N;

            

             A49: ( Inf (( Frege ( curry H)) . h)) <= ((( Frege ( curry H)) . h) . j) by YELLOW_2: 53;

            ( sup ((( curry F) . j) .: (f . j))) = ( sup ((( curry F) . j) .: (hj . j))) by A20

            .= (H . (j,hj)) by A2

            .= ((( curry H) . j) . (h . j)) by Th20

            .= ((( Frege ( curry H)) . h) . j) by A34, A42, Th9;

            hence ( Inf (( Frege ( curry H)) . h)) <= y by A41, A48, A49, ORDERS_2: 3;

          end;

          then ( Inf (( Frege ( curry H)) . h)) <= ( inf ( rng ( Sups G))) by YELLOW_0: 33;

          then

           A50: ( Inf (( Frege ( curry H)) . h)) <= ( Inf ( Sups G)) by YELLOW_2:def 6;

          f in ( Funcs (J,( Fin K))) by A20;

          then ( Inf ( Sups G)) in X by A17, A39;

          then ( Inf ( Sups G)) <= ( sup X) by YELLOW_2: 22;

          hence thesis by A50, ORDERS_2: 3;

        end;

        ( rng ( Infs ( Frege ( curry H)))) is_<=_than ( sup X)

        proof

          let x be Element of L;

          assume x in ( rng ( Infs ( Frege ( curry H))));

          then

          consider h be object such that

           A51: h in ( dom ( Frege ( curry H))) and

           A52: x = ( //\ ((( Frege ( curry H)) . h),L)) by Th13;

          reconsider h as Element of ( product ( doms ( curry H))) by A51;

          ( Inf (( Frege ( curry H)) . h)) <= ( sup X) by A33;

          hence thesis by A52;

        end;

        then

         A53: ( sup ( rng ( Infs ( Frege ( curry H))))) <= ( sup X) by YELLOW_0: 32;

        ( dom ( curry F)) = J by Th20

        .= ( dom ( curry H)) by Th20;

        then ( Inf ( Sups ( curry F))) = ( Inf ( Sups ( curry H))) by A15, Th11;

        then ( Inf ( Sups ( curry F))) <= ( sup X) by A14, A53, YELLOW_2:def 5;

        hence ( Inf ( Sups ( curry F))) = ( sup X) by A18, ORDERS_2: 2;

      end;

    end;

    

     Lm14: (for J, K holds for F be Function of [:J, K:], the carrier of L holds for X be Subset of L st X = { a where a be Element of L : ex f be non-empty ManySortedSet of J st f in ( Funcs (J,( Fin K))) & ex G be DoubleIndexedSet of f, L st (for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x))) & a = ( Inf ( Sups G)) } holds ( Inf ( Sups ( curry F))) = ( sup X)) implies L is continuous

    proof

      assume

       A1: for J, K holds for F be Function of [:J, K:], the carrier of L holds for X be Subset of L st X = { a where a be Element of L : ex f be non-empty ManySortedSet of J st f in ( Funcs (J,( Fin K))) & ex G be DoubleIndexedSet of f, L st (for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x))) & a = ( Inf ( Sups G)) } holds ( Inf ( Sups ( curry F))) = ( sup X);

      for J, K holds for F be Function of [:J, K:], the carrier of L st for j be Element of J holds ( rng (( curry F) . j)) is directed holds ( Inf ( Sups ( curry F))) = ( Sup ( Infs ( Frege ( curry F))))

      proof

        let J, K;

        let F be Function of [:J, K:], the carrier of L such that

         A2: for j be Element of J holds ( rng (( curry F) . j)) is directed;

        defpred P[ Element of L] means ex f be non-empty ManySortedSet of J st f in ( Funcs (J,( Fin K))) & ex G be DoubleIndexedSet of f, L st (for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x))) & $1 = ( Inf ( Sups G));

        reconsider X = { a where a be Element of L : P[a] } as Subset of L from DOMAIN_1:sch 7;

        X is_<=_than ( Sup ( Infs ( Frege ( curry F))))

        proof

          let a9 be Element of L;

          assume a9 in X;

          then

          consider a be Element of L such that

           A3: a9 = a and

           A4: ex f be non-empty ManySortedSet of J st f in ( Funcs (J,( Fin K))) & ex G be DoubleIndexedSet of f, L st (for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x))) & a = ( Inf ( Sups G));

          defpred P[ object, object] means $1 in J & $2 in K & ex b st b = ((( curry F) . $1) . $2) & a <= b;

          consider f be non-empty ManySortedSet of J such that

           A5: f in ( Funcs (J,( Fin K))) and

           A6: ex G be DoubleIndexedSet of f, L st (for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x))) & a = ( Inf ( Sups G)) by A4;

          consider G be DoubleIndexedSet of f, L such that

           A7: for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x)) and

           A8: a = ( Inf ( Sups G)) by A6;

          

           A9: for x be object st x in J holds ex y be object st y in K & P[x, y]

          proof

            let x be object;

            assume x in J;

            then

            reconsider j = x as Element of J;

            ( Sup (G . j)) in ( rng ( Sups G)) by Th14;

            then ( inf ( rng ( Sups G))) <= ( Sup (G . j)) by YELLOW_2: 22;

            then

             A10: ( Inf ( Sups G)) <= ( Sup (G . j)) by YELLOW_2:def 6;

            ( rng (( curry F) . j)) is non empty directed & ( rng (G . j)) is finite Subset of ( rng (( curry F) . j)) by A2, A5, A7, Lm12;

            then

            consider y be Element of L such that

             A11: y in ( rng (( curry F) . j)) and

             A12: ( rng (G . j)) is_<=_than y by WAYBEL_0: 1;

            consider k be object such that

             A13: k in ( dom (( curry F) . j)) and

             A14: y = ((( curry F) . j) . k) by A11, FUNCT_1:def 3;

            reconsider k as Element of K by A13;

            take k;

            ( sup ( rng (G . j))) <= y by A12, YELLOW_0: 32;

            then ( Sup (G . j)) <= y by YELLOW_2:def 5;

            hence thesis by A8, A14, A10, ORDERS_2: 3;

          end;

          consider g be Function such that

           A15: ( dom g) = J and ( rng g) c= K and

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

          

           A17: ( dom ( doms ( curry F))) = ( dom ( curry F)) by FUNCT_6: 59;

          then

           A18: ( dom g) = ( dom ( doms ( curry F))) by A15, Th20;

          for x be object st x in ( dom ( doms ( curry F))) holds (g . x) in (( doms ( curry F)) . x)

          proof

            let x be object;

            assume x in ( dom ( doms ( curry F)));

            then

            reconsider j = x as Element of J by A17;

            ( dom ( curry F)) = J by Th20;

            

            then (( doms ( curry F)) . j) = ( dom (( curry F) . j)) by FUNCT_6: 22

            .= K by Th20;

            hence thesis by A16;

          end;

          then

          reconsider g as Element of ( product ( doms ( curry F))) by A18, CARD_3: 9;

          for j holds a <= ((( Frege ( curry F)) . g) . j)

          proof

            let j;

            

             A19: ex b st b = ((( curry F) . j) . (g . j)) & a <= b by A16;

            ( dom ( Frege ( curry F))) = ( product ( doms ( curry F))) & J = ( dom ( curry F)) by PARTFUN1:def 2;

            hence thesis by A19, Th9;

          end;

          then

           A20: a <= ( Inf (( Frege ( curry F)) . g)) by YELLOW_2: 55;

          ( Inf (( Frege ( curry F)) . g)) in ( rng ( Infs ( Frege ( curry F)))) by Th14;

          then ( Inf (( Frege ( curry F)) . g)) <= ( sup ( rng ( Infs ( Frege ( curry F))))) by YELLOW_2: 22;

          then ( Inf (( Frege ( curry F)) . g)) <= ( Sup ( Infs ( Frege ( curry F)))) by YELLOW_2:def 5;

          hence a9 <= ( Sup ( Infs ( Frege ( curry F)))) by A3, A20, ORDERS_2: 3;

        end;

        then ( sup X) <= ( Sup ( Infs ( Frege ( curry F)))) by YELLOW_0: 32;

        then

         A21: ( Inf ( Sups ( curry F))) <= ( Sup ( Infs ( Frege ( curry F)))) by A1;

        ( Inf ( Sups ( curry F))) >= ( Sup ( Infs ( Frege ( curry F)))) by Th16;

        hence thesis by A21, ORDERS_2: 2;

      end;

      hence thesis by Lm10;

    end;

    theorem :: WAYBEL_5:23

    L is continuous iff for J, K holds for F be Function of [:J, K:], the carrier of L holds for X be Subset of L st X = { a where a be Element of L : ex f be non-empty ManySortedSet of J st f in ( Funcs (J,( Fin K))) & ex G be DoubleIndexedSet of f, L st (for j, x st x in (f . j) holds ((G . j) . x) = (F . (j,x))) & a = ( Inf ( Sups G)) } holds ( Inf ( Sups ( curry F))) = ( sup X) by Lm13, Lm14;

    begin

    definition

      let L be non empty RelStr;

      :: WAYBEL_5:def3

      attr L is completely-distributive means

      : Def3: L is complete & for J be non empty set, K be non-empty ManySortedSet of J holds for F be DoubleIndexedSet of K, L holds ( Inf ( Sups F)) = ( Sup ( Infs ( Frege F)));

    end

    reserve J for non empty set,

K for non-empty ManySortedSet of J;

    registration

      cluster -> completely-distributive for 1 -element Poset;

      coherence

      proof

        let L be 1 -element Poset;

        reconsider L9 = L as complete LATTICE;

        thus L is complete;

        reconsider L9 as continuous LATTICE;

        for J be non empty set, K be non-empty ManySortedSet of J holds for F be DoubleIndexedSet of K, L9 holds ( Inf ( Sups F)) = ( Sup ( Infs ( Frege F)))

        proof

          let J be non empty set, K be non-empty ManySortedSet of J;

          let F be DoubleIndexedSet of K, L9;

          for j be Element of J holds ( rng (F . j)) is directed;

          hence thesis by Lm8;

        end;

        hence thesis;

      end;

    end

    registration

      cluster completely-distributive for LATTICE;

      existence

      proof

        set x = the set, R = the Order of {x};

         RelStr (# {x}, R #) is 1 -element RelStr;

        hence thesis;

      end;

    end

    theorem :: WAYBEL_5:24

    

     Th24: for L be completely-distributive LATTICE holds L is continuous

    proof

      let L be completely-distributive LATTICE;

      

       A1: for F be DoubleIndexedSet of K, L st for j be Element of J holds ( rng (F . j)) is directed holds ( Inf ( Sups F)) = ( Sup ( Infs ( Frege F))) by Def3;

      L is complete by Def3;

      hence thesis by A1, Lm9;

    end;

    registration

      cluster completely-distributive -> complete continuous for LATTICE;

      correctness by Th24;

    end

    theorem :: WAYBEL_5:25

    

     Th25: for L be non empty antisymmetric transitive with_infima RelStr holds for x be Element of L holds for X,Y be Subset of L st ex_sup_of (X,L) & ex_sup_of (Y,L) & Y = { (x "/\" y) where y be Element of L : y in X } holds (x "/\" ( sup X)) >= ( sup Y)

    proof

      let L be non empty antisymmetric transitive with_infima RelStr;

      let x be Element of L;

      let X,Y be Subset of L such that

       A1: ex_sup_of (X,L) and

       A2: ex_sup_of (Y,L) and

       A3: Y = { (x "/\" y) where y be Element of L : y in X };

      Y is_<=_than (x "/\" ( sup X))

      proof

        let y be Element of L;

        assume y in Y;

        then

        consider z be Element of L such that

         A4: y = (x "/\" z) and

         A5: z in X by A3;

        

         A6: y <= z by A4, YELLOW_0: 23;

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

        then z <= ( sup X) by A5;

        then

         A7: y <= ( sup X) by A6, YELLOW_0:def 2;

        y <= x by A4, YELLOW_0: 23;

        hence thesis by A7, YELLOW_0: 23;

      end;

      hence thesis by A2, YELLOW_0: 30;

    end;

    

     Lm15: for L be completely-distributive LATTICE holds for X be non empty Subset of L holds for x be Element of L holds (x "/\" ( sup X)) = ( "\/" ({ (x "/\" y) where y be Element of L : y in X },L))

    proof

      let L be completely-distributive LATTICE;

      let X be non empty Subset of L;

      let x be Element of L;

      set A = { (x "/\" y) where y be Element of L : y in X };

      set J = {1, 2}, K = ((1,2) --> ( {1},X));

      set F = ((1,2) --> (( {1} --> x),( id X)));

      

       A1: (F . 1) = ( {1} --> x) by FUNCT_4: 63;

      

       A2: ( dom K) = J by FUNCT_4: 62;

      

       A3: (K . 2) = X by FUNCT_4: 63;

      

       A4: ( dom F) = J by FUNCT_4: 62;

      reconsider j1 = 1, j2 = 2 as Element of J by TARSKI:def 2;

      

       A5: (F . 2) = ( id X) by FUNCT_4: 63;

      reconsider F as ManySortedSet of J by A4, PARTFUN1:def 2, RELAT_1:def 18;

      

       A6: (K . 1) = {1} by FUNCT_4: 63;

      reconsider K as ManySortedSet of J by A2, PARTFUN1:def 2, RELAT_1:def 18;

      for i be object holds i in J implies (K . i) is non empty by A6, A3, TARSKI:def 2;

      then

      reconsider K as non-empty ManySortedSet of J by PBOOLE:def 13;

      for j be object st j in J holds (F . j) is Function of (K . j), ((J --> the carrier of L) . j)

      proof

        let j be object;

        assume

         A7: j in J;

        then

         A8: ((J --> the carrier of L) . j) = the carrier of L by FUNCOP_1: 7;

        per cases by A7, TARSKI:def 2;

          suppose j = 1;

          hence thesis by A1, A6, A7, FUNCOP_1: 7;

        end;

          suppose j = 2;

          hence thesis by A5, A3, A8, FUNCT_2: 7;

        end;

      end;

      then

      reconsider F as DoubleIndexedSet of K, L by PBOOLE:def 15;

      ( rng ( Infs ( Frege F))) is_<=_than ( "\/" ({ (x "/\" y) where y be Element of L : y in X },L))

      proof

        let y be Element of L;

        assume y in ( rng ( Infs ( Frege F)));

        then

        consider f be object such that

         A9: f in ( dom ( Frege F)) and

         A10: y = ( //\ ((( Frege F) . f),L)) by Th13;

        reconsider f as Function by A9;

        

         A11: (f . j2) in (K . j2) by A9, Lm6;

        then

        reconsider f2 = (f . 2) as Element of X by FUNCT_4: 63;

        

         A12: (f . j1) in (K . j1) by A9, Lm6;

        

         A13: {x, f2} c= ( rng (( Frege F) . f))

        proof

          let z be object;

          assume z in {x, f2};

          then z = x or z = (f . 2) by TARSKI:def 2;

          then z = ((F . j1) . (f . j1)) or z = ((F . j2) . (f . j2)) by A1, A5, A6, A3, A12, A11, FUNCOP_1: 7, FUNCT_1: 18;

          hence thesis by A9, Lm5;

        end;

        (x "/\" f2) in A;

        then

         A14: (x "/\" f2) <= ( "\/" (A,L)) by YELLOW_2: 22;

        

         A15: ex_inf_of (( rng (( Frege F) . f)),L) & ex_inf_of ( {x, (f . 2)},L) by YELLOW_0: 17;

        y = ( "/\" (( rng (( Frege F) . f)),L)) by A10, YELLOW_2:def 6;

        then y <= ( inf {x, f2}) by A15, A13, YELLOW_0: 35;

        then y <= (x "/\" f2) by YELLOW_0: 40;

        hence thesis by A14, YELLOW_0:def 2;

      end;

      then ( sup ( rng ( Infs ( Frege F)))) <= ( "\/" ({ (x "/\" y) where y be Element of L : y in X },L)) by YELLOW_0: 32;

      then

       A16: ( Sup ( Infs ( Frege F))) <= ( "\/" ({ (x "/\" y) where y be Element of L : y in X },L)) by YELLOW_2:def 5;

      ((x "/\" ) .: X) = A by WAYBEL_1: 61;

      then

      reconsider A9 = A as Subset of L;

       ex_sup_of (X,L) & ex_sup_of (A9,L) by YELLOW_0: 17;

      then

       A17: (x "/\" ( sup X)) >= ( sup A9) by Th25;

      (x "/\" ( sup X)) is_<=_than ( rng ( Sups F))

      proof

        let y be Element of L;

        assume y in ( rng ( Sups F));

        then

        consider j be Element of J such that

         A18: y = ( Sup (F . j)) by Th14;

        per cases by TARSKI:def 2;

          suppose j = 1;

          then ( rng (F . j)) = {x} by A1, FUNCOP_1: 8;

          then ( Sup (F . j)) = ( sup {x}) by YELLOW_2:def 5;

          then y = x by A18, YELLOW_0: 39;

          hence (x "/\" ( sup X)) <= y by YELLOW_0: 23;

        end;

          suppose j = 2;

          then ( rng (F . j)) = X by A5;

          then y = ( sup X) by A18, YELLOW_2:def 5;

          hence (x "/\" ( sup X)) <= y by YELLOW_0: 23;

        end;

      end;

      then (x "/\" ( sup X)) <= ( inf ( rng ( Sups F))) by YELLOW_0: 33;

      then (x "/\" ( sup X)) <= ( Inf ( Sups F)) by YELLOW_2:def 6;

      then (x "/\" ( sup X)) <= ( Sup ( Infs ( Frege F))) by Def3;

      then (x "/\" ( sup X)) <= ( "\/" ({ (x "/\" y) where y be Element of L : y in X },L)) by A16, YELLOW_0:def 2;

      hence thesis by A17, YELLOW_0:def 3;

    end;

    theorem :: WAYBEL_5:26

    

     Th26: for L be completely-distributive LATTICE holds for X be Subset of L holds for x be Element of L holds (x "/\" ( sup X)) = ( "\/" ({ (x "/\" y) where y be Element of L : y in X },L))

    proof

      let L be completely-distributive LATTICE;

      let X be Subset of L;

      let x be Element of L;

      set A = { (x "/\" y) where y be Element of L : y in X };

      per cases ;

        suppose

         A1: X is empty;

        now

          set z = the Element of A;

          assume A <> {} ;

          then z in A;

          then ex y be Element of L st z = (x "/\" y) & y in X;

          hence contradiction by A1;

        end;

        then

         A2: ( "\/" (A,L)) = ( Bottom L) by YELLOW_0:def 11;

        ( sup X) = ( Bottom L) by A1, YELLOW_0:def 11;

        hence thesis by A2, WAYBEL_1: 3;

      end;

        suppose X is non empty;

        hence thesis by Lm15;

      end;

    end;

    registration

      cluster completely-distributive -> Heyting for LATTICE;

      correctness

      proof

        let L be LATTICE;

        assume L is completely-distributive;

        then

        reconsider L as completely-distributive LATTICE;

        for X be Subset of L holds for x be Element of L holds (x "/\" ( sup X)) = ( "\/" ({ (x "/\" y) where y be Element of L : y in X },L)) by Th26;

        then for x be Element of L holds (x "/\" ) is lower_adjoint by WAYBEL_1: 64;

        hence thesis by WAYBEL_1:def 19;

      end;

    end

    begin

    definition

      let L be non empty RelStr;

      mode CLSubFrame of L is infs-inheriting directed-sups-inheriting non empty full SubRelStr of L;

    end

    theorem :: WAYBEL_5:27

    

     Th27: for F be DoubleIndexedSet of K, L st for j be Element of J holds ( rng (F . j)) is directed holds ( rng ( Infs ( Frege F))) is directed

    proof

      let F be DoubleIndexedSet of K, L;

      set X = ( rng ( Infs ( Frege F)));

      assume

       A1: for j be Element of J holds ( rng (F . j)) is directed;

      for x,y be Element of L st x in X & y in X holds ex z be Element of L st z in X & x <= z & y <= z

      proof

        let x,y be Element of L;

        assume that

         A2: x in X and

         A3: y in X;

        consider h be object such that

         A4: h in ( dom ( Frege F)) and

         A5: y = ( //\ ((( Frege F) . h),L)) by A3, Th13;

        reconsider h as Function by A4;

        reconsider H = (( Frege F) . h) as Function of J, the carrier of L by A4, Th10;

        consider g be object such that

         A6: g in ( dom ( Frege F)) and

         A7: x = ( //\ ((( Frege F) . g),L)) by A2, Th13;

        reconsider g as Function by A6;

        reconsider G = (( Frege F) . g) as Function of J, the carrier of L by A6, Th10;

        

         A8: ex_inf_of (( rng (( Frege F) . g)),L) by YELLOW_0: 17;

        defpred P[ object, object] means $1 in J & $2 in (K . $1) & for c be Element of L st c = ((F . $1) . $2) holds (for a be Element of L st a = (G . $1) holds a <= c) & (for b be Element of L st b = (H . $1) holds b <= c);

        

         A9: for j be Element of J holds ex k be Element of (K . j) st (G . j) <= ((F . j) . k) & (H . j) <= ((F . j) . k)

        proof

          let j be Element of J;

          j in J;

          then

           A10: j in ( dom F) by PARTFUN1:def 2;

          then

           A11: (g . j) in ( dom (F . j)) by A6, Th9;

          j in J;

          then

           A12: j in ( dom F) by PARTFUN1:def 2;

          then (G . j) = ((F . j) . (g . j)) by A6, Th9;

          then

           A13: (G . j) in ( rng (F . j)) by A11, FUNCT_1:def 3;

          

           A14: (h . j) in ( dom (F . j)) by A4, A10, Th9;

          (H . j) = ((F . j) . (h . j)) by A4, A12, Th9;

          then

           A15: (H . j) in ( rng (F . j)) by A14, FUNCT_1:def 3;

          ( rng (F . j)) is directed Subset of L by A1;

          then

          consider c be Element of L such that

           A16: c in ( rng (F . j)) and

           A17: (G . j) <= c & (H . j) <= c by A13, A15, WAYBEL_0:def 1;

          consider k be object such that

           A18: k in ( dom (F . j)) and

           A19: c = ((F . j) . k) by A16, FUNCT_1:def 3;

          reconsider k as Element of (K . j) by A18;

          take k;

          thus thesis by A17, A19;

        end;

        

         A20: for j be object st j in J holds ex k be object st k in ( union ( rng K)) & P[j, k]

        proof

          let j9 be object;

          assume j9 in J;

          then

          reconsider j = j9 as Element of J;

          consider k be Element of (K . j) such that

           A21: (G . j) <= ((F . j) . k) & (H . j) <= ((F . j) . k) by A9;

          take k;

          j in J;

          then j in ( dom K) by PARTFUN1:def 2;

          then (K . j) in ( rng K) by FUNCT_1:def 3;

          hence k in ( union ( rng K)) by TARSKI:def 4;

          thus thesis by A21;

        end;

        consider f be Function such that

         A22: ( dom f) = J and ( rng f) c= ( union ( rng K)) and

         A23: for j be object st j in J holds P[j, (f . j)] from FUNCT_1:sch 6( A20);

         A24:

        now

          let x be object;

          assume x in ( dom ( doms F));

          then

           A25: x in ( dom F) by FUNCT_6: 59;

          then

          reconsider j = x as Element of J;

          (( doms F) . x) = ( dom (F . j)) by A25, FUNCT_6: 22

          .= (K . j) by FUNCT_2:def 1;

          hence (f . x) in (( doms F) . x) by A23;

        end;

        ( dom f) = ( dom F) by A22, PARTFUN1:def 2

        .= ( dom ( doms F)) by FUNCT_6: 59;

        then f in ( product ( doms F)) by A24, CARD_3: 9;

        then

         A26: f in ( dom ( Frege F)) by PARTFUN1:def 2;

        then

        reconsider Ff = (( Frege F) . f) as Function of J, the carrier of L by Th10;

        take z = ( Inf Ff);

        thus z in X by A26, Th13;

        

         A27: x = ( "/\" (( rng (( Frege F) . g)),L)) by A7, YELLOW_2:def 6;

        now

          let j be Element of J;

          

           A28: j in J;

          then j in ( dom G) by FUNCT_2:def 1;

          then

           A29: (G . j) in ( rng G) by FUNCT_1:def 3;

          j in ( dom F) by A28, PARTFUN1:def 2;

          then ((F . j) . (f . j)) = ((( Frege F) . f) . j) by A26, Th9;

          then

           A30: (G . j) <= (Ff . j) by A23;

          x is_<=_than ( rng G) by A27, A8, YELLOW_0:def 10;

          then x <= (G . j) by A29;

          hence x <= (Ff . j) by A30, ORDERS_2: 3;

        end;

        hence x <= z by YELLOW_2: 55;

        

         A31: ex_inf_of (( rng (( Frege F) . h)),L) by YELLOW_0: 17;

        

         A32: y = ( "/\" (( rng (( Frege F) . h)),L)) by A5, YELLOW_2:def 6;

        now

          let j be Element of J;

          

           A33: j in J;

          then j in ( dom H) by FUNCT_2:def 1;

          then

           A34: (H . j) in ( rng H) by FUNCT_1:def 3;

          j in ( dom F) by A33, PARTFUN1:def 2;

          then ((F . j) . (f . j)) = ((( Frege F) . f) . j) by A26, Th9;

          then

           A35: (H . j) <= (Ff . j) by A23;

          y is_<=_than ( rng H) by A32, A31, YELLOW_0:def 10;

          then y <= (H . j) by A34;

          hence y <= (Ff . j) by A35, ORDERS_2: 3;

        end;

        hence thesis by YELLOW_2: 55;

      end;

      hence thesis by WAYBEL_0:def 1;

    end;

    theorem :: WAYBEL_5:28

    L is continuous implies for S be CLSubFrame of L holds S is continuous LATTICE

    proof

      assume

       A1: L is continuous;

      let S be CLSubFrame of L;

      reconsider L9 = L as complete LATTICE;

      

       A2: S is complete LATTICE by YELLOW_2: 30;

      for J, K holds for F be DoubleIndexedSet of K, S st for j be Element of J holds ( rng (F . j)) is directed holds ( Inf ( Sups F)) = ( Sup ( Infs ( Frege F)))

      proof

        let J, K;

        let F be DoubleIndexedSet of K, S such that

         A3: for j be Element of J holds ( rng (F . j)) is directed;

        now

          let j be object;

          assume j in J;

          then

          reconsider j9 = j as Element of J;

          

           A5: (F . j9) is Function of (K . j9), the carrier of S & the carrier of S c= the carrier of L by YELLOW_0:def 13;

          thus (F . j) is Function of (K . j), ((J --> the carrier of L) . j) by A5, FUNCT_2: 7;

        end;

        then

        reconsider F9 = F as DoubleIndexedSet of K, L by PBOOLE:def 15;

         ex_inf_of (( rng ( Sups F)),L) by YELLOW_0: 17;

        then

         A6: ( "/\" (( rng ( Sups F)),L)) in the carrier of S by YELLOW_0:def 18;

        now

          let x be object;

          assume x in ( rng ( Sups F9));

          then

          consider j be Element of J such that

           A7: x = ( Sup (F9 . j)) by Th14;

          

           A8: ex_sup_of (( rng (F . j)),L9) & ( rng (F . j)) is directed Subset of S by A3, YELLOW_0: 17;

          x = ( sup ( rng (F9 . j))) by A7, YELLOW_2:def 5

          .= ( sup ( rng (F . j))) by A8, WAYBEL_0: 7

          .= ( Sup (F . j)) by YELLOW_2:def 5;

          hence x in ( rng ( Sups F)) by Th14;

        end;

        then

         A9: ( rng ( Sups F9)) c= ( rng ( Sups F));

        now

          let x be object;

          assume x in ( rng ( Sups F));

          then

          consider j be Element of J such that

           A10: x = ( Sup (F . j)) by Th14;

          

           A11: ex_sup_of (( rng (F . j)),L9) & ( rng (F . j)) is directed Subset of S by A3, YELLOW_0: 17;

          x = ( sup ( rng (F . j))) by A10, YELLOW_2:def 5

          .= ( sup ( rng (F9 . j))) by A11, WAYBEL_0: 7

          .= ( Sup (F9 . j)) by YELLOW_2:def 5;

          hence x in ( rng ( Sups F9)) by Th14;

        end;

        then ( rng ( Sups F)) c= ( rng ( Sups F9));

        then ex_inf_of (( rng ( Sups F9)),L9) & ( rng ( Sups F9)) = ( rng ( Sups F)) by A9, XBOOLE_0:def 10, YELLOW_0: 17;

        then ( inf ( rng ( Sups F9))) = ( inf ( rng ( Sups F))) by A6, YELLOW_0: 63;

        then

         A12: ( Inf ( Sups F9)) = ( inf ( rng ( Sups F))) by YELLOW_2:def 6;

        now

          let x be object;

          assume x in ( rng ( Infs ( Frege F)));

          then

          consider f be object such that

           A13: f in ( dom ( Frege F)) and

           A14: x = ( //\ ((( Frege F) . f),S)) by Th13;

          reconsider f as Function by A13;

          (( Frege F) . f) is Function of J, the carrier of S by A13, Th10;

          then

           A15: ( rng (( Frege F) . f)) c= the carrier of S by RELAT_1:def 19;

          

           A16: ex_inf_of (( rng (( Frege F) . f)),L9) by YELLOW_0: 17;

          then

           A17: ( "/\" (( rng (( Frege F) . f)),L)) in the carrier of S by A15, YELLOW_0:def 18;

          x = ( "/\" (( rng (( Frege F) . f)),S)) by A14, YELLOW_2:def 6

          .= ( "/\" (( rng (( Frege F9) . f)),L)) by A15, A16, A17, YELLOW_0: 63

          .= ( //\ ((( Frege F9) . f),L)) by YELLOW_2:def 6;

          hence x in ( rng ( Infs ( Frege F9))) by A13, Th13;

        end;

        then

         A18: ( rng ( Infs ( Frege F))) c= ( rng ( Infs ( Frege F9)));

        now

          let x be object;

          assume x in ( rng ( /\\ (( Frege F9),L)));

          then

          consider f be object such that

           A19: f in ( dom ( Frege F9)) and

           A20: x = ( //\ ((( Frege F9) . f),L)) by Th13;

          reconsider f as Element of ( product ( doms F9)) by A19;

          (( Frege F) . f) is Function of J, the carrier of S by A19, Th10;

          then

           A21: ( rng (( Frege F) . f)) c= the carrier of S by RELAT_1:def 19;

          

           A22: ex_inf_of (( rng (( Frege F) . f)),L9) by YELLOW_0: 17;

          then

           A23: ( "/\" (( rng (( Frege F) . f)),L)) in the carrier of S by A21, YELLOW_0:def 18;

          x = ( "/\" (( rng (( Frege F9) . f)),L)) by A20, YELLOW_2:def 6

          .= ( "/\" (( rng (( Frege F) . f)),S)) by A21, A22, A23, YELLOW_0: 63

          .= ( //\ ((( Frege F) . f),S)) by YELLOW_2:def 6;

          hence x in ( rng ( Infs ( Frege F))) by A19, Th13;

        end;

        then ( rng ( /\\ (( Frege F9),L))) c= ( rng ( /\\ (( Frege F),S)));

        then

         A24: ( rng ( Infs ( Frege F9))) = ( rng ( Infs ( Frege F))) by A18, XBOOLE_0:def 10;

        for j be Element of J holds ( rng (F9 . j)) is directed

        proof

          let j be Element of J;

          ( rng (F . j)) is directed by A3;

          hence thesis by YELLOW_2: 7;

        end;

        then

         A25: ( Inf ( Sups F9)) = ( Sup ( Infs ( Frege F9))) by A1, Lm8;

         ex_sup_of (( rng ( /\\ (( Frege F9),L))),L9) & ( rng ( Infs ( Frege F))) is non empty directed Subset of S by A2, A3, Th27, YELLOW_0: 17;

        then ( sup ( rng ( Infs ( Frege F9)))) = ( sup ( rng ( Infs ( Frege F)))) by A24, WAYBEL_0: 7;

        

        then ( Sup ( Infs ( Frege F9))) = ( sup ( rng ( Infs ( Frege F)))) by YELLOW_2:def 5

        .= ( Sup ( Infs ( Frege F))) by YELLOW_2:def 5;

        hence thesis by A25, A12, YELLOW_2:def 6;

      end;

      hence thesis by A2, Lm9;

    end;

    theorem :: WAYBEL_5:29

    

     Th29: for S be non empty Poset st ex g be Function of L, S st g is infs-preserving onto holds S is complete LATTICE

    proof

      let S be non empty Poset;

      given g be Function of L, S such that

       A1: g is infs-preserving and

       A2: g is onto;

      for A be Subset of S holds ex_inf_of (A,S)

      proof

        let A be Subset of S;

        set Y = (g " A);

        ( rng g) = the carrier of S by A2, FUNCT_2:def 3;

        then

         A3: A = (g .: Y) by FUNCT_1: 77;

         ex_inf_of (Y,L) & g preserves_inf_of Y by A1, WAYBEL_0:def 32, YELLOW_0: 17;

        hence thesis by A3, WAYBEL_0:def 30;

      end;

      then S is complete non empty Poset by YELLOW_2: 28;

      hence thesis;

    end;

    notation

      let J be set, y be set;

      synonym J => y for J --> y;

    end

    registration

      let J be set, y be set;

      cluster (J => y) -> total;

      coherence ;

    end

    definition

      let A,B,J be set, f be Function of A, B;

      :: original: =>

      redefine

      func J => f -> ManySortedFunction of (J --> A), (J --> B) ;

      coherence

      proof

        set JA = (J --> A), JB = (J --> B);

        for j be object st j in J holds ((J => f) . j) is Function of (JA . j), (JB . j)

        proof

          let j be object;

          assume

           A1: j in J;

          then (JA . j) = A & (JB . j) = B by FUNCOP_1: 7;

          hence thesis by A1, FUNCOP_1: 7;

        end;

        hence thesis by PBOOLE:def 15;

      end;

    end

    theorem :: WAYBEL_5:30

    

     Th30: for A,B be set holds for f be Function of A, B, g be Function of B, A st (g * f) = ( id A) holds ((J => g) ** (J => f)) = ( id (J --> A))

    proof

      let A,B be set;

      let f be Function of A, B;

      let g be Function of B, A;

      set F = ((J => g) ** (J => f));

      ( dom F) = J by MSUALG_3: 2;

      then

      reconsider F as ManySortedSet of J by PARTFUN1:def 2, RELAT_1:def 18;

      assume

       A1: (g * f) = ( id A);

      

       A2: for j be object st j in J holds (F . j) = ( id ((J --> A) . j))

      proof

        let j be object;

        assume

         A3: j in J;

        then

         A4: ((J --> A) . j) = A by FUNCOP_1: 7;

        ((J => g) . j) = g & ((J => f) . j) = f by A3, FUNCOP_1: 7;

        hence thesis by A1, A3, A4, MSUALG_3: 2;

      end;

      now

        let j be object;

        assume j in J;

        then (F . j) = ( id ((J --> A) . j)) by A2;

        hence (F . j) is Function of ((J --> A) . j), ((J --> A) . j);

      end;

      then

      reconsider F as ManySortedFunction of (J --> A), (J --> A) by PBOOLE:def 15;

      for j be set st j in J holds (F . j) = ( id ((J --> A) . j)) by A2;

      hence thesis by MSUALG_3:def 1;

    end;

    theorem :: WAYBEL_5:31

    

     Th31: for J,A be non empty set, B be set, K be ManySortedSet of J holds for F be DoubleIndexedSet of K, A holds for f be Function of A, B holds ((J => f) ** F) is DoubleIndexedSet of K, B

    proof

      let J,A be non empty set;

      let B be set;

      let K be ManySortedSet of J;

      let F be DoubleIndexedSet of K, A;

      let f be Function of A, B;

      set fF = ((J => f) ** F);

      ( dom fF) = J by MSUALG_3: 2;

      then

      reconsider fF as ManySortedSet of J by PARTFUN1:def 2, RELAT_1:def 18;

      for j be object st j in J holds (fF . j) is Function of (K . j), ((J --> B) . j)

      proof

        let j be object;

        assume

         A1: j in J;

        then

        reconsider j9 = j as Element of J;

        reconsider Fj = (F . j9) as Function of (K . j), A;

        

         A2: (fF . j) = (((J => f) . j) * (F . j)) by A1, MSUALG_3: 2

        .= (f * Fj);

        thus thesis by A2;

      end;

      hence ((J --> f) ** F) is DoubleIndexedSet of K, B by PBOOLE:def 15;

    end;

    theorem :: WAYBEL_5:32

    

     Th32: for J,A,B be non empty set, K be ManySortedSet of J holds for F be DoubleIndexedSet of K, A holds for f be Function of A, B holds ( doms ((J => f) ** F)) = ( doms F)

    proof

      let J,A,B be non empty set;

      let K be ManySortedSet of J;

      let F be DoubleIndexedSet of K, A;

      let f be Function of A, B;

      

       A1: ( dom ( doms ((J => f) ** F))) = ( dom ((J => f) ** F)) by FUNCT_6: 59

      .= J by MSUALG_3: 2;

       A2:

      now

        let x be object;

        assume

         A3: x in J;

        then

        reconsider j = x as Element of J;

        

         A4: j in ( dom F) by A3, PARTFUN1:def 2;

        

         A5: ( rng (F . j)) c= A & ( dom f) = A by FUNCT_2:def 1;

        j in ( dom ((J => f) ** F)) by A1, A3, FUNCT_6: 59;

        

        then (( doms ((J => f) ** F)) . j) = ( dom (((J => f) ** F) . j)) by FUNCT_6: 22

        .= ( dom (((J => f) . j) * (F . j))) by MSUALG_3: 2

        .= ( dom (f * (F . j)))

        .= ( dom (F . j)) by A5, RELAT_1: 27

        .= (( doms F) . j) by A4, FUNCT_6: 22;

        hence (( doms ((J => f) ** F)) . x) = (( doms F) . x);

      end;

      ( dom ( doms F)) = ( dom F) by FUNCT_6: 59

      .= J by PARTFUN1:def 2;

      hence thesis by A1, A2, FUNCT_1: 2;

    end;

    theorem :: WAYBEL_5:33

    L is continuous implies for S be non empty Poset st ex g be Function of L, S st g is infs-preserving directed-sups-preserving & g is onto holds S is continuous LATTICE

    proof

      assume

       A1: L is continuous;

      let S be non empty Poset;

      given g be Function of L, S such that

       A2: g is infs-preserving directed-sups-preserving and

       A3: g is onto;

      reconsider S9 = S as complete LATTICE by A2, A3, Th29;

      for J, K holds for F be DoubleIndexedSet of K, S9 st for j be Element of J holds ( rng (F . j)) is directed holds ( Inf ( Sups F)) = ( Sup ( Infs ( Frege F)))

      proof

        let J, K;

        let F be DoubleIndexedSet of K, S9 such that

         A4: for j be Element of J holds ( rng (F . j)) is directed;

        consider d be Function of S, L such that

         A5: [g, d] is Galois and for t be Element of S holds (d . t) is_minimum_of (g " ( uparrow t)) by A2, WAYBEL_1: 14;

        reconsider dF = ((J => d) ** F) as DoubleIndexedSet of K, L by Th31;

        

         A6: ex_inf_of (( rng ( Sups dF)),L) & g preserves_inf_of ( rng ( Sups dF)) by A2, WAYBEL_0:def 32, YELLOW_0: 17;

        for t be Element of S holds (d . t) is_minimum_of (g " {t}) by A3, A5, WAYBEL_1: 22;

        then

         A7: (g * d) = ( id S) by WAYBEL_1: 23;

        

         A8: for f be set st f in ( dom ( Frege dF)) holds ( rng (( Frege F) . f)) = (g .: ( rng (( Frege dF) . f)))

        proof

          let f be set;

          assume

           A9: f in ( dom ( Frege dF));

          then

          reconsider f as Element of ( product ( doms dF));

          

           A10: ( dom ( Frege dF)) = ( product ( doms dF)) by PARTFUN1:def 2

          .= ( product ( doms F)) by Th32

          .= ( dom ( Frege F)) by PARTFUN1:def 2;

          

           A11: ( dom (( Frege dF) . f)) = ( dom dF) by A9, Th8

          .= J by PARTFUN1:def 2;

           A12:

          now

            let i be object;

            assume

             A13: i in J;

            then

            reconsider j = i as Element of J;

            

             A14: j in ( dom F) by A13, PARTFUN1:def 2;

            

             A15: j in ( dom dF) by A13, PARTFUN1:def 2;

            then (f . j) in ( dom (dF . j)) by A9, Th9;

            then (f . j) in ( dom (((J => d) . j) * (F . j))) by MSUALG_3: 2;

            then

             A16: (f . j) in ( dom (d * (F . j)));

            ((g * (( Frege dF) . f)) . j) = (g . ((( Frege dF) . f) . j)) by A11, FUNCT_1: 13

            .= (g . ((dF . j) . (f . j))) by A9, A15, Th9

            .= (g . ((((J => d) . j) * (F . j)) . (f . j))) by MSUALG_3: 2

            .= (g . ((d * (F . j)) . (f . j)))

            .= ((g * (d * (F . j))) . (f . j)) by A16, FUNCT_1: 13

            .= ((( id the carrier of S) * (F . j)) . (f . j)) by A7, RELAT_1: 36

            .= ((F . j) . (f . j)) by FUNCT_2: 17

            .= ((( Frege F) . f) . j) by A9, A10, A14, Th9;

            hence ((g * (( Frege dF) . f)) . i) = ((( Frege F) . f) . i);

          end;

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

          then ( rng (( Frege dF) . f)) c= ( dom g);

          then

           A17: ( dom (g * (( Frege dF) . f))) = ( dom (( Frege dF) . f)) by RELAT_1: 27;

          ( dom (( Frege F) . f)) = ( dom F) by A9, A10, Th8

          .= J by PARTFUN1:def 2;

          

          then ( rng (( Frege F) . f)) = ( rng (g * (( Frege dF) . f))) by A11, A17, A12, FUNCT_1: 2

          .= (g .: ( rng (( Frege dF) . f))) by RELAT_1: 127;

          hence thesis;

        end;

        

         A18: ( rng ( Infs ( Frege F))) c= (g .: ( rng ( Infs ( Frege dF))))

        proof

          let y be object;

          assume y in ( rng ( Infs ( Frege F)));

          then

          consider f be object such that

           A19: f in ( dom ( Frege F)) and

           A20: y = ( //\ ((( Frege F) . f),S)) by Th13;

          reconsider f as Element of ( product ( doms F)) by A19;

          reconsider f9 = f as Element of ( product ( doms dF)) by Th32;

          set X = ( rng (( Frege dF) . f9));

          

           A21: g preserves_inf_of X & ex_inf_of (X,L) by A2, WAYBEL_0:def 32, YELLOW_0: 17;

          

           A22: ( dom ( Frege dF)) = ( product ( doms dF)) by PARTFUN1:def 2

          .= ( product ( doms F)) by Th32

          .= ( dom ( Frege F)) by PARTFUN1:def 2;

          then ( rng (( Frege F) . f)) = (g .: ( rng (( Frege dF) . f))) by A8, A19;

          then y = ( "/\" ((g .: ( rng (( Frege dF) . f))),S)) by A20, YELLOW_2:def 6;

          

          then

           A23: y = (g . ( inf X)) by A21, WAYBEL_0:def 30

          .= (g . ( Inf (( Frege dF) . f9))) by YELLOW_2:def 6;

          ( Inf (( Frege dF) . f9)) in ( rng ( Infs ( Frege dF))) by A19, A22, Th13;

          hence thesis by A23, FUNCT_2: 35;

        end;

        

         A24: (g .: ( rng ( Infs ( Frege dF)))) c= ( rng ( Infs ( Frege F)))

        proof

          let y be object;

          assume y in (g .: ( rng ( Infs ( Frege dF))));

          then

          consider x be object such that x in the carrier of L and

           A25: x in ( rng ( Infs ( Frege dF))) and

           A26: y = (g . x) by FUNCT_2: 64;

          consider f be object such that

           A27: f in ( dom ( Frege dF)) and

           A28: x = ( //\ ((( Frege dF) . f),L)) by A25, Th13;

          reconsider f as Element of ( product ( doms dF)) by A27;

          set X = ( rng (( Frege dF) . f));

          g preserves_inf_of X & ex_inf_of (X,L) by A2, WAYBEL_0:def 32, YELLOW_0: 17;

          then ( inf (g .: X)) = (g . ( inf X)) by WAYBEL_0:def 30;

          then

           A29: y = ( inf (g .: X)) by A26, A28, YELLOW_2:def 6;

          

           A30: ( dom ( Frege dF)) = ( product ( doms dF)) by PARTFUN1:def 2

          .= ( product ( doms F)) by Th32

          .= ( dom ( Frege F)) by PARTFUN1:def 2;

          reconsider f9 = f as Element of ( product ( doms F)) by Th32;

          ( rng (( Frege F) . f)) = (g .: ( rng (( Frege dF) . f))) by A8, A27;

          then y = ( Inf (( Frege F) . f9)) by A29, YELLOW_2:def 6;

          hence thesis by A27, A30, Th13;

        end;

        

         A31: d is monotone by A5, WAYBEL_1: 8;

        

         A32: for j be Element of J holds ( rng (dF . j)) is directed

        proof

          let j be Element of J;

          ((J => d) . j) = d;

          

          then

           A33: ( rng (dF . j)) = ( rng (d * (F . j))) by MSUALG_3: 2

          .= (d .: ( rng (F . j))) by RELAT_1: 127;

          ( rng (F . j)) is directed by A4;

          hence thesis by A31, A33, YELLOW_2: 15;

        end;

        then ( rng ( Infs ( Frege dF))) is directed non empty by Th27;

        then

         A34: g preserves_sup_of ( rng ( Infs ( Frege dF))) by A2, WAYBEL_0:def 37;

        reconsider gdF = ((J => g) ** dF) as DoubleIndexedSet of K, S;

        

         A35: ex_sup_of (( rng ( Infs ( Frege dF))),L) by YELLOW_0: 17;

        

         A36: ( rng ( Sups gdF)) c= (g .: ( rng ( Sups dF)))

        proof

          let y be object;

          assume y in ( rng ( Sups gdF));

          then

          consider j be Element of J such that

           A37: y = ( Sup (gdF . j)) by Th14;

          (gdF . j) = (((J => g) . j) * (dF . j)) by MSUALG_3: 2

          .= (g * (dF . j));

          then ( rng (gdF . j)) = (g .: ( rng (dF . j))) by RELAT_1: 127;

          then

           A38: y = ( sup (g .: ( rng (dF . j)))) by A37, YELLOW_2:def 5;

          ( rng (dF . j)) is directed by A32;

          then

           A39: g preserves_sup_of ( rng (dF . j)) by A2, WAYBEL_0:def 37;

           ex_sup_of (( rng (dF . j)),L) by YELLOW_0: 17;

          then ( sup (g .: ( rng (dF . j)))) = (g . ( sup ( rng (dF . j)))) by A39, WAYBEL_0:def 31;

          then

           A40: y = (g . ( Sup (dF . j))) by A38, YELLOW_2:def 5;

          ( Sup (dF . j)) in ( rng ( Sups dF)) by Th14;

          hence thesis by A40, FUNCT_2: 35;

        end;

        

         A41: (g .: ( rng ( Sups dF))) c= ( rng ( Sups gdF))

        proof

          let y be object;

          assume y in (g .: ( rng ( Sups dF)));

          then

          consider x be object such that x in the carrier of L and

           A42: x in ( rng ( Sups dF)) and

           A43: y = (g . x) by FUNCT_2: 64;

          consider j be Element of J such that

           A44: x = ( Sup (dF . j)) by A42, Th14;

          ( rng (dF . j)) is directed by A32;

          then

           A45: g preserves_sup_of ( rng (dF . j)) by A2, WAYBEL_0:def 37;

           ex_sup_of (( rng (dF . j)),L) by YELLOW_0: 17;

          then ( sup (g .: ( rng (dF . j)))) = (g . ( sup ( rng (dF . j)))) by A45, WAYBEL_0:def 31;

          then

           A46: y = ( sup (g .: ( rng (dF . j)))) by A43, A44, YELLOW_2:def 5;

          (gdF . j) = (((J => g) . j) * (dF . j)) by MSUALG_3: 2

          .= (g * (dF . j));

          then ( rng (gdF . j)) = (g .: ( rng (dF . j))) by RELAT_1: 127;

          then y = ( Sup (gdF . j)) by A46, YELLOW_2:def 5;

          hence thesis by Th14;

        end;

        F = (( id (J --> the carrier of S)) ** F) by MSUALG_3: 4

        .= (((J --> g) ** (J --> d)) ** F) by A7, Th30

        .= gdF by PBOOLE: 140;

        

        then ( Inf ( Sups F)) = ( inf ( rng ( Sups gdF))) by YELLOW_2:def 6

        .= ( inf (g .: ( rng ( Sups dF)))) by A36, A41, XBOOLE_0:def 10

        .= (g . ( inf ( rng ( Sups dF)))) by A6, WAYBEL_0:def 30

        .= (g . ( Inf ( Sups dF))) by YELLOW_2:def 6

        .= (g . ( Sup ( Infs ( Frege dF)))) by A1, A32, Lm8

        .= (g . ( sup ( rng ( Infs ( Frege dF))))) by YELLOW_2:def 5

        .= ( sup (g .: ( rng ( Infs ( Frege dF))))) by A34, A35, WAYBEL_0:def 31

        .= ( sup ( rng ( Infs ( Frege F)))) by A24, A18, XBOOLE_0:def 10

        .= ( Sup ( Infs ( Frege F))) by YELLOW_2:def 5;

        hence thesis;

      end;

      hence thesis by Lm9;

    end;