orders_3.miz



    begin

    definition

      let IT be RelStr;

      :: ORDERS_3:def1

      attr IT is discrete means

      : Def1: the InternalRel of IT = ( id the carrier of IT);

    end

    registration

      cluster strict discrete non empty for Poset;

      existence

      proof

        set A = the non empty set;

        reconsider R = ( id A) as Relation of A;

        reconsider R as Order of A;

        take RelStr (# A, R #);

        thus thesis;

      end;

    end

    registration

      cluster RelStr (# {} , ( id {} ) #) -> empty;

      coherence ;

      let P be empty RelStr;

      cluster the InternalRel of P -> empty;

      coherence ;

    end

    registration

      cluster empty -> discrete for RelStr;

      coherence ;

    end

    definition

      let P be RelStr;

      let IT be Subset of P;

      :: ORDERS_3:def2

      attr IT is disconnected means ex A,B be Subset of P st A <> {} & B <> {} & IT = (A \/ B) & A misses B & the InternalRel of P = ((the InternalRel of P |_2 A) \/ (the InternalRel of P |_2 B));

    end

    notation

      let P be RelStr;

      let IT be Subset of P;

      antonym IT is connected for IT is disconnected;

    end

    definition

      let IT be RelStr;

      :: ORDERS_3:def3

      attr IT is disconnected means ( [#] IT) is disconnected;

    end

    notation

      let IT be RelStr;

      antonym IT is connected for IT is disconnected;

    end

    reserve T for non empty RelStr,

a for Element of T;

    theorem :: ORDERS_3:1

    for DP be discrete non empty RelStr, x,y be Element of DP holds x <= y iff x = y

    proof

      let DP be discrete non empty RelStr, x,y be Element of DP;

      hereby

        assume x <= y;

        then [x, y] in the InternalRel of DP by ORDERS_2:def 5;

        then [x, y] in ( id the carrier of DP) by Def1;

        hence x = y by RELAT_1:def 10;

      end;

      assume x = y;

      then [x, y] in ( id the carrier of DP) by RELAT_1:def 10;

      then [x, y] in the InternalRel of DP by Def1;

      hence thesis by ORDERS_2:def 5;

    end;

    theorem :: ORDERS_3:2

    for R be Relation, a be set st R is Order of {a} holds R = ( id {a})

    proof

      let R be Relation, a be set;

      assume

       A1: R is Order of {a};

      then

       A2: R <> {} ;

      R c= [: {a}, {a}:] by A1;

      then R c= { [a, a]} by ZFMISC_1: 29;

      then R = { [a, a]} by A2, ZFMISC_1: 33;

      hence thesis by SYSREL: 13;

    end;

    theorem :: ORDERS_3:3

    T is reflexive & ( [#] T) = {a} implies T is discrete

    proof

      assume

       A1: T is reflexive;

      set R = the InternalRel of T;

      assume

       A2: ( [#] T) = {a};

      R = ( id {a})

      proof

        

         A3: ( id {a}) = { [a, a]} by SYSREL: 13;

        R c= [: {a}, {a}:] by A2;

        hence R c= ( id {a}) by A3, ZFMISC_1: 29;

        let x be object;

        assume x in ( id {a});

        then

         A4: x = [a, a] by A3, TARSKI:def 1;

        a >= a by A1, ORDERS_2: 1;

        hence thesis by A4, ORDERS_2:def 5;

      end;

      hence thesis by A2;

    end;

    reserve a for set;

    theorem :: ORDERS_3:4

    

     Th4: ( [#] T) = {a} implies T is connected

    proof

      reconsider OT = ( [#] T) as non empty set;

      assume

       A1: ( [#] T) = {a};

      

       A2: for Z,Z9 be non empty Subset of OT holds not Z misses Z9

      proof

        let Z,Z9 be non empty Subset of OT;

        Z = {a} by A1, ZFMISC_1: 33;

        hence thesis by A1, ZFMISC_1: 33;

      end;

      ( [#] T) is connected by A2;

      hence thesis;

    end;

    theorem :: ORDERS_3:5

    

     Th5: for DP be discrete non empty Poset st (ex a,b be Element of DP st a <> b) holds DP is disconnected

    proof

      let DP be discrete non empty Poset;

      given a,b be Element of DP such that

       A1: a <> b;

       not b in {a} by A1, TARSKI:def 1;

      then

      reconsider A = (the carrier of DP \ {a}) as non empty Subset of DP by XBOOLE_0:def 5;

      reconsider B = {a} as non empty Subset of DP;

      

       A2: the carrier of DP = ((the carrier of DP \ {a}) \/ {a}) & (the carrier of DP \ {a}) misses {a} by XBOOLE_1: 45, XBOOLE_1: 79;

      the InternalRel of DP c= ( [:A, A:] \/ [:B, B:])

      proof

        let x be object;

        assume

         A3: x in the InternalRel of DP;

        then

        consider x1,x2 be object such that

         A4: x = [x1, x2] by RELAT_1:def 1;

        

         A5: x in ( id the carrier of DP) by A3, Def1;

        then

         A6: x1 = x2 by A4, RELAT_1:def 10;

        per cases ;

          suppose

           A7: x1 in A;

          

           A8: [:A, A:] c= ( [:A, A:] \/ [:B, B:]) by XBOOLE_1: 7;

           [x1, x1] in [:A, A:] by A7, ZFMISC_1: 87;

          hence thesis by A4, A6, A8;

        end;

          suppose

           A9: not x1 in A;

          x1 in the carrier of DP by A5, A4, RELAT_1:def 10;

          then x1 in (the carrier of DP \ A) by A9, XBOOLE_0:def 5;

          then x1 in (the carrier of DP /\ B) by XBOOLE_1: 48;

          then x1 in B by XBOOLE_1: 28;

          then

           A10: [x1, x1] in [:B, B:] by ZFMISC_1: 87;

           [:B, B:] c= ( [:A, A:] \/ [:B, B:]) by XBOOLE_1: 7;

          hence thesis by A4, A6, A10;

        end;

      end;

      then

       A11: the InternalRel of DP = (the InternalRel of DP /\ ( [:A, A:] \/ [:B, B:])) by XBOOLE_1: 28;

      (the InternalRel of DP |_2 A) = (the InternalRel of DP /\ [:A, A:]) & (the InternalRel of DP |_2 B) = (the InternalRel of DP /\ [:B, B:]) by WELLORD1:def 6;

      then the InternalRel of DP = ((the InternalRel of DP |_2 A) \/ (the InternalRel of DP |_2 B)) by A11, XBOOLE_1: 23;

      then ( [#] DP) is disconnected by A2;

      hence thesis;

    end;

    registration

      cluster strict connected for non empty Poset;

      existence

      proof

        set x = the set;

        reconsider A = RelStr (# {x}, ( id {x}) #) as non empty Poset;

        A is connected by Th4;

        hence thesis;

      end;

      cluster strict disconnected discrete for non empty Poset;

      existence

      proof

        ex Y be non empty Poset st Y is strict & Y is disconnected & Y is discrete

        proof

          reconsider A = RelStr (# {1, 2}, ( id {1, 2}) #) as non empty Poset;

          reconsider A as discrete non empty Poset by Def1;

          take A;

          ex a,b be Element of A st a <> b

          proof

            set a = 1, b = 2;

            reconsider a, b as Element of A by TARSKI:def 2;

            take a, b;

            thus thesis;

          end;

          hence thesis by Th5;

        end;

        hence thesis;

      end;

    end

    begin

    definition

      let IT be set;

      :: ORDERS_3:def4

      attr IT is POSet_set-like means

      : Def4: for a be set st a in IT holds a is non empty Poset;

    end

    registration

      cluster non empty POSet_set-like for set;

      existence

      proof

        set P = the non empty Poset;

        set A = {P};

        take A;

        for a be set st a in A holds a is non empty Poset by TARSKI:def 1;

        hence thesis;

      end;

    end

    definition

      mode POSet_set is POSet_set-like set;

    end

    definition

      let P be non empty POSet_set;

      :: original: Element

      redefine

      mode Element of P -> non empty Poset ;

      coherence by Def4;

    end

    definition

      let L1,L2 be RelStr;

      let f be Function of L1, L2;

      :: ORDERS_3:def5

      attr f is monotone means for x,y be Element of L1 st x <= y holds for a,b be Element of L2 st a = (f . x) & b = (f . y) holds a <= b;

    end

    

     Lm1: for A,B,C be non empty RelStr holds for f be Function of A, B, g be Function of B, C st f is monotone & g is monotone holds ex gf be Function of A, C st gf = (g * f) & gf is monotone

    proof

      let A,B,C be non empty RelStr;

      let f be Function of A, B, g be Function of B, C;

      assume that

       A1: f is monotone and

       A2: g is monotone;

      reconsider gf = (g * f) as Function of A, C;

      take gf;

      now

        let p1,p2 be Element of A;

        reconsider p19 = (f . p1), p29 = (f . p2) as Element of B;

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

        then

         A3: (g . (f . p1)) = ((g * f) . p1) & (g . (f . p2)) = ((g * f) . p2) by FUNCT_1: 13;

        assume p1 <= p2;

        then

         A4: p19 <= p29 by A1;

        let r1,r2 be Element of C;

        assume r1 = (gf . p1) & r2 = (gf . p2);

        hence r1 <= r2 by A2, A3, A4;

      end;

      hence thesis;

    end;

    reserve P for non empty POSet_set,

A,B for Element of P;

    definition

      let A,B be RelStr;

      :: ORDERS_3:def6

      func MonFuncs (A,B) -> set means

      : Def6: a in it iff ex f be Function of A, B st a = f & f in ( Funcs (the carrier of A,the carrier of B)) & f is monotone;

      existence

      proof

        defpred P[ object] means ex f be Function of A, B st f = $1 & f is monotone;

        consider AB be set such that

         A1: for a be object holds a in AB iff a in ( Funcs (the carrier of A,the carrier of B)) & P[a] from XBOOLE_0:sch 1;

        take AB;

        thus a in AB iff ex f be Function of A, B st a = f & f in ( Funcs (the carrier of A,the carrier of B)) & f is monotone

        proof

          hereby

            assume

             A2: a in AB;

            then

            consider f be Function of A, B such that

             A3: f = a & f is monotone by A1;

            take f;

            thus a = f & f in ( Funcs (the carrier of A,the carrier of B)) & f is monotone by A1, A2, A3;

          end;

          given f be Function of A, B such that

           A4: a = f & f in ( Funcs (the carrier of A,the carrier of B)) & f is monotone;

          thus thesis by A1, A4;

        end;

      end;

      uniqueness

      proof

        let A1,A2 be set such that

         A5: a in A1 iff ex f be Function of A, B st a = f & f in ( Funcs (the carrier of A,the carrier of B)) & f is monotone and

         A6: a in A2 iff ex f be Function of A, B st a = f & f in ( Funcs (the carrier of A,the carrier of B)) & f is monotone;

        for a be object holds a in A2 implies a in A1

        proof

          let a be object;

          assume a in A2;

          then ex f be Function of A, B st a = f & f in ( Funcs (the carrier of A,the carrier of B)) & f is monotone by A6;

          hence thesis by A5;

        end;

        then

         A7: A2 c= A1;

        for a be object holds a in A1 implies a in A2

        proof

          let a be object;

          assume a in A1;

          then ex f be Function of A, B st a = f & f in ( Funcs (the carrier of A,the carrier of B)) & f is monotone by A5;

          hence thesis by A6;

        end;

        then A1 c= A2;

        hence A1 = A2 by A7;

      end;

    end

    theorem :: ORDERS_3:6

    

     Th6: for A,B,C be non empty RelStr holds for f,g be Function st f in ( MonFuncs (A,B)) & g in ( MonFuncs (B,C)) holds (g * f) in ( MonFuncs (A,C))

    proof

      let A,B,C be non empty RelStr;

      let f,g be Function;

      assume that

       A1: f in ( MonFuncs (A,B)) and

       A2: g in ( MonFuncs (B,C));

      consider f9 be Function of A, B such that

       A3: f = f9 and f9 in ( Funcs (the carrier of A,the carrier of B)) and

       A4: f9 is monotone by A1, Def6;

      consider g9 be Function of B, C such that

       A5: g = g9 and g9 in ( Funcs (the carrier of B,the carrier of C)) and

       A6: g9 is monotone by A2, Def6;

      consider gf be Function of A, C such that

       A7: gf = (g9 * f9) & gf is monotone by A4, A6, Lm1;

      gf in ( Funcs (the carrier of A,the carrier of C)) by FUNCT_2: 8;

      hence thesis by A3, A5, A7, Def6;

    end;

    theorem :: ORDERS_3:7

    

     Th7: ( id the carrier of T) in ( MonFuncs (T,T))

    proof

      reconsider IT = ( id T) as Function of the carrier of T, the carrier of T;

      reconsider IT9 = IT as Function of T, T;

      ( id T) is monotone & IT9 in ( Funcs (the carrier of T,the carrier of T)) by FUNCT_2: 9;

      hence thesis by Def6;

    end;

    registration

      let T;

      cluster ( MonFuncs (T,T)) -> non empty;

      coherence by Th7;

    end

    definition

      let X be set;

      :: ORDERS_3:def7

      func Carr X -> set means

      : Def7: a in it iff ex s be 1-sorted st s in X & a = the carrier of s;

      existence

      proof

        defpred P[ object, object] means ex s be 1-sorted st s = $1 & $2 = the carrier of s;

        

         A1: for x,y,z be object st P[x, y] & P[x, z] holds y = z;

        consider CX be set such that

         A2: for x be object holds x in CX iff ex y be object st y in X & P[y, x] from TARSKI:sch 1( A1);

        take CX;

        let x be set;

        x in CX iff ex s be 1-sorted st s in X & x = the carrier of s

        proof

          thus x in CX implies ex s be 1-sorted st s in X & x = the carrier of s

          proof

            assume x in CX;

            then

            consider y be object such that

             A3: y in X and

             A4: ex s be 1-sorted st s = y & x = the carrier of s by A2;

            consider s be 1-sorted such that

             A5: s = y and x = the carrier of s by A4;

            take s;

            thus thesis by A3, A4, A5;

          end;

          given s be 1-sorted such that

           A6: s in X & x = the carrier of s;

          thus thesis by A2, A6;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let C1,C2 be set;

        assume that

         A7: a in C1 iff ex s be 1-sorted st s in X & a = the carrier of s and

         A8: a in C2 iff ex s be 1-sorted st s in X & a = the carrier of s;

        for a be object holds a in C1 iff a in C2

        proof

          let a be object;

          thus a in C1 implies a in C2

          proof

            assume a in C1;

            then ex s be 1-sorted st s in X & a = the carrier of s by A7;

            hence thesis by A8;

          end;

          thus a in C2 implies a in C1

          proof

            assume a in C2;

            then ex s be 1-sorted st s in X & a = the carrier of s by A8;

            hence thesis by A7;

          end;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    

     Lm2: the carrier of A in ( Carr P) by Def7;

    registration

      let P;

      cluster ( Carr P) -> non empty;

      coherence by Lm2;

    end

    theorem :: ORDERS_3:8

    for f be 1-sorted holds ( Carr {f}) = {the carrier of f}

    proof

      let f be 1-sorted;

      thus ( Carr {f}) c= {the carrier of f}

      proof

        let a be object;

        assume a in ( Carr {f});

        then

        consider s be 1-sorted such that

         A1: s in {f} and

         A2: a = the carrier of s by Def7;

        s = f by A1, TARSKI:def 1;

        hence thesis by A2, TARSKI:def 1;

      end;

      

       A3: f in {f} by TARSKI:def 1;

      thus {the carrier of f} c= ( Carr {f})

      proof

        let a be object;

        assume a in {the carrier of f};

        then a = the carrier of f by TARSKI:def 1;

        hence thesis by A3, Def7;

      end;

    end;

    theorem :: ORDERS_3:9

    for f,g be 1-sorted holds ( Carr {f, g}) = {the carrier of f, the carrier of g}

    proof

      let f,g be 1-sorted;

      thus ( Carr {f, g}) c= {the carrier of f, the carrier of g}

      proof

        let a be object;

        assume a in ( Carr {f, g});

        then

        consider s be 1-sorted such that

         A1: s in {f, g} and

         A2: a = the carrier of s by Def7;

        per cases by A1, TARSKI:def 2;

          suppose s = f;

          hence thesis by A2, TARSKI:def 2;

        end;

          suppose s = g;

          hence thesis by A2, TARSKI:def 2;

        end;

      end;

      thus {the carrier of f, the carrier of g} c= ( Carr {f, g})

      proof

        let a be object;

        

         A3: f in {f, g} by TARSKI:def 2;

        

         A4: g in {f, g} by TARSKI:def 2;

        assume

         A5: a in {the carrier of f, the carrier of g};

        per cases by A5, TARSKI:def 2;

          suppose a = the carrier of f;

          hence thesis by A3, Def7;

        end;

          suppose a = the carrier of g;

          hence thesis by A4, Def7;

        end;

      end;

    end;

    theorem :: ORDERS_3:10

    

     Th10: ( MonFuncs (A,B)) c= ( Funcs ( Carr P))

    proof

      reconsider CA = the carrier of A, CB = the carrier of B as Element of ( Carr P) by Def7;

      let x be object;

      assume x in ( MonFuncs (A,B));

      then

       A1: ex g be Function of A, B st x = g & g in ( Funcs (the carrier of A,the carrier of B)) & g is monotone by Def6;

      ( Funcs (CA,CB)) c= ( Funcs ( Carr P)) by ENS_1: 2;

      hence thesis by A1;

    end;

    theorem :: ORDERS_3:11

    

     Th11: for A,B be RelStr holds ( MonFuncs (A,B)) c= ( Funcs (the carrier of A,the carrier of B))

    proof

      let A,B be RelStr;

      let a be object;

      assume a in ( MonFuncs (A,B));

      then ex f be Function of A, B st a = f & f in ( Funcs (the carrier of A,the carrier of B)) & f is monotone by Def6;

      hence thesis;

    end;

    registration

      let A,B be non empty Poset;

      cluster ( MonFuncs (A,B)) -> functional;

      coherence

      proof

        reconsider X = ( MonFuncs (A,B)) as Subset of ( Funcs (the carrier of A,the carrier of B)) by Th11;

        X is functional;

        hence thesis;

      end;

    end

    definition

      let P be non empty POSet_set;

      :: ORDERS_3:def8

      func POSCat P -> strict with_triple-like_morphisms Category means the carrier of it = P & (for a,b be Element of P, f be Element of ( Funcs ( Carr P)) st f in ( MonFuncs (a,b)) holds [ [a, b], f] is Morphism of it ) & (for m be Morphism of it holds ex a,b be Element of P, f be Element of ( Funcs ( Carr P)) st m = [ [a, b], f] & f in ( MonFuncs (a,b))) & for m1,m2 be Morphism of it , a1,a2,a3 be Element of P, f1,f2 be Element of ( Funcs ( Carr P)) st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], (f2 * f1)];

      existence

      proof

        deffunc F( Function, Function) = ($1 * $2);

        defpred P[ Element of P, Element of P, set] means $3 in ( MonFuncs ($1,$2));

        

         A1: for a,b,c be Element of P, f,g be Element of ( Funcs ( Carr P)) st P[a, b, f] & P[b, c, g] holds F(g,f) in ( Funcs ( Carr P)) & P[a, c, F(g,f)]

        proof

          let a,b,c be Element of P;

          let f,g be Element of ( Funcs ( Carr P));

          assume f in ( MonFuncs (a,b)) & g in ( MonFuncs (b,c));

          then

           A2: (g * f) in ( MonFuncs (a,c)) by Th6;

          ( MonFuncs (a,c)) c= ( Funcs ( Carr P)) by Th10;

          hence thesis by A2;

        end;

        

         A3: for a be Element of P holds ex f be Element of ( Funcs ( Carr P)) st P[a, a, f] & for b be Element of P, g be Element of ( Funcs ( Carr P)) holds ( P[a, b, g] implies F(g,f) = g) & ( P[b, a, g] implies F(f,g) = g)

        proof

          let a be Element of P;

          set f = ( id the carrier of a);

          ( MonFuncs (a,a)) c= ( Funcs ( Carr P)) & f in ( MonFuncs (a,a)) by Th7, Th10;

          then

          reconsider f as Element of ( Funcs ( Carr P));

          take f;

          now

            let b be Element of P, g be Element of ( Funcs ( Carr P));

            

             A4: g in ( MonFuncs (b,a)) implies (f * g) = g

            proof

              assume g in ( MonFuncs (b,a));

              then ex g9 be Function of b, a st g9 = g & g9 in ( Funcs (the carrier of b,the carrier of a)) & g9 is monotone by Def6;

              then

              reconsider g as Function of the carrier of b, the carrier of a;

              ( rng g) c= the carrier of a;

              hence thesis by RELAT_1: 53;

            end;

            g in ( MonFuncs (a,b)) implies (g * f) = g

            proof

              assume g in ( MonFuncs (a,b));

              then ex g9 be Function of a, b st g9 = g & g9 in ( Funcs (the carrier of a,the carrier of b)) & g9 is monotone by Def6;

              then

              reconsider g as Function of the carrier of a, the carrier of b;

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

              hence thesis by RELAT_1: 51;

            end;

            hence (g in ( MonFuncs (a,b)) implies (g * f) = g) & (g in ( MonFuncs (b,a)) implies (f * g) = g) by A4;

          end;

          hence thesis by Th7;

        end;

        

         A5: for a,b,c,d be Element of P, f,g,h be Element of ( Funcs ( Carr P)) st P[a, b, f] & P[b, c, g] & P[c, d, h] holds F(h,F) = F(F,f) by RELAT_1: 36;

        ex C be with_triple-like_morphisms strict Category st the carrier of C = P & (for a,b be Element of P, f be Element of ( Funcs ( Carr P)) st P[a, b, f] holds [ [a, b], f] is Morphism of C) & (for m be Morphism of C holds ex a,b be Element of P, f be Element of ( Funcs ( Carr P)) st m = [ [a, b], f] & P[a, b, f]) & for m1,m2 be Morphism of C, a1,a2,a3 be Element of P, f1,f2 be Element of ( Funcs ( Carr P)) st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)] from CAT_5:sch 1( A1, A3, A5);

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( Element of ( Funcs ( Carr P)), Element of ( Funcs ( Carr P))) = ($1 * $2);

        defpred P[ Element of P, Element of P, Element of ( Funcs ( Carr P))] means $3 in ( MonFuncs ($1,$2));

         A6:

        now

          let a be Element of P;

          thus ex f be Element of ( Funcs ( Carr P)) st P[a, a, f] & for b be Element of P, g be Element of ( Funcs ( Carr P)) holds ( P[a, b, g] implies F(g,f) = g) & ( P[b, a, g] implies F(f,g) = g)

          proof

            set f = ( id the carrier of a);

            

             A7: f in ( MonFuncs (a,a)) by Th7;

            ( MonFuncs (a,a)) c= ( Funcs ( Carr P)) by Th10;

            then

            reconsider f as Element of ( Funcs ( Carr P)) by A7;

            now

              let b be Element of P, g be Element of ( Funcs ( Carr P));

              

               A8: g in ( MonFuncs (b,a)) implies (f * g) = g

              proof

                assume g in ( MonFuncs (b,a));

                then ex g9 be Function of b, a st g9 = g & g9 in ( Funcs (the carrier of b,the carrier of a)) & g9 is monotone by Def6;

                then

                reconsider g as Function of the carrier of b, the carrier of a;

                ( rng g) c= the carrier of a;

                hence thesis by RELAT_1: 53;

              end;

              g in ( MonFuncs (a,b)) implies (g * f) = g

              proof

                assume g in ( MonFuncs (a,b));

                then ex g9 be Function of a, b st g9 = g & g9 in ( Funcs (the carrier of a,the carrier of b)) & g9 is monotone by Def6;

                then

                reconsider g as Function of the carrier of a, the carrier of b;

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

                hence thesis by RELAT_1: 51;

              end;

              hence (g in ( MonFuncs (a,b)) implies (g * f) = g) & (g in ( MonFuncs (b,a)) implies (f * g) = g) by A8;

            end;

            hence thesis by A7;

          end;

        end;

        thus for C1,C2 be strict with_triple-like_morphisms Category st the carrier of C1 = P & (for a,b be Element of P, f be Element of ( Funcs ( Carr P)) st P[a, b, f] holds [ [a, b], f] is Morphism of C1) & (for m be Morphism of C1 holds ex a,b be Element of P, f be Element of ( Funcs ( Carr P)) st m = [ [a, b], f] & P[a, b, f]) & (for m1,m2 be Morphism of C1, a1,a2,a3 be Element of P, f1,f2 be Element of ( Funcs ( Carr P)) st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)]) & the carrier of C2 = P & (for a,b be Element of P, f be Element of ( Funcs ( Carr P)) st P[a, b, f] holds [ [a, b], f] is Morphism of C2) & (for m be Morphism of C2 holds ex a,b be Element of P, f be Element of ( Funcs ( Carr P)) st m = [ [a, b], f] & P[a, b, f]) & for m1,m2 be Morphism of C2, a1,a2,a3 be Element of P, f1,f2 be Element of ( Funcs ( Carr P)) st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)] holds C1 = C2 from CAT_5:sch 2( A6);

      end;

    end

    begin

    scheme :: ORDERS_3:sch1

    AltCatEx { A() -> non empty set , F( object, object) -> functional set } :

ex C be strict AltCatStr st the carrier of C = A() & for i,j be Element of A() holds (the Arrows of C . (i,j)) = F(i,j) & for i,j,k be Element of A() holds (the Comp of C . (i,j,k)) = ( FuncComp (F(i,j),F(j,k)))

      provided

       A1: for i,j,k be Element of A() holds for f,g be Function st f in F(i,j) & g in F(j,k) holds (g * f) in F(i,k);

      deffunc H( set, set, set) = ( FuncComp (F($1,$2),F($2,$3)));

      consider M be ManySortedSet of [:A(), A():] such that

       A2: for i,j be Element of A() holds (M . (i,j)) = F(i,j) from ALTCAT_1:sch 2;

      consider c be ManySortedSet of [:A(), A(), A():] such that

       A3: for i,j,k be Element of A() holds (c . (i,j,k)) = H(i,j,k) from ALTCAT_1:sch 4;

      c is Function-yielding

      proof

        let i be object;

        assume i in ( dom c);

        then i in [:A(), A(), A():];

        then

        consider x1,x2,x3 be object such that

         A4: x1 in A() & x2 in A() & x3 in A() and

         A5: i = [x1, x2, x3] by MCART_1: 68;

        (c . i) = (c . (x1,x2,x3)) by A5, MULTOP_1:def 1

        .= ( FuncComp (F(x1,x2),F(x2,x3))) by A3, A4;

        hence thesis;

      end;

      then

      reconsider c as ManySortedFunction of [:A(), A(), A():];

      now

        let i be object;

        assume i in [:A(), A(), A():];

        then

        consider x1,x2,x3 be object such that

         A6: x1 in A() and

         A7: x2 in A() and

         A8: x3 in A() and

         A9: i = [x1, x2, x3] by MCART_1: 68;

        (M . (x1,x2)) = F(x1,x2) by A2, A6, A7;

        

        then

         A10: [:F(x2,x3), F(x1,x2):] = [:(M . (x2,x3)), (M . (x1,x2)):] by A2, A7, A8

        .= ( {|M, M|} . (x1,x2,x3)) by A6, A7, A8, ALTCAT_1:def 4

        .= ( {|M, M|} . i) by A9, MULTOP_1:def 1;

        

         A11: ( {|M|} . i) = ( {|M|} . (x1,x2,x3)) by A9, MULTOP_1:def 1

        .= (M . (x1,x3)) by A6, A7, A8, ALTCAT_1:def 3;

         A12:

        now

          assume ( {|M, M|} . i) <> {} ;

          then

          consider j be object such that

           A13: j in [:F(x2,x3), F(x1,x2):] by A10, XBOOLE_0:def 1;

          consider j1,j2 be object such that

           A14: j1 in F(x2,x3) and

           A15: j2 in F(x1,x2) and j = [j1, j2] by A13, ZFMISC_1: 84;

          reconsider j2 as Function by A15;

          reconsider j1 as Function by A14;

          (j1 * j2) in F(x1,x3) by A1, A6, A7, A8, A14, A15;

          hence ( {|M|} . i) <> {} by A2, A6, A8, A11;

        end;

        

         A16: (c . i) = (c . (x1,x2,x3)) by A9, MULTOP_1:def 1

        .= ( FuncComp (F(x1,x2),F(x2,x3))) by A3, A6, A7, A8;

        then

        reconsider ci = (c . i) as Function;

        

         A17: ( dom ci) = [:F(x2,x3), F(x1,x2):] by A16, PARTFUN1:def 2;

        ( rng ( FuncComp (F(x1,x2),F(x2,x3)))) c= F(x1,x3)

        proof

          set F = ( FuncComp (F(x1,x2),F(x2,x3)));

          let i be object;

          assume i in ( rng F);

          then

          consider j be object such that

           A18: j in ( dom F) and

           A19: i = (F . j) by FUNCT_1:def 3;

          consider f,g be Function such that

           A20: j = [g, f] and

           A21: (F . j) = (g * f) by A18, ALTCAT_1:def 9;

          g in F(x2,x3) & f in F(x1,x2) by A18, A20, ZFMISC_1: 87;

          hence thesis by A1, A6, A7, A8, A19, A21;

        end;

        then ( rng ci) c= ( {|M|} . i) by A2, A6, A8, A16, A11;

        hence (c . i) is Function of ( {|M, M|} . i), ( {|M|} . i) by A17, A10, A12, FUNCT_2:def 1, RELSET_1: 4;

      end;

      then

      reconsider c as BinComp of M by PBOOLE:def 15;

      set C = AltCatStr (# A(), M, c #);

      take C;

      thus the carrier of C = A();

      let i,j be Element of A();

      thus (the Arrows of C . (i,j)) = F(i,j) by A2;

      let i,j,k be Element of A();

      thus thesis by A3;

    end;

    scheme :: ORDERS_3:sch2

    AltCatUniq { A() -> non empty set , F( object, object) -> functional set } :

for C1,C2 be strict AltCatStr st (the carrier of C1 = A() & for i,j be Element of A() holds (the Arrows of C1 . (i,j)) = F(i,j) & for i,j,k be Element of A() holds (the Comp of C1 . (i,j,k)) = ( FuncComp (F(i,j),F(j,k)))) & (the carrier of C2 = A() & for i,j be Element of A() holds (the Arrows of C2 . (i,j)) = F(i,j) & for i,j,k be Element of A() holds (the Comp of C2 . (i,j,k)) = ( FuncComp (F(i,j),F(j,k)))) holds C1 = C2;

      let C1,C2 be strict AltCatStr;

      assume that

       A1: the carrier of C1 = A() and

       A2: for i,j be Element of A() holds (the Arrows of C1 . (i,j)) = F(i,j) & for i,j,k be Element of A() holds (the Comp of C1 . (i,j,k)) = ( FuncComp (F(i,j),F(j,k))) and

       A3: the carrier of C2 = A() and

       A4: for i,j be Element of A() holds (the Arrows of C2 . (i,j)) = F(i,j) & for i,j,k be Element of A() holds (the Comp of C2 . (i,j,k)) = ( FuncComp (F(i,j),F(j,k)));

       A5:

      now

        let i,j,k be object;

        assume

         A6: i in A() & j in A() & k in A();

        

        hence (the Comp of C1 . (i,j,k)) = ( FuncComp (F(i,j),F(j,k))) by A2

        .= (the Comp of C2 . (i,j,k)) by A4, A6;

      end;

      now

        let i,j be Element of A();

        

        thus (the Arrows of C1 . (i,j)) = F(i,j) by A2

        .= (the Arrows of C2 . (i,j)) by A4;

      end;

      then the Arrows of C1 = the Arrows of C2 by A1, A3, ALTCAT_1: 7;

      hence thesis by A1, A3, A5, ALTCAT_1: 8;

    end;

    definition

      let P be non empty POSet_set;

      :: ORDERS_3:def9

      func POSAltCat P -> strict AltCatStr means

      : Def9: the carrier of it = P & for i,j be Element of P holds (the Arrows of it . (i,j)) = ( MonFuncs (i,j)) & for i,j,k be Element of P holds (the Comp of it . (i,j,k)) = ( FuncComp (( MonFuncs (i,j)),( MonFuncs (j,k))));

      existence

      proof

        

         A1: for i,j,k be Element of P holds for f,g be Function st f in ( MonFuncs (i,j)) & g in ( MonFuncs (j,k)) holds (g * f) in ( MonFuncs (i,k)) by Th6;

        thus ex C be strict AltCatStr st the carrier of C = P & for i,j be Element of P holds (the Arrows of C . (i,j)) = ( MonFuncs (i,j)) & for i,j,k be Element of P holds (the Comp of C . (i,j,k)) = ( FuncComp (( MonFuncs (i,j)),( MonFuncs (j,k)))) from AltCatEx( A1);

      end;

      uniqueness

      proof

        thus for C1,C2 be strict AltCatStr st (the carrier of C1 = P & for i,j be Element of P holds (the Arrows of C1 . (i,j)) = ( MonFuncs (i,j)) & for i,j,k be Element of P holds (the Comp of C1 . (i,j,k)) = ( FuncComp (( MonFuncs (i,j)),( MonFuncs (j,k))))) & (the carrier of C2 = P & for i,j be Element of P holds (the Arrows of C2 . (i,j)) = ( MonFuncs (i,j)) & for i,j,k be Element of P holds (the Comp of C2 . (i,j,k)) = ( FuncComp (( MonFuncs (i,j)),( MonFuncs (j,k))))) holds C1 = C2 from AltCatUniq;

      end;

    end

    registration

      let P be non empty POSet_set;

      cluster ( POSAltCat P) -> transitive non empty;

      coherence

      proof

        set A = ( POSAltCat P);

        thus A is transitive

        proof

          let o1,o2,o3 be Object of A;

          reconsider o19 = o1, o29 = o2, o39 = o3 as Element of P by Def9;

          assume that

           A1: <^o1, o2^> <> {} and

           A2: <^o2, o3^> <> {} ;

          ( MonFuncs (o19,o29)) <> {} by A1, Def9;

          then

          consider f be object such that

           A3: f in ( MonFuncs (o19,o29)) by XBOOLE_0:def 1;

          ( MonFuncs (o29,o39)) <> {} by A2, Def9;

          then

          consider g be object such that

           A4: g in ( MonFuncs (o29,o39)) by XBOOLE_0:def 1;

          reconsider f, g as Function by A3, A4;

          (g * f) in ( MonFuncs (o19,o39)) by A3, A4, Th6;

          hence thesis by Def9;

        end;

        thus thesis by Def9;

      end;

    end

    registration

      let P be non empty POSet_set;

      cluster ( POSAltCat P) -> associative with_units;

      coherence

      proof

        set A = ( POSAltCat P);

        set G = the Arrows of A, C = the Comp of A;

        thus C is associative

        proof

          let i,j,k,l be Element of A;

          let f,g,h be set;

          reconsider i9 = i, j9 = j, k9 = k, l9 = l as Element of P by Def9;

          assume that

           A1: f in (G . (i,j)) and

           A2: g in (G . (j,k)) and

           A3: h in (G . (k,l));

          

           A4: g in ( MonFuncs (j9,k9)) by A2, Def9;

          

           A5: h in ( MonFuncs (k9,l9)) by A3, Def9;

          

           A6: f in ( MonFuncs (i9,j9)) by A1, Def9;

          then

          reconsider f9 = f, g9 = g, h9 = h as Function by A4, A5;

          

           A7: (C . (i,j,l)) = ( FuncComp (( MonFuncs (i9,j9)),( MonFuncs (j9,l9)))) by Def9;

          (C . (j,k,l)) = ( FuncComp (( MonFuncs (j9,k9)),( MonFuncs (k9,l9)))) by Def9;

          then

           A8: ((C . (j,k,l)) . (h,g)) = (h9 * g9) by A4, A5, ALTCAT_1: 11;

          (C . (i,j,k)) = ( FuncComp (( MonFuncs (i9,j9)),( MonFuncs (j9,k9)))) by Def9;

          then

           A9: ((C . (i,j,k)) . (g,f)) = (g9 * f9) by A6, A4, ALTCAT_1: 11;

          (h9 * g9) in ( MonFuncs (j9,l9)) by A4, A5, Th6;

          then

           A10: ((C . (i,j,l)) . ((h9 * g9),f9)) = ((h9 * g9) * f9) by A6, A7, ALTCAT_1: 11;

          

           A11: (C . (i,k,l)) = ( FuncComp (( MonFuncs (i9,k9)),( MonFuncs (k9,l9)))) by Def9;

          (g9 * f9) in ( MonFuncs (i9,k9)) by A6, A4, Th6;

          then ((C . (i,k,l)) . (h,(g9 * f9))) = (h9 * (g9 * f9)) by A5, A11, ALTCAT_1: 11;

          hence thesis by A9, A8, A10, RELAT_1: 36;

        end;

        thus C is with_left_units

        proof

          let j be Element of A;

          reconsider j9 = j as Element of P by Def9;

          take e = ( id the carrier of j9);

          (G . (j,j)) = ( MonFuncs (j9,j9)) by Def9;

          hence e in (G . (j,j)) by Th7;

          let i be Element of A, f be set;

          reconsider i9 = i as Element of P by Def9;

          

           A12: (C . (i,j,j)) = ( FuncComp (( MonFuncs (i9,j9)),( MonFuncs (j9,j9)))) by Def9;

          assume f in (G . (i,j));

          then

           A13: f in ( MonFuncs (i9,j9)) by Def9;

          then

          consider f9 be Function of i9, j9 such that

           A14: f = f9 and f9 in ( Funcs (the carrier of i9,the carrier of j9)) and f9 is monotone by Def6;

          

           A15: e in ( MonFuncs (j9,j9)) by Th7;

          then

          consider e9 be Function of j9, j9 such that

           A16: e = e9 and e9 in ( Funcs (the carrier of j9,the carrier of j9)) and e9 is monotone by Def6;

          ( rng f9) c= the carrier of j9;

          then (e9 * f9) = f by A16, A14, RELAT_1: 53;

          hence thesis by A15, A16, A13, A14, A12, ALTCAT_1: 11;

        end;

        thus C is with_right_units

        proof

          let i be Element of A;

          reconsider i9 = i as Element of P by Def9;

          take e = ( id the carrier of i9);

          (G . (i,i)) = ( MonFuncs (i9,i9)) by Def9;

          hence e in (G . (i,i)) by Th7;

          let j be Element of A, f be set;

          reconsider j9 = j as Element of P by Def9;

          

           A17: (C . (i,i,j)) = ( FuncComp (( MonFuncs (i9,i9)),( MonFuncs (i9,j9)))) by Def9;

          assume f in (G . (i,j));

          then

           A18: f in ( MonFuncs (i9,j9)) by Def9;

          then

          consider f9 be Function of i9, j9 such that

           A19: f = f9 and f9 in ( Funcs (the carrier of i9,the carrier of j9)) and f9 is monotone by Def6;

          

           A20: e in ( MonFuncs (i9,i9)) by Th7;

          then

          consider e9 be Function of i9, i9 such that

           A21: e = e9 and e9 in ( Funcs (the carrier of i9,the carrier of i9)) and e9 is monotone by Def6;

          ( dom f9) = the carrier of i9 by FUNCT_2:def 1;

          then (f9 * e9) = f by A21, A19, RELAT_1: 52;

          hence thesis by A20, A21, A18, A19, A17, ALTCAT_1: 11;

        end;

      end;

    end

    theorem :: ORDERS_3:12

    for o1,o2 be Object of ( POSAltCat P), A,B be Element of P st o1 = A & o2 = B holds <^o1, o2^> c= ( Funcs (the carrier of A,the carrier of B))

    proof

      let o1,o2 be Object of ( POSAltCat P), A,B be Element of P;

      assume

       A1: o1 = A & o2 = B;

      let x be object;

      assume x in <^o1, o2^>;

      then x in ( MonFuncs (A,B)) by A1, Def9;

      then ex f be Function of A, B st f = x & f in ( Funcs (the carrier of A,the carrier of B)) & f is monotone by Def6;

      hence thesis;

    end;