cat_2.miz



    begin

    ::$Canceled

    reserve B,C,D,C9,D9 for Category;

    definition

      let B, C;

      let c be Object of C;

      :: CAT_2:def1

      func B --> c -> Functor of B, C equals (the carrier' of B --> ( id c));

      coherence

      proof

        reconsider T = (the carrier' of B --> ( id c)) as Function of the carrier' of B, the carrier' of C;

        now

          thus for b be Object of B holds ex d be Object of C st (T . ( id b)) = ( id d) by FUNCOP_1: 7;

          thus for f be Morphism of B holds (T . ( id ( dom f))) = ( id ( dom (T . f))) & (T . ( id ( cod f))) = ( id ( cod (T . f)))

          proof

            let f be Morphism of B;

            (T . ( id ( cod f))) = ( id c) by FUNCOP_1: 7;

            then

             A1: (T . ( id ( cod f))) = ( id ( cod ( id c)));

            (T . ( id ( dom f))) = ( id c) by FUNCOP_1: 7;

            then (T . ( id ( dom f))) = ( id ( dom ( id c)));

            hence thesis by A1, FUNCOP_1: 7;

          end;

          let f,g be Morphism of B such that ( dom g) = ( cod f);

          ( Hom (c,c)) <> {} ;

          then

           A2: (T . f) = ( id c) & (( id c) * ( id c)) = (( id c) (*) ( id c)) by CAT_1:def 13, FUNCOP_1: 7;

          (T . (g (*) f)) = ( id c) & (T . g) = ( id c) by FUNCOP_1: 7;

          hence (T . (g (*) f)) = ((T . g) (*) (T . f)) by A2;

        end;

        hence thesis by CAT_1: 61;

      end;

    end

    theorem :: CAT_2:5

    for c be Object of C, b be Object of B holds (( Obj (B --> c)) . b) = c

    proof

      let c be Object of C, b be Object of B;

      ((B --> c) . ( id b)) = ( id c) by FUNCOP_1: 7;

      hence thesis by CAT_1: 67;

    end;

    definition

      let C, D;

      :: CAT_2:def2

      func Funct (C,D) -> set means

      : Def2: for x be set holds x in it iff x is Functor of C, D;

      existence

      proof

        defpred P[ object] means $1 is Functor of C, D;

        consider F be set such that

         A1: for x be object holds x in F iff x in ( Funcs (the carrier' of C,the carrier' of D)) & P[x] from XBOOLE_0:sch 1;

        take F;

        let x be set;

        thus x in F implies x is Functor of C, D by A1;

        assume

         A2: x is Functor of C, D;

        then x in ( Funcs (the carrier' of C,the carrier' of D)) by FUNCT_2: 8;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let F1,F2 be set such that

         A3: for x be set holds x in F1 iff x is Functor of C, D and

         A4: for x be set holds x in F2 iff x is Functor of C, D;

        now

          let x be object;

          x in F1 iff x is Functor of C, D by A3;

          hence x in F1 iff x in F2 by A4;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    registration

      let C, D;

      cluster ( Funct (C,D)) -> non empty;

      coherence

      proof

        set x = the Functor of C, D;

        x in ( Funct (C,D)) by Def2;

        hence thesis;

      end;

    end

    definition

      let C, D;

      :: CAT_2:def3

      mode FUNCTOR-DOMAIN of C,D -> non empty set means

      : Def3: for x be Element of it holds x is Functor of C, D;

      existence

      proof

        take ( Funct (C,D));

        thus thesis by Def2;

      end;

    end

    definition

      let C, D;

      let F be FUNCTOR-DOMAIN of C, D;

      :: original: Element

      redefine

      mode Element of F -> Functor of C, D ;

      coherence by Def3;

    end

    definition

      let A be non empty set;

      let C, D;

      let F be FUNCTOR-DOMAIN of C, D, T be Function of A, F, x be Element of A;

      :: original: .

      redefine

      func T . x -> Element of F ;

      coherence

      proof

        thus (T . x) is Element of F;

      end;

    end

    definition

      let C, D;

      :: original: Funct

      redefine

      func Funct (C,D) -> FUNCTOR-DOMAIN of C, D ;

      coherence

      proof

        let x be Element of ( Funct (C,D));

        thus thesis by Def2;

      end;

    end

    definition

      let C;

      :: CAT_2:def4

      mode Subcategory of C -> Category means

      : Def4: the carrier of it c= the carrier of C & (for a,b be Object of it , a9,b9 be Object of C st a = a9 & b = b9 holds ( Hom (a,b)) c= ( Hom (a9,b9))) & the Comp of it c= the Comp of C & for a be Object of it , a9 be Object of C st a = a9 holds ( id a) = ( id a9);

      existence

      proof

        take C;

        thus thesis;

      end;

    end

    registration

      let C;

      cluster strict for Subcategory of C;

      existence

      proof

        set c = the Object of C;

        set E = ( 1Cat (c,( id c)));

        now

          thus the carrier of E c= the carrier of C

          proof

            let a be object;

            assume a in the carrier of E;

            then a = c by TARSKI:def 1;

            hence thesis;

          end;

          thus for a,b be Object of E, a9,b9 be Object of C st a = a9 & b = b9 holds ( Hom (a,b)) c= ( Hom (a9,b9))

          proof

            let a,b be Object of E, a9,b9 be Object of C;

            assume a = a9 & b = b9;

            then

             A1: a9 = c & b9 = c by TARSKI:def 1;

            let x be object;

            assume x in ( Hom (a,b));

            then x = ( id c) by TARSKI:def 1;

            hence thesis by A1, CAT_1: 27;

          end;

          thus the Comp of E c= the Comp of C

          proof

            reconsider i = ( id c) as Morphism of C;

            

             A2: ( Hom (c,c)) <> {} ;

            

             A3: ( dom ( id c)) = c & ( cod ( id c)) = c;

            then

             A4: [( id c), ( id c)] in ( dom the Comp of C) by CAT_1: 15;

            the Comp of E = ((( id c),( id c)) .--> (( id c) * ( id c)))

            .= ((( id c),( id c)) .--> (( id c) (*) i)) by A2, CAT_1:def 13

            .= ( [( id c), ( id c)] .--> (the Comp of C . (( id c),( id c)))) by A3, CAT_1: 16;

            hence thesis by A4, FUNCT_4: 7;

          end;

          let a be Object of E, a9 be Object of C;

          assume a = a9;

          then a9 = c by TARSKI:def 1;

          hence ( id a) = ( id a9) by TARSKI:def 1;

        end;

        then E is Subcategory of C by Def4;

        hence thesis;

      end;

    end

    reserve E for Subcategory of C;

    theorem :: CAT_2:6

    

     Th2: for e be Object of E holds e is Object of C

    proof

      let e be Object of E;

      e in the carrier of E & the carrier of E c= the carrier of C by Def4;

      hence thesis;

    end;

    theorem :: CAT_2:7

    

     Th3: the carrier' of E c= the carrier' of C

    proof

      let x be object;

      assume x in the carrier' of E;

      then

      reconsider f = x as Morphism of E;

      set a = ( dom f), b = ( cod f);

      reconsider a9 = a, b9 = b as Object of C by Th2;

      f in ( Hom (a,b)) & ( Hom (a,b)) c= ( Hom (a9,b9)) by Def4;

      then f in ( Hom (a9,b9)) & ( Hom (a9,b9)) <> {} ;

      hence thesis;

    end;

    theorem :: CAT_2:8

    

     Th4: for f be Morphism of E holds f is Morphism of C

    proof

      let f be Morphism of E;

      f in the carrier' of E & the carrier' of E c= the carrier' of C by Th3;

      hence thesis;

    end;

    theorem :: CAT_2:9

    

     Th5: for f be Morphism of E, f9 be Morphism of C st f = f9 holds ( dom f) = ( dom f9) & ( cod f) = ( cod f9)

    proof

      let f be Morphism of E, f9 be Morphism of C such that

       A1: f = f9;

      set a = ( dom f), b = ( cod f);

      reconsider a9 = a, b9 = b as Object of C by Th2;

      f in ( Hom (a,b)) & ( Hom (a,b)) c= ( Hom (a9,b9)) by Def4;

      hence thesis by A1, CAT_1: 1;

    end;

    theorem :: CAT_2:10

    for a,b be Object of E, a9,b9 be Object of C, f be Morphism of a, b st a = a9 & b = b9 & ( Hom (a,b)) <> {} holds f is Morphism of a9, b9

    proof

      let a,b be Object of E, a9,b9 be Object of C, f be Morphism of a, b;

      assume a = a9 & b = b9 & ( Hom (a,b)) <> {} ;

      then f in ( Hom (a,b)) & ( Hom (a,b)) c= ( Hom (a9,b9)) by Def4, CAT_1:def 5;

      then f in ( Hom (a9,b9)) & ( Hom (a9,b9)) <> {} ;

      hence thesis by CAT_1:def 5;

    end;

    theorem :: CAT_2:11

    

     Th7: for f,g be Morphism of E, f9,g9 be Morphism of C st f = f9 & g = g9 & ( dom g) = ( cod f) holds (g (*) f) = (g9 (*) f9)

    proof

      let f,g be Morphism of E, f9,g9 be Morphism of C such that

       A1: f = f9 & g = g9 and

       A2: ( dom g) = ( cod f);

      ( dom g) = ( dom g9) & ( cod f) = ( cod f9) by A1, Th5;

      then

       A3: (g9 (*) f9) = (the Comp of C . (g9,f9)) by A2, CAT_1: 16;

      

       A4: the Comp of E c= the Comp of C by Def4;

      (g (*) f) = (the Comp of E . (g,f)) & [g, f] in ( dom the Comp of E) by A2, CAT_1: 15, CAT_1: 16;

      hence thesis by A1, A3, A4, GRFUNC_1: 2;

    end;

    theorem :: CAT_2:12

    

     Th8: C is Subcategory of C

    proof

      thus the carrier of C c= the carrier of C;

      thus thesis;

    end;

    theorem :: CAT_2:13

    

     Th9: ( id E) is Functor of E, C

    proof

      ( rng ( id E)) c= the carrier' of C by Th3;

      then

      reconsider T = ( id E) as Function of the carrier' of E, the carrier' of C by FUNCT_2: 6;

      now

        thus for e be Object of E holds ex c be Object of C st (T . ( id e)) = ( id c)

        proof

          let e be Object of E;

          reconsider c = e as Object of C by Th2;

          (T . ( id e)) = ( id e) by FUNCT_1: 18

          .= ( id c) by Def4;

          hence thesis;

        end;

        thus for f be Morphism of E holds (T . ( id ( dom f))) = ( id ( dom (T . f))) & (T . ( id ( cod f))) = ( id ( cod (T . f)))

        proof

          let f be Morphism of E;

          

           A1: (T . ( id ( dom f))) = ( id ( dom f)) by FUNCT_1: 18

          .= ( id ( dom (( id E) . f))) by FUNCT_1: 18;

          

           A2: (T . ( id ( cod f))) = ( id ( cod f)) by FUNCT_1: 18

          .= ( id ( cod (( id E) . f))) by FUNCT_1: 18;

          ( dom (T . f)) = ( dom (( id E) . f)) & ( cod (T . f)) = ( cod (( id E) . f)) by Th5;

          hence thesis by A1, A2, Def4;

        end;

        let f,g be Morphism of E;

        

         A3: (T . f) = f & (T . g) = g by FUNCT_1: 18;

        assume

         A4: ( dom g) = ( cod f);

        then (T . (g (*) f)) = ((( id E) . g) (*) (( id E) . f)) by CAT_1: 64;

        hence (T . (g (*) f)) = ((T . g) (*) (T . f)) by A4, A3, Th7;

      end;

      hence thesis by CAT_1: 61;

    end;

    definition

      let C, E;

      :: CAT_2:def5

      func incl (E) -> Functor of E, C equals ( id E);

      coherence by Th9;

    end

    theorem :: CAT_2:14

    

     Th10: for a be Object of E holds (( Obj ( incl E)) . a) = a

    proof

      let a be Object of E;

      reconsider a9 = a as Object of C by Th2;

      ( id a9) = ( id a) by Def4

      .= (( incl E) . ( id a)) by FUNCT_1: 18

      .= ( id (( Obj ( incl E)) . a)) by CAT_1: 68;

      hence thesis by CAT_1: 59;

    end;

    theorem :: CAT_2:15

    for a be Object of E holds (( incl E) . a) = a by Th10;

    theorem :: CAT_2:16

    ( incl E) is faithful

    proof

      let a,b be Object of E such that ( Hom (a,b)) <> {} ;

      let f1,f2 be Morphism of a, b;

      (( incl E) . f1) = f1 by FUNCT_1: 18;

      hence thesis by FUNCT_1: 18;

    end;

    theorem :: CAT_2:17

    

     Th13: ( incl E) is full iff for a,b be Object of E, a9,b9 be Object of C st a = a9 & b = b9 holds ( Hom (a,b)) = ( Hom (a9,b9))

    proof

      set T = ( incl E);

      thus T is full implies for a,b be Object of E, a9,b9 be Object of C st a = a9 & b = b9 holds ( Hom (a,b)) = ( Hom (a9,b9))

      proof

        assume

         A1: for a,b be Object of E st ( Hom ((T . a),(T . b))) <> {} holds for g be Morphism of (T . a), (T . b) holds ( Hom (a,b)) <> {} & ex f be Morphism of a, b st g = (T . f);

        let a,b be Object of E, a9,b9 be Object of C such that

         A2: a = a9 & b = b9;

        now

          let x be object;

          ( Hom (a,b)) c= ( Hom (a9,b9)) by A2, Def4;

          hence x in ( Hom (a,b)) implies x in ( Hom (a9,b9));

          assume

           A3: x in ( Hom (a9,b9));

          

           A4: (T . a) = a9 & (T . b) = b9 by A2, Th10;

          then

          reconsider g = x as Morphism of (T . a), (T . b) by A3, CAT_1:def 5;

          consider f be Morphism of a, b such that

           A5: g = (T . f) by A1, A4, A3;

          

           A6: g = f by A5, FUNCT_1: 18;

          ( Hom (a,b)) <> {} by A1, A4, A3;

          hence x in ( Hom (a,b)) by A6, CAT_1:def 5;

        end;

        hence thesis by TARSKI: 2;

      end;

      assume

       A7: for a,b be Object of E, a9,b9 be Object of C st a = a9 & b = b9 holds ( Hom (a,b)) = ( Hom (a9,b9));

      let a,b be Object of E such that

       A8: ( Hom ((T . a),(T . b))) <> {} ;

      let g be Morphism of (T . a), (T . b);

      

       A9: g in ( Hom ((T . a),(T . b))) by A8, CAT_1:def 5;

      

       A10: a = (T . a) & b = (T . b) by Th10;

      hence ( Hom (a,b)) <> {} by A7, A8;

      ( Hom (a,b)) = ( Hom ((T . a),(T . b))) by A7, A10;

      then

      reconsider f = g as Morphism of a, b by A9, CAT_1:def 5;

      take f;

      thus thesis by FUNCT_1: 18;

    end;

    definition

      let D;

      let C be Subcategory of D;

      :: CAT_2:def6

      attr C is full means

      : Def6: for c1,c2 be Object of C, d1,d2 be Object of D st c1 = d1 & c2 = d2 holds ( Hom (c1,c2)) = ( Hom (d1,d2));

    end

    registration

      let D;

      cluster full for Subcategory of D;

      existence

      proof

        reconsider C = D as Subcategory of D by Th8;

        take C;

        let c1,c2 be Object of C, d1,d2 be Object of D;

        assume c1 = d1 & c2 = d2;

        hence ( Hom (c1,c2)) = ( Hom (d1,d2));

      end;

    end

    theorem :: CAT_2:18

    E is full iff ( incl E) is full by Th13;

    theorem :: CAT_2:19

    

     Th15: for O be non empty Subset of the carrier of C holds ( union { ( Hom (a,b)) where a be Object of C, b be Object of C : a in O & b in O }) is non empty Subset of the carrier' of C

    proof

      let O be non empty Subset of the carrier of C;

      set H = { ( Hom (a,b)) where a be Object of C, b be Object of C : a in O & b in O };

      set M = ( union H);

      

       A1: M c= the carrier' of C

      proof

        let x be object;

        assume x in M;

        then

        consider X be set such that

         A2: x in X and

         A3: X in H by TARSKI:def 4;

        ex a,b be Object of C st X = ( Hom (a,b)) & a in O & b in O by A3;

        hence thesis by A2;

      end;

      now

        set a = the Element of O;

        reconsider a as Object of C;

        ( id a) in ( Hom (a,a)) & ( Hom (a,a)) in H by CAT_1: 27;

        then ( id a) in M by TARSKI:def 4;

        hence ex f be set st f in M;

      end;

      hence thesis by A1;

    end;

    theorem :: CAT_2:20

    

     Th16: for O be non empty Subset of the carrier of C, M be non empty set st M = ( union { ( Hom (a,b)) where a be Object of C, b be Object of C : a in O & b in O }) holds (the Source of C | M) is Function of M, O & (the Target of C | M) is Function of M, O & (the Comp of C || M) is PartFunc of [:M, M:], M

    proof

      let O be non empty Subset of the carrier of C;

      set H = { ( Hom (a,b)) where a be Object of C, b be Object of C : a in O & b in O };

      

       A1: ( dom the Source of C) = the carrier' of C by FUNCT_2:def 1;

      let M be non empty set such that

       A2: M = ( union H);

       A3:

      now

        let f be Morphism of C;

        assume f in M;

        then

        consider X be set such that

         A4: f in X and

         A5: X in H by A2, TARSKI:def 4;

        ex a,b be Object of C st X = ( Hom (a,b)) & a in O & b in O by A5;

        hence ( dom f) in O & ( cod f) in O by A4, CAT_1: 1;

      end;

      set d = (the Source of C | M), c = (the Target of C | M), p = (the Comp of C || M);

      

       A6: ( dom the Target of C) = the carrier' of C by FUNCT_2:def 1;

      

       A7: ( dom d) = (( dom the Source of C) /\ M) by RELAT_1: 61;

      

       A8: ( rng d) c= O

      proof

        let y be object;

        assume y in ( rng d);

        then

        consider x be object such that

         A9: x in ( dom d) and

         A10: y = (d . x) by FUNCT_1:def 3;

        reconsider f = x as Morphism of C by A1, A7, A9, XBOOLE_0:def 4;

        (d . f) = ( dom f) & f in M by A7, A9, FUNCT_1: 47, XBOOLE_0:def 4;

        hence thesis by A3, A10;

      end;

      

       A11: M is non empty Subset of the carrier' of C by A2, Th15;

      then

       A12: ( dom c) = M by A6, RELAT_1: 62;

      

       A13: ( dom c) = (( dom the Target of C) /\ M) by RELAT_1: 61;

      

       A14: ( rng c) c= O

      proof

        let y be object;

        assume y in ( rng c);

        then

        consider x be object such that

         A15: x in ( dom c) and

         A16: y = (c . x) by FUNCT_1:def 3;

        reconsider f = x as Morphism of C by A6, A13, A15, XBOOLE_0:def 4;

        (c . f) = ( cod f) & f in M by A13, A15, FUNCT_1: 47, XBOOLE_0:def 4;

        hence thesis by A3, A16;

      end;

      ( dom d) = M by A1, A11, RELAT_1: 62;

      hence d is Function of M, O & c is Function of M, O by A8, A14, A12, FUNCT_2:def 1, RELSET_1: 4;

      

       A17: ( dom p) = (( dom the Comp of C) /\ [:M, M:]) by RELAT_1: 61;

      

       A18: ( dom the Comp of C) c= [:the carrier' of C, the carrier' of C:] by RELAT_1:def 18;

      ( rng p) c= M

      proof

        let y be object;

        assume y in ( rng p);

        then

        consider x be object such that

         A19: x in ( dom p) and

         A20: y = (p . x) by FUNCT_1:def 3;

        

         A21: x in ( dom the Comp of C) by A17, A19, XBOOLE_0:def 4;

        then

        consider g,f be Morphism of C such that

         A22: x = [g, f] by A18, DOMAIN_1: 1;

        

         A23: [g, f] in [:M, M:] by A17, A19, A22, XBOOLE_0:def 4;

        then g in M by ZFMISC_1: 87;

        then

         A24: ( cod g) in O by A3;

        ( dom g) = ( cod f) by A21, A22, CAT_1: 15;

        then

         A25: ( dom (g (*) f)) = ( dom f) & ( cod (g (*) f)) = ( cod g) by CAT_1: 17;

        f in M by A23, ZFMISC_1: 87;

        then ( dom f) in O by A3;

        then

         A26: ( Hom (( dom (g (*) f)),( cod (g (*) f)))) in H by A24, A25;

        

         A27: (g (*) f) in ( Hom (( dom (g (*) f)),( cod (g (*) f))));

        (p . x) = (the Comp of C . (g,f)) by A19, A22, FUNCT_1: 47

        .= (g (*) f) by A21, A22, CAT_1:def 1;

        hence thesis by A2, A20, A26, A27, TARSKI:def 4;

      end;

      hence p is PartFunc of [:M, M:], M by A17, RELSET_1: 4, XBOOLE_1: 17;

      thus thesis;

    end;

    registration

      let O,M be non empty set, d,c be Function of M, O, p be PartFunc of [:M, M:], M;

      cluster CatStr (# O, M, d, c, p #) -> non void non empty;

      coherence ;

    end

    

     Lm1: for O be non empty Subset of the carrier of C, M be non empty set, d,c be Function of M, O, p be PartFunc of [:M, M:], M, i be Function of O, M st M = ( union { ( Hom (a,b)) where a be Object of C, b be Object of C : a in O & b in O }) & d = (the Source of C | M) & c = (the Target of C | M) & p = (the Comp of C || M) holds CatStr (# O, M, d, c, p #) is Category

    proof

      let O be non empty Subset of the carrier of C, M be non empty set, d,c be Function of M, O, p be PartFunc of [:M, M:], M, i be Function of O, M;

      set H = { ( Hom (a,b)) where a be Object of C, b be Object of C : a in O & b in O };

      assume that

       A1: M = ( union H) and

       A2: d = (the Source of C | M) and

       A3: c = (the Target of C | M) and

       A4: p = (the Comp of C || M);

      set B = CatStr (# O, M, d, c, p #);

       A5:

      now

        let f be Morphism of B;

        consider X be set such that

         A6: f in X and

         A7: X in H by A1, TARSKI:def 4;

        ex a,b be Object of C st X = ( Hom (a,b)) & a in O & b in O by A7;

        hence f is Morphism of C by A6;

      end;

      

       A8: for f,g be Morphism of B holds [g, f] in ( dom p) iff (d . g) = (c . f)

      proof

        let f,g be Morphism of B;

        reconsider gg = g, ff = f as Morphism of C by A5;

        

         A9: (d . g) = ( dom gg) & (c . f) = ( cod ff) by A2, A3, FUNCT_1: 49;

        thus [g, f] in ( dom p) implies (d . g) = (c . f)

        proof

          assume [g, f] in ( dom p);

          then [g, f] in (( dom the Comp of C) /\ [:M, M:]) by A4, RELAT_1: 61;

          then [gg, ff] in ( dom the Comp of C) by XBOOLE_0:def 4;

          hence thesis by A9, CAT_1:def 6;

        end;

        assume (d . g) = (c . f);

        then [g, f] in ( dom the Comp of C) by A9, CAT_1:def 6;

        then [g, f] in (( dom the Comp of C) /\ [:M, M:]) by XBOOLE_0:def 4;

        hence thesis by A4, RELAT_1: 61;

      end;

      

       A10: B is Category-like by A8;

      

       A11: B is transitive

      proof

        thus for f,g be Morphism of B st ( dom g) = ( cod f) holds ( dom (g (*) f)) = ( dom f) & ( cod (g (*) f)) = ( cod g)

        proof

          let f,g be Morphism of B;

          reconsider ff = f, gg = g as Morphism of C by A5;

          

           A12: (d . g) = ( dom gg) & (c . f) = ( cod ff) by A2, A3, FUNCT_1: 49;

          assume

           A13: ( dom g) = ( cod f);

          

           A14: [g, f] in ( dom the Comp of B) by A13, A8;

          

           A15: (p . (g,f)) = (g (*) f) by A13, A8, CAT_1:def 1;

          

           A16: ( dom p) c= ( dom the Comp of C) by A4, RELAT_1: 60;

          

           A17: (p . [g, f]) = (the Comp of C . (g,f)) by A4, A8, A13, FUNCT_1: 47

          .= (gg (*) ff) by A16, A14, CAT_1:def 1;

          

          thus ( dom (g (*) f)) = ( dom (gg (*) ff)) by A17, A2, A15, FUNCT_1: 49

          .= ( dom ff) by A13, A12, CAT_1:def 7

          .= ( dom f) by A2, FUNCT_1: 49;

          

          thus ( cod (g (*) f)) = ( cod (gg (*) ff)) by A17, A3, A15, FUNCT_1: 49

          .= ( cod gg) by A13, A12, CAT_1:def 7

          .= ( cod g) by A3, FUNCT_1: 49;

        end;

      end;

      

       A18: B is associative

      proof

        thus for f,g,h be Morphism of B st ( dom h) = ( cod g) & ( dom g) = ( cod f) holds (h (*) (g (*) f)) = ((h (*) g) (*) f)

        proof

          let f,g,h be Morphism of B;

          reconsider ff = f, gg = g, hh = h as Morphism of C by A5;

          assume that

           A19: ( dom h) = ( cod g) and

           A20: ( dom g) = ( cod f);

          

           A21: (h (*) g) = (the Comp of B . (h,g)) by A19, A8, CAT_1:def 1;

          

           A22: (g (*) f) = (the Comp of B . (g,f)) by A20, A8, CAT_1:def 1;

          

           A23: ( dom (h (*) g)) = ( dom g) by A11, A19;

          

           A24: (c . g) = ( cod gg) & (d . g) = ( dom gg) by A2, A3, FUNCT_1: 49;

          

           A25: (c . f) = ( cod ff) by A3, FUNCT_1: 49;

          

           A26: f is Morphism of C & (d . h) = ( dom hh) by A2, A5, FUNCT_1: 49;

          

           A27: ( dom gg) = (d . g) by A2, FUNCT_1: 49

          .= ( cod ff) by A3, A20, FUNCT_1: 49;

          then

           A28: (gg (*) ff) = (the Comp of C . (gg,ff)) by CAT_1: 16;

          

           A29: ( dom hh) = (d . h) by A2, FUNCT_1: 49

          .= ( cod gg) by A3, A19, FUNCT_1: 49;

          then

           A30: ( cod (gg (*) ff)) = ( dom hh) by A27, CAT_1:def 7;

          

           A31: (hh (*) gg) = (the Comp of C . (hh,gg)) by A29, CAT_1: 16;

          

           A32: ( cod ff) = ( dom (hh (*) gg)) by A27, A29, CAT_1:def 7;

          

           A33: ( cod (g (*) f)) = ( cod g) by A11, A20;

          

          hence (h (*) (g (*) f)) = (the Comp of B . (h,(the Comp of B . (g,f)))) by A22, A19, A8, CAT_1:def 1

          .= (the Comp of C . [h, (p . [g, f])]) by A4, A8, A19, A33, A22, FUNCT_1: 47

          .= (the Comp of C . (hh,(gg (*) ff))) by A4, A8, A20, A28, FUNCT_1: 47

          .= (hh (*) (gg (*) ff)) by A30, CAT_1: 16

          .= ((hh (*) gg) (*) ff) by A19, A20, A26, A24, A25, CAT_1:def 8

          .= (the Comp of C . ((the Comp of C . (hh,gg)),ff)) by A31, A32, CAT_1: 16

          .= (the Comp of C . [(p . [h, g]), f]) by A4, A8, A19, FUNCT_1: 47

          .= (the Comp of B . ((the Comp of B . (h,g)),f)) by A4, A8, A20, A23, A21, FUNCT_1: 47

          .= ((h (*) g) (*) f) by A21, A20, A8, A23, CAT_1:def 1;

        end;

      end;

      

       A34: B is reflexive

      proof

        let b be Object of B;

        b in O;

        then

        reconsider bb = b as Object of C;

        

         A35: ( Hom (bb,bb)) in H;

        ( id bb) in ( Hom (bb,bb)) by CAT_1: 27;

        then

        reconsider ii = ( id bb) as Morphism of B by A35, A1, TARSKI:def 4;

        

         A36: ( dom ii) = ( dom ( id bb)) by A2, FUNCT_1: 49

        .= bb;

        ( cod ii) = ( cod ( id bb)) by A3, FUNCT_1: 49

        .= bb;

        then ii in ( Hom (b,b)) by A36;

        hence ( Hom (b,b)) <> {} ;

      end;

      B is with_identities

      proof

        let a be Element of B;

        a in O;

        then

        reconsider aa = a as Object of C;

        

         A37: ( Hom (aa,aa)) in H;

        ( id aa) in ( Hom (aa,aa)) by CAT_1: 27;

        then

        reconsider ii = ( id aa) as Morphism of B by A37, A1, TARSKI:def 4;

        

         A38: ( dom ii) = ( dom ( id aa)) by A2, FUNCT_1: 49

        .= aa;

        

         A39: ( cod ii) = ( cod ( id aa)) by A3, FUNCT_1: 49

        .= aa;

        then

        reconsider ii as Morphism of a, a by A38, CAT_1: 4;

        take ii;

        let b be Element of B;

        b in O;

        then

        reconsider bb = b as Object of C;

        thus ( Hom (a,b)) <> {} implies for g be Morphism of a, b holds (g (*) ii) = g

        proof

          assume

           A40: ( Hom (a,b)) <> {} ;

          let g be Morphism of a, b;

          reconsider gg = g as Morphism of C by A5;

          

           A41: ( dom gg) = ( dom g) by A2, FUNCT_1: 49

          .= aa by A40, CAT_1: 5;

          

           A42: ( cod ( id aa)) = aa;

          ( cod gg) = ( cod g) by A3, FUNCT_1: 49

          .= bb by A40, CAT_1: 5;

          then

          reconsider gg as Morphism of aa, bb by A41, CAT_1: 4;

          

           A43: ( dom g) = a by A40, CAT_1: 5;

          

          hence (g (*) ii) = (p . (g,ii)) by A39, A8, CAT_1:def 1

          .= (the Comp of C . (gg,( id aa))) by A43, A4, A39, A8, FUNCT_1: 47

          .= (gg (*) ( id aa)) by A41, A42, CAT_1: 16

          .= g by A41, CAT_1: 22;

        end;

        thus ( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (ii (*) f) = f

        proof

          assume

           A44: ( Hom (b,a)) <> {} ;

          let g be Morphism of b, a;

          reconsider gg = g as Morphism of C by A5;

          

           A45: ( cod gg) = ( cod g) by A3, FUNCT_1: 49

          .= aa by A44, CAT_1: 5;

          

           A46: ( dom ( id aa)) = aa;

          ( dom gg) = ( dom g) by A2, FUNCT_1: 49

          .= bb by A44, CAT_1: 5;

          then

          reconsider gg as Morphism of bb, aa by A45, CAT_1: 4;

          

           A47: ( cod g) = a by A44, CAT_1: 5;

          

          hence (ii (*) g) = (p . (ii,g)) by A38, A8, CAT_1:def 1

          .= (the Comp of C . (( id aa),gg)) by A4, A47, A38, A8, FUNCT_1: 47

          .= (( id aa) (*) gg) by A45, A46, CAT_1: 16

          .= g by A45, CAT_1: 21;

        end;

      end;

      hence B is Category by A10, A11, A18, A34;

    end;

    

     Lm2: for O be non empty Subset of the carrier of C, M be non empty set, d,c be Function of M, O, p be PartFunc of [:M, M:], M, i be Function of O, M st M = ( union { ( Hom (a,b)) where a be Object of C, b be Object of C : a in O & b in O }) & d = (the Source of C | M) & c = (the Target of C | M) & p = (the Comp of C || M) holds CatStr (# O, M, d, c, p #) is Subcategory of C

    proof

      let O be non empty Subset of the carrier of C, M be non empty set, d,c be Function of M, O, p be PartFunc of [:M, M:], M, i be Function of O, M;

      set H = { ( Hom (a,b)) where a be Object of C, b be Object of C : a in O & b in O };

      assume that

       A1: M = ( union H) and

       A2: d = (the Source of C | M) and

       A3: c = (the Target of C | M) and

       A4: p = (the Comp of C || M);

      set B = CatStr (# O, M, d, c, p #);

       A5:

      now

        let f be Morphism of B;

        consider X be set such that

         A6: f in X and

         A7: X in H by A1, TARSKI:def 4;

        ex a,b be Object of C st X = ( Hom (a,b)) & a in O & b in O by A7;

        hence f is Morphism of C by A6;

      end;

      

       A8: for a,b be Object of B, a9,b9 be Object of C st a = a9 & b = b9 holds ( Hom (a,b)) = ( Hom (a9,b9))

      proof

        let a,b be Object of B, a9,b9 be Object of C such that

         A9: a = a9 & b = b9;

        now

          let x be object;

          thus x in ( Hom (a,b)) implies x in ( Hom (a9,b9))

          proof

            assume

             A10: x in ( Hom (a,b));

            then

            reconsider f = x as Morphism of B;

            reconsider f9 = f as Morphism of C by A5;

            ( cod f) = ( cod f9) by A3, FUNCT_1: 49;

            then

             A11: b = ( cod f9) by A10, CAT_1: 1;

            ( dom f) = ( dom f9) by A2, FUNCT_1: 49;

            then a = ( dom f9) by A10, CAT_1: 1;

            hence thesis by A9, A11;

          end;

          assume

           A12: x in ( Hom (a9,b9));

          then

          reconsider f9 = x as Morphism of C;

          ( Hom (a9,b9)) in H by A9;

          then

          reconsider f = f9 as Morphism of B by A1, A12, TARSKI:def 4;

          ( cod f) = ( cod f9) by A3, FUNCT_1: 49;

          then

           A13: ( cod f) = b9 by A12, CAT_1: 1;

          ( dom f) = ( dom f9) by A2, FUNCT_1: 49;

          then ( dom f) = a9 by A12, CAT_1: 1;

          hence x in ( Hom (a,b)) by A9, A13;

        end;

        hence thesis by TARSKI: 2;

      end;

      reconsider B as Category by Lm1, A1, A2, A3, A4;

      

       A14: for a be Object of B, a9 be Object of C st a = a9 holds ( id a) = ( id a9)

      proof

        let a be Object of B, a9 be Object of C such that

         A15: a = a9;

        

         A16: ( Hom (a9,a9)) in H by A15;

        

         A17: ( id a9) in ( Hom (a9,a9)) by CAT_1: 27;

        then

        reconsider ii = ( id a9) as Morphism of B by A16, A1, TARSKI:def 4;

        

         A18: ( dom ii) = ( dom ( id a9)) by A2, FUNCT_1: 49

        .= a9;

        

         A19: ( cod ii) = ( cod ( id a9)) by A3, FUNCT_1: 49

        .= a9;

        ii in ( Hom (a,a)) by A17, A8, A15;

        then

        reconsider ii as Morphism of a, a by CAT_1:def 5;

        

         A20: for f,g be Morphism of B holds [g, f] in ( dom p) iff (d . g) = (c . f)

        proof

          let f,g be Morphism of B;

          reconsider gg = g, ff = f as Morphism of C by A5;

          

           A21: (d . g) = ( dom gg) & (c . f) = ( cod ff) by A2, A3, FUNCT_1: 49;

          thus [g, f] in ( dom p) implies (d . g) = (c . f)

          proof

            assume [g, f] in ( dom p);

            then [g, f] in (( dom the Comp of C) /\ [:M, M:]) by A4, RELAT_1: 61;

            then [gg, ff] in ( dom the Comp of C) by XBOOLE_0:def 4;

            hence thesis by A21, CAT_1:def 6;

          end;

          assume (d . g) = (c . f);

          then [g, f] in ( dom the Comp of C) by A21, CAT_1:def 6;

          then [g, f] in (( dom the Comp of C) /\ [:M, M:]) by XBOOLE_0:def 4;

          hence thesis by A4, RELAT_1: 61;

        end;

        for b be Object of B holds (( Hom (a,b)) <> {} implies for f be Morphism of a, b holds (f (*) ii) = f) & (( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (ii (*) f) = f)

        proof

          let b be Object of B;

          b in O;

          then

          reconsider bb = b as Element of C;

          thus ( Hom (a,b)) <> {} implies for f be Morphism of a, b holds (f (*) ii) = f

          proof

            assume

             A22: ( Hom (a,b)) <> {} ;

            let g be Morphism of a, b;

            reconsider gg = g as Morphism of C by A5;

            

             A23: ( dom gg) = ( dom g) by A2, FUNCT_1: 49

            .= a9 by A15, A22, CAT_1: 5;

            

             A24: ( cod ( id a9)) = a9;

            ( cod gg) = ( cod g) by A3, FUNCT_1: 49

            .= bb by A22, CAT_1: 5;

            then

            reconsider gg as Morphism of a9, bb by A23, CAT_1: 4;

            

             A25: ( dom g) = a by A22, CAT_1: 5;

            

            hence (g (*) ii) = (p . (g,ii)) by A19, A20, A15, CAT_1:def 1

            .= (the Comp of C . (gg,( id a9))) by A19, A20, A15, A4, A25, FUNCT_1: 47

            .= (gg (*) ( id a9)) by A23, A24, CAT_1: 16

            .= g by A23, CAT_1: 22;

          end;

          assume

           A26: ( Hom (b,a)) <> {} ;

          let g be Morphism of b, a;

          reconsider gg = g as Morphism of C by A5;

          

           A27: ( cod gg) = ( cod g) by A3, FUNCT_1: 49

          .= a9 by A15, A26, CAT_1: 5;

          

           A28: ( dom ( id a9)) = a9;

          ( dom gg) = ( dom g) by A2, FUNCT_1: 49

          .= bb by A26, CAT_1: 5;

          then

          reconsider gg as Morphism of bb, a9 by A27, CAT_1: 4;

          

           A29: ( cod g) = a by A26, CAT_1: 5;

          

          hence (ii (*) g) = (p . (ii,g)) by A18, A20, A15, CAT_1:def 1

          .= (the Comp of C . (( id a9),gg)) by A18, A20, A15, A4, A29, FUNCT_1: 47

          .= (( id a9) (*) gg) by A27, A28, CAT_1: 16

          .= g by A27, CAT_1: 21;

        end;

        hence ( id a) = ( id a9) by CAT_1:def 12;

      end;

      (for a,b be Object of B, a9,b9 be Object of C st a = a9 & b = b9 holds ( Hom (a,b)) c= ( Hom (a9,b9))) & the Comp of B c= the Comp of C by A4, A8, RELAT_1: 59;

      hence thesis by A14, Def4;

    end;

    theorem :: CAT_2:21

    for O be non empty Subset of the carrier of C, M be non empty set, d,c be Function of M, O, p be PartFunc of [:M, M:], M, i be Function of O, M st M = ( union { ( Hom (a,b)) where a be Object of C, b be Object of C : a in O & b in O }) & d = (the Source of C | M) & c = (the Target of C | M) & p = (the Comp of C || M) holds CatStr (# O, M, d, c, p #) is full Subcategory of C

    proof

      let O be non empty Subset of the carrier of C, M be non empty set, d,c be Function of M, O, p be PartFunc of [:M, M:], M, i be Function of O, M;

      set H = { ( Hom (a,b)) where a be Object of C, b be Object of C : a in O & b in O };

      assume that

       A1: M = ( union H) and

       A2: d = (the Source of C | M) and

       A3: c = (the Target of C | M) and

       A4: p = (the Comp of C || M);

      set B = CatStr (# O, M, d, c, p #);

       A5:

      now

        let f be Morphism of B;

        consider X be set such that

         A6: f in X and

         A7: X in H by A1, TARSKI:def 4;

        ex a,b be Object of C st X = ( Hom (a,b)) & a in O & b in O by A7;

        hence f is Morphism of C by A6;

      end;

      

       A8: for a,b be Object of B, a9,b9 be Object of C st a = a9 & b = b9 holds ( Hom (a,b)) = ( Hom (a9,b9))

      proof

        let a,b be Object of B, a9,b9 be Object of C such that

         A9: a = a9 & b = b9;

        now

          let x be object;

          thus x in ( Hom (a,b)) implies x in ( Hom (a9,b9))

          proof

            assume

             A10: x in ( Hom (a,b));

            then

            reconsider f = x as Morphism of B;

            reconsider f9 = f as Morphism of C by A5;

            ( cod f) = ( cod f9) by A3, FUNCT_1: 49;

            then

             A11: b = ( cod f9) by A10, CAT_1: 1;

            ( dom f) = ( dom f9) by A2, FUNCT_1: 49;

            then a = ( dom f9) by A10, CAT_1: 1;

            hence thesis by A9, A11;

          end;

          assume

           A12: x in ( Hom (a9,b9));

          then

          reconsider f9 = x as Morphism of C;

          ( Hom (a9,b9)) in H by A9;

          then

          reconsider f = f9 as Morphism of B by A1, A12, TARSKI:def 4;

          ( cod f) = ( cod f9) by A3, FUNCT_1: 49;

          then

           A13: ( cod f) = b9 by A12, CAT_1: 1;

          ( dom f) = ( dom f9) by A2, FUNCT_1: 49;

          then ( dom f) = a9 by A12, CAT_1: 1;

          hence x in ( Hom (a,b)) by A9, A13;

        end;

        hence thesis by TARSKI: 2;

      end;

      reconsider B as Subcategory of C by Lm2, A1, A2, A3, A4;

      B is full by A8;

      hence thesis;

    end;

    theorem :: CAT_2:22

    for O be non empty Subset of the carrier of C, M be non empty set, d,c be Function of M, O, p be PartFunc of [:M, M:], M st CatStr (# O, M, d, c, p #) is full Subcategory of C holds M = ( union { ( Hom (a,b)) where a be Object of C, b be Object of C : a in O & b in O }) & d = (the Source of C | M) & c = (the Target of C | M) & p = (the Comp of C || M)

    proof

      let O be non empty Subset of the carrier of C, M be non empty set, d,c be Function of M, O, p be PartFunc of [:M, M:], M;

      set H = { ( Hom (a,b)) where a be Object of C, b be Object of C : a in O & b in O };

      set B = CatStr (# O, M, d, c, p #);

      assume

       A1: B is full Subcategory of C;

      

       A2: for f be Morphism of B holds (d . f) = (the Source of C . f) & (c . f) = (the Target of C . f)

      proof

        let f be Morphism of B;

        reconsider f9 = f as Morphism of C by A1, Th4;

        ( dom f) = ( dom f9) & ( cod f) = ( cod f9) by A1, Th5;

        hence thesis;

      end;

      now

        let x be object;

        thus x in M implies x in ( union H)

        proof

          assume x in M;

          then

          reconsider f = x as Morphism of B;

          reconsider f9 = f as Morphism of C by A1, Th4;

          set a9 = ( dom f9), b9 = ( cod f9);

          (the Source of B . f) = (the Source of C . f9) & (the Target of B . f) = (the Target of C . f9) by A2;

          then f in ( Hom (a9,b9)) & ( Hom (a9,b9)) in H;

          hence thesis by TARSKI:def 4;

        end;

        assume x in ( union H);

        then

        consider X be set such that

         A3: x in X and

         A4: X in H by TARSKI:def 4;

        consider a9,b9 be Object of C such that

         A5: X = ( Hom (a9,b9)) and

         A6: a9 in O & b9 in O by A4;

        reconsider a = a9, b = b9 as Object of B by A6;

        ( Hom (a,b)) = ( Hom (a9,b9)) by A1, Def6;

        hence x in M by A3, A5;

      end;

      hence M = ( union H) by TARSKI: 2;

      then

      reconsider d9 = (the Source of C | M), c9 = (the Target of C | M) as Function of M, O by Th16;

      set p9 = (the Comp of C || M);

      now

        let f be Element of M;

        (d . f) = (the Source of C . f) by A2;

        hence (d . f) = (d9 . f) by FUNCT_1: 49;

      end;

      hence d = (the Source of C | M) by FUNCT_2: 63;

      now

        let f be Element of M;

        (c . f) = (the Target of C . f) by A2;

        hence (c . f) = (c9 . f) by FUNCT_1: 49;

      end;

      hence c = (the Target of C | M) by FUNCT_2: 63;

      now

        

         A7: ( dom p) c= [:M, M:] by RELAT_1:def 18;

        

         A8: ( dom p9) = (( dom the Comp of C) /\ [:M, M:]) by RELAT_1: 61;

        the Comp of B c= the Comp of C by A1, Def4;

        then ( dom p) c= ( dom the Comp of C) by GRFUNC_1: 2;

        then

         A9: ( dom p) c= ( dom p9) by A7, A8, XBOOLE_1: 19;

        ( dom p9) c= ( dom p)

        proof

          let x be object;

          assume

           A10: x in ( dom p9);

          then x in [:M, M:] by A8, XBOOLE_0:def 4;

          then

          consider g,f be Element of M such that

           A11: x = [g, f] by DOMAIN_1: 1;

          reconsider f, g as Morphism of B;

          reconsider f9 = f, g9 = g as Morphism of C by A1, Th4;

           [g, f] in ( dom the Comp of C) by A8, A10, A11, XBOOLE_0:def 4;

          then

           A12: ( dom g9) = ( cod f9) by CAT_1: 15;

          ( cod f) = ( cod f9) & ( dom g) = ( dom g9) by A1, Th5;

          hence thesis by A1, A11, A12, CAT_1: 15;

        end;

        hence ( dom p) = ( dom p9) by A9, XBOOLE_0:def 10;

        let x be object;

        assume

         A13: x in ( dom p);

        then

        consider g,f be Element of M such that

         A14: x = [g, f] by A7, DOMAIN_1: 1;

        reconsider f, g as Morphism of B;

        

         A15: ( dom g) = ( cod f) by A1, A13, A14, CAT_1: 15;

        reconsider f9 = f, g9 = g as Morphism of C by A1, Th4;

        

         A16: ( cod f) = ( cod f9) & ( dom g) = ( dom g9) by A1, Th5;

        (p . x) = (p . (g,f)) by A14;

        

        hence (p . x) = (g (*) f) by A1, A15, CAT_1: 16

        .= (g9 (*) f9) by A1, A15, Th7

        .= (the Comp of C . (g9,f9)) by A16, A1, A13, A14, CAT_1: 15, CAT_1: 16

        .= (p9 . x) by A9, A13, A14, FUNCT_1: 47;

      end;

      hence p = (the Comp of C || M) by FUNCT_1: 2;

    end;

    definition

      let C, D;

      :: CAT_2:def7

      func [:C,D:] -> Category equals CatStr (# [:the carrier of C, the carrier of D:], [:the carrier' of C, the carrier' of D:], [:the Source of C, the Source of D:], [:the Target of C, the Target of D:], |:the Comp of C, the Comp of D:| #);

      coherence

      proof

        set O = [:the carrier of C, the carrier of D:], M = [:the carrier' of C, the carrier' of D:], d = [:the Source of C, the Source of D:], c = [:the Target of C, the Target of D:], p = |:the Comp of C, the Comp of D:|;

        

         A1: for f,g be Element of M st (d . g) = (c . f) holds [(g `1 ), (f `1 )] in ( dom the Comp of C) & [(g `2 ), (f `2 )] in ( dom the Comp of D)

        proof

          let f,g be Element of M;

          

           A2: (d . ((g `1 ),(g `2 ))) = [(the Source of C . (g `1 )), (the Source of D . (g `2 ))] & (c . ((f `1 ),(f `2 ))) = [(the Target of C . (f `1 )), (the Target of D . (f `2 ))] by FUNCT_3: 75;

          assume

           A3: (d . g) = (c . f);

          g = [(g `1 ), (g `2 )] & f = [(f `1 ), (f `2 )] by MCART_1: 21;

          then ( dom (g `1 )) = ( cod (f `1 )) & ( dom (g `2 )) = ( cod (f `2 )) by A2, A3, XTUPLE_0: 1;

          hence thesis by CAT_1:def 6;

        end;

        

         A4: for f,g be Element of M st [g, f] in ( dom p) holds ( dom (g `1 )) = ( cod (f `1 )) & ( dom (g `2 )) = ( cod (f `2 ))

        proof

          let f,g be Element of M;

          assume

           A5: [g, f] in ( dom p);

          g = [(g `1 ), (g `2 )] & f = [(f `1 ), (f `2 )] by MCART_1: 21;

          then [(g `1 ), (f `1 )] in ( dom the Comp of C) & [(g `2 ), (f `2 )] in ( dom the Comp of D) by A5, FUNCT_4: 54;

          hence thesis by CAT_1:def 6;

        end;

        set B = CatStr (# O, M, d, c, p #);

        

         A6: B is Category-like

        proof

          let ff,gg be Morphism of B;

          reconsider f = ff, g = gg as Element of M;

          

           A7: g = [(g `1 ), (g `2 )] & f = [(f `1 ), (f `2 )] by MCART_1: 21;

          thus [gg, ff] in ( dom the Comp of B) implies ( dom gg) = ( cod ff)

          proof

            

             A8: (d . ((g `1 ),(g `2 ))) = [( dom (g `1 )), ( dom (g `2 ))] & (c . ((f `1 ),(f `2 ))) = [( cod (f `1 )), ( cod (f `2 ))] by FUNCT_3: 75;

            assume

             A9: [gg, ff] in ( dom the Comp of B);

            then ( dom (g `1 )) = ( cod (f `1 )) by A4;

            hence thesis by A4, A7, A9, A8;

          end;

          assume ( dom gg) = ( cod ff);

          then [(g `1 ), (f `1 )] in ( dom the Comp of C) & [(g `2 ), (f `2 )] in ( dom the Comp of D) by A1;

          hence thesis by A7, FUNCT_4: 54;

        end;

        

         A10: for f,g be Morphism of B holds [g, f] in ( dom the Comp of B) iff ( dom g) = ( cod f) by A6;

        

         A11: for f,g be Element of M st (d . g) = (c . f) holds (p . (g,f)) = [(the Comp of C . ((g `1 ),(f `1 ))), (the Comp of D . ((g `2 ),(f `2 )))]

        proof

          let f,g be Element of M;

          reconsider ff = f, gg = g as Morphism of B;

          assume (d . g) = (c . f);

          then

           A12: ( dom gg) = ( cod ff);

          g = [(g `1 ), (g `2 )] & f = [(f `1 ), (f `2 )] by MCART_1: 21;

          hence thesis by A12, A10, FUNCT_4: 55;

        end;

        

         A13: for f,g be Element of M st (d . g) = (c . f) holds (d . (p . (g,f))) = (d . f) & (c . (p . (g,f))) = (c . g)

        proof

          let f,g be Element of M;

          reconsider ff = f, gg = g as Morphism of B;

          

           A14: f = [(f `1 ), (f `2 )] & (d . ((f `1 ),(f `2 ))) = [( dom (f `1 )), ( dom (f `2 ))] by FUNCT_3: 75, MCART_1: 21;

          assume

           A15: (d . g) = (c . f);

          then

           A16: (the Comp of C . [(g `1 ), (f `1 )]) in the carrier' of C by A1, PARTFUN1: 4;

          then

           A17: (the Comp of C . ((g `1 ),(f `1 ))) in ( dom the Source of C) by FUNCT_2:def 1;

          ( dom gg) = ( cod ff) by A15;

          then

           A18: [gg, ff] in ( dom p) by A6;

          then

           A19: ( dom (g `1 )) = ( cod (f `1 )) by A4;

          then [(g `1 ), (f `1 )] in ( dom the Comp of C) by CAT_1:def 6;

          then

           A20: (the Comp of C . ((g `1 ),(f `1 ))) = ((g `1 ) (*) (f `1 )) by CAT_1:def 1;

          

           A21: ( dom ((g `1 ) (*) (f `1 ))) = ( dom (f `1 )) by A19, CAT_1:def 7;

          

           A22: (the Comp of D . [(g `2 ), (f `2 )]) in the carrier' of D by A1, A15, PARTFUN1: 4;

          then

           A23: (the Comp of D . ((g `2 ),(f `2 ))) in ( dom the Source of D) by FUNCT_2:def 1;

          

           A24: ( dom (g `2 )) = ( cod (f `2 )) by A4, A18;

          then [(g `2 ), (f `2 )] in ( dom the Comp of D) by CAT_1:def 6;

          then

           A25: (the Comp of D . ((g `2 ),(f `2 ))) = ((g `2 ) (*) (f `2 )) by CAT_1:def 1;

          

           A26: ( dom ((g `2 ) (*) (f `2 ))) = ( dom (f `2 )) by A24, CAT_1:def 7;

          

          thus (d . (p . (g,f))) = (d . ((the Comp of C . ((g `1 ),(f `1 ))),(the Comp of D . ((g `2 ),(f `2 ))))) by A11, A15

          .= (d . f) by A14, A21, A26, A17, A23, A20, A25, FUNCT_3:def 8;

          

           A27: g = [(g `1 ), (g `2 )] & (c . ((g `1 ),(g `2 ))) = [(the Target of C . (g `1 )), (the Target of D . (g `2 ))] by FUNCT_3: 75, MCART_1: 21;

          

           A28: ( cod ((g `2 ) (*) (f `2 ))) = ( cod (g `2 )) by A24, CAT_1:def 7;

          

           A29: ( cod ((g `1 ) (*) (f `1 ))) = ( cod (g `1 )) by A19, CAT_1:def 7;

          

           A30: (the Comp of D . ((g `2 ),(f `2 ))) in ( dom the Target of D) by A22, FUNCT_2:def 1;

          

           A31: (the Comp of C . ((g `1 ),(f `1 ))) in ( dom the Target of C) by A16, FUNCT_2:def 1;

          

          thus (c . (p . (g,f))) = (c . ((the Comp of C . ((g `1 ),(f `1 ))),(the Comp of D . ((g `2 ),(f `2 ))))) by A11, A15

          .= (c . g) by A27, A29, A28, A31, A30, A20, A25, FUNCT_3:def 8;

        end;

        

         A32: B is transitive

        proof

          let ff,gg be Morphism of B;

          reconsider f = ff, g = gg as Element of M;

          assume

           A33: ( dom gg) = ( cod ff);

          then

           A34: (the Comp of B . (gg,ff)) = (gg (*) ff) by A10, CAT_1:def 1;

          thus ( dom (gg (*) ff)) = ( dom ff) by A13, A33, A34;

          thus ( cod (gg (*) ff)) = ( cod gg) by A13, A33, A34;

        end;

        

         A35: B is associative

        proof

          let ff,gg,hh be Morphism of B;

          reconsider f = ff, g = gg, h = hh as Element of M;

          assume that

           A36: ( dom hh) = ( cod gg) and

           A37: ( dom gg) = ( cod ff);

          

           A38: (the Comp of C . [(h `1 ), (g `1 )]) in the carrier' of C & (the Comp of D . [(h `2 ), (g `2 )]) in the carrier' of D by A1, A36, PARTFUN1: 4;

          (the Comp of C . [(g `1 ), (f `1 )]) in the carrier' of C & (the Comp of D . [(g `2 ), (f `2 )]) in the carrier' of D by A1, A37, PARTFUN1: 4;

          then

          reconsider pgf = [(the Comp of C . [(g `1 ), (f `1 )]), (the Comp of D . [(g `2 ), (f `2 )])], phg = [(the Comp of C . [(h `1 ), (g `1 )]), (the Comp of D . [(h `2 ), (g `2 )])] as Element of M by A38, ZFMISC_1: 87;

          set pgf2 = (pgf `2 ), phg2 = (phg `2 );

          set pgf1 = (pgf `1 ), phg1 = (phg `1 );

          

           A39: (p . (g,f)) = [(the Comp of C . ((g `1 ),(f `1 ))), (the Comp of D . ((g `2 ),(f `2 )))] by A11, A37;

          

           A40: (d . h) = (c . (p . (g,f))) by A13, A36, A37;

          

           A41: (p . (h,g)) = [(the Comp of C . ((h `1 ),(g `1 ))), (the Comp of D . ((h `2 ),(g `2 )))] by A11, A36;

           [(h `2 ), (g `2 )] in ( dom the Comp of D) by A1, A36;

          then

           A42: ( dom (h `2 )) = ( cod (g `2 )) by CAT_1:def 6;

           [(h `1 ), (g `1 )] in ( dom the Comp of C) by A1, A36;

          then

           A43: ( dom (h `1 )) = ( cod (g `1 )) by CAT_1:def 6;

           [(g `2 ), (f `2 )] in ( dom the Comp of D) by A1, A37;

          then

           A44: ( dom (g `2 )) = ( cod (f `2 )) by CAT_1:def 6;

           [(g `1 ), (f `1 )] in ( dom the Comp of C) by A1, A37;

          then

           A45: ( dom (g `1 )) = ( cod (f `1 )) by CAT_1:def 6;

          

           A46: (d . (p . (h,g))) = (c . f) by A13, A36, A37;

          

           A47: (pgf `1 ) = (the Comp of C . ((g `1 ),(f `1 ))) & (phg `1 ) = (the Comp of C . ((h `1 ),(g `1 )));

          

           A48: (pgf `2 ) = (the Comp of D . ((g `2 ),(f `2 ))) & (phg `2 ) = (the Comp of D . ((h `2 ),(g `2 )));

          

           A49: ((h `2 ) (*) ((g `2 ) (*) (f `2 ))) = (((h `2 ) (*) (g `2 )) (*) (f `2 )) by A42, A44, CAT_1:def 8;

          

           A50: (gg (*) ff) = (p . (g,f)) by A37, A10, CAT_1:def 1;

          then

           A51: ( cod (gg (*) ff)) = ( dom hh) by A13, A36, A37;

          

           A52: (hh (*) gg) = (p . (h,g)) by A36, A10, CAT_1:def 1;

          then

           A53: ( dom (hh (*) gg)) = ( cod ff) by A13, A36, A37;

          

           A54: ( cod ((g `1 ) (*) (f `1 ))) = ( cod (g `1 )) by A45, CAT_1:def 7;

          

           A55: pgf1 = ((g `1 ) (*) (f `1 )) by A47, A45, CAT_1: 16;

          

           A56: ( cod ((g `2 ) (*) (f `2 ))) = ( cod (g `2 )) by A44, CAT_1:def 7;

          pgf2 = ((g `2 ) (*) (f `2 )) by A48, A44, CAT_1: 16;

          then

           A57: (the Comp of D . ((h `2 ),pgf2)) = ((h `2 ) (*) ((g `2 ) (*) (f `2 ))) by A42, A56, CAT_1: 16;

          

           A58: ( dom ((h `1 ) (*) (g `1 ))) = ( dom (g `1 )) by A43, CAT_1:def 7;

          

           A59: phg1 = ((h `1 ) (*) (g `1 )) by A47, A43, CAT_1: 16;

          

           A60: ( dom ((h `2 ) (*) (g `2 ))) = ( dom (g `2 )) by A42, CAT_1:def 7;

          phg2 = ((h `2 ) (*) (g `2 )) by A48, A42, CAT_1: 16;

          then

           A61: (the Comp of D . (phg2,(f `2 ))) = (((h `2 ) (*) (g `2 )) (*) (f `2 )) by A44, A60, CAT_1: 16;

          

          thus (hh (*) (gg (*) ff)) = (p . (h,(p . (g,f)))) by A51, A50, A10, CAT_1:def 1

          .= [(the Comp of C . ((h `1 ),pgf1)), (the Comp of D . ((h `2 ),pgf2))] by A40, A11, A39

          .= [((h `1 ) (*) ((g `1 ) (*) (f `1 ))), ((h `2 ) (*) ((g `2 ) (*) (f `2 )))] by A55, A57, A43, A54, CAT_1: 16

          .= [(((h `1 ) (*) (g `1 )) (*) (f `1 )), (((h `2 ) (*) (g `2 )) (*) (f `2 ))] by A43, A45, A49, CAT_1:def 8

          .= [(the Comp of C . (phg1,(f `1 ))), (the Comp of D . (phg2,(f `2 )))] by A59, A61, A45, A58, CAT_1: 16

          .= (p . ((p . (h,g)),f)) by A46, A11, A41

          .= ((hh (*) gg) (*) ff) by A53, A10, A52, CAT_1:def 1;

        end;

        

         A62: B is reflexive

        proof

          let b be Element of B;

          reconsider bb = b as Element of O;

          reconsider ii = [( id (bb `1 )), ( id (bb `2 ))] as Morphism of B;

          

           A63: ( cod ii) = (c . (( id (bb `1 )),( id (bb `2 ))))

          .= [( cod ( id (bb `1 ))), ( cod ( id (bb `2 )))] by FUNCT_3: 75

          .= [(bb `1 ), ( cod ( id (bb `2 )))]

          .= [(bb `1 ), (bb `2 )]

          .= bb by MCART_1: 21;

          ( dom ii) = (d . (( id (bb `1 )),( id (bb `2 ))))

          .= [( dom ( id (bb `1 ))), ( dom ( id (bb `2 )))] by FUNCT_3: 75

          .= [(bb `1 ), ( dom ( id (bb `2 )))]

          .= [(bb `1 ), (bb `2 )]

          .= bb by MCART_1: 21;

          then [( id (bb `1 )), ( id (bb `2 ))] in ( Hom (b,b)) by A63;

          hence ( Hom (b,b)) <> {} ;

        end;

        B is with_identities

        proof

          let a be Element of B;

          reconsider aa = a as Element of O;

          reconsider ii = [( id (aa `1 )), ( id (aa `2 ))] as Morphism of B;

          

           A64: ( cod ii) = (c . (( id (aa `1 )),( id (aa `2 ))))

          .= [( cod ( id (aa `1 ))), ( cod ( id (aa `2 )))] by FUNCT_3: 75

          .= [(aa `1 ), ( cod ( id (aa `2 )))]

          .= [(aa `1 ), (aa `2 )]

          .= aa by MCART_1: 21;

          

           A65: ( dom ii) = (d . (( id (aa `1 )),( id (aa `2 ))))

          .= [( dom ( id (aa `1 ))), ( dom ( id (aa `2 )))] by FUNCT_3: 75

          .= [(aa `1 ), ( dom ( id (aa `2 )))]

          .= [(aa `1 ), (aa `2 )]

          .= aa by MCART_1: 21;

          then

          reconsider ii = [( id (aa `1 )), ( id (aa `2 ))] as Morphism of a, a by A64, CAT_1: 4;

          take ii;

          let b be Element of B;

          thus ( Hom (a,b)) <> {} implies for g be Morphism of a, b holds (g (*) ii) = g

          proof

            assume

             A66: ( Hom (a,b)) <> {} ;

            let g be Morphism of a, b;

            reconsider gg = g as Element of M;

            ( cod ii) = ( dom g) by A66, A64, CAT_1: 5;

            then

             A67: [g, ii] in ( dom p) by A6;

            

            then

             A68: ( dom (gg `1 )) = ( cod ( [( id (aa `1 )), ( id (aa `2 ))] `1 )) by A4

            .= ( cod ( id (aa `1 )));

            

             A69: (the Comp of C . ((gg `1 ),( id (aa `1 )))) = ((gg `1 ) (*) ( id (aa `1 ))) by A68, CAT_1: 16

            .= (gg `1 ) by A68, CAT_1: 22;

            

             A70: ( dom (gg `2 )) = ( cod ( [( id (aa `1 )), ( id (aa `2 ))] `2 )) by A4, A67

            .= ( cod ( id (aa `2 )));

            

             A71: (the Comp of D . ((gg `2 ),( id (aa `2 )))) = ((gg `2 ) (*) ( id (aa `2 ))) by A70, CAT_1: 16

            .= (gg `2 ) by A70, CAT_1: 22;

            

             A72: ( cod ii) = ( dom g) by A64, A66, CAT_1: 5;

            then [g, ii] in ( dom the Comp of B) by A6;

            

            hence (g (*) ii) = (p . (g,ii)) by CAT_1:def 1

            .= [(the Comp of C . ((gg `1 ),( [( id (aa `1 )), ( id (aa `2 ))] `1 ))), (the Comp of D . ((gg `2 ),( [( id (aa `1 )), ( id (aa `2 ))] `2 )))] by A11, A72

            .= g by A69, A71, MCART_1: 21;

          end;

          assume

           A73: ( Hom (b,a)) <> {} ;

          let g be Morphism of b, a;

          reconsider gg = g as Element of M;

          ( dom ii) = ( cod g) by A73, A65, CAT_1: 5;

          then

           A74: [ii, g] in ( dom p) by A6;

          

          then

           A75: ( cod (gg `1 )) = ( dom ( [( id (aa `1 )), ( id (aa `2 ))] `1 )) by A4

          .= ( dom ( id (aa `1 )));

          

           A76: (the Comp of C . (( id (aa `1 )),(gg `1 ))) = (( id (aa `1 )) (*) (gg `1 )) by A75, CAT_1: 16

          .= (gg `1 ) by A75, CAT_1: 21;

          

           A77: ( cod (gg `2 )) = ( dom ( [( id (aa `1 )), ( id (aa `2 ))] `2 )) by A4, A74

          .= ( dom ( id (aa `2 )));

          

           A78: (the Comp of D . (( id (aa `2 )),(gg `2 ))) = (( id (aa `2 )) (*) (gg `2 )) by A77, CAT_1: 16

          .= (gg `2 ) by A77, CAT_1: 21;

          

           A79: ( dom ii) = ( cod g) by A65, A73, CAT_1: 5;

          then [ii, g] in ( dom the Comp of B) by A6;

          

          hence (ii (*) g) = (p . (ii,g)) by CAT_1:def 1

          .= [(the Comp of C . (( [( id (aa `1 )), ( id (aa `2 ))] `1 ),(gg `1 ))), (the Comp of D . (( [( id (aa `1 )), ( id (aa `2 ))] `2 ),(gg `2 )))] by A11, A79

          .= g by A76, A78, MCART_1: 21;

        end;

        hence thesis by A6, A32, A35, A62;

      end;

    end

    theorem :: CAT_2:23

    the carrier of [:C, D:] = [:the carrier of C, the carrier of D:] & the carrier' of [:C, D:] = [:the carrier' of C, the carrier' of D:] & the Source of [:C, D:] = [:the Source of C, the Source of D:] & the Target of [:C, D:] = [:the Target of C, the Target of D:] & the Comp of [:C, D:] = |:the Comp of C, the Comp of D:|;

    definition

      let C, D;

      let c be Object of C;

      let d be Object of D;

      :: original: [

      redefine

      func [c,d] -> Object of [:C, D:] ;

      coherence

      proof

        thus [c, d] is Object of [:C, D:];

      end;

    end

    ::$Canceled

    theorem :: CAT_2:25

    for cd be Object of [:C, D:] holds ex c be Object of C, d be Object of D st cd = [c, d] by DOMAIN_1: 1;

    definition

      let C, D;

      let f be Morphism of C;

      let g be Morphism of D;

      :: original: [

      redefine

      func [f,g] -> Morphism of [:C, D:] ;

      coherence

      proof

        thus [f, g] is Morphism of [:C, D:];

      end;

    end

    ::$Canceled

    theorem :: CAT_2:27

    for fg be Morphism of [:C, D:] holds ex f be Morphism of C, g be Morphism of D st fg = [f, g] by DOMAIN_1: 1;

    theorem :: CAT_2:28

    

     Th22: for f be Morphism of C holds for g be Morphism of D holds ( dom [f, g]) = [( dom f), ( dom g)] & ( cod [f, g]) = [( cod f), ( cod g)]

    proof

      let f be Morphism of C;

      let g be Morphism of D;

      

      thus ( dom [f, g]) = ( [:the Source of C, the Source of D:] . (f,g))

      .= [( dom f), ( dom g)] by FUNCT_3: 75;

      

      thus ( cod [f, g]) = ( [:the Target of C, the Target of D:] . (f,g))

      .= [( cod f), ( cod g)] by FUNCT_3: 75;

    end;

    theorem :: CAT_2:29

    

     Th23: for f,f9 be Morphism of C holds for g,g9 be Morphism of D st ( dom f9) = ( cod f) & ( dom g9) = ( cod g) holds ( [f9, g9] (*) [f, g]) = [(f9 (*) f), (g9 (*) g)]

    proof

      let f,f9 be Morphism of C;

      let g,g9 be Morphism of D;

      assume that

       A1: ( dom f9) = ( cod f) and

       A2: ( dom g9) = ( cod g);

      

       A3: [f9, f] in ( dom the Comp of C) & [g9, g] in ( dom the Comp of D) by A1, A2, CAT_1: 15;

      ( dom [f9, g9]) = [( dom f9), ( dom g9)] & ( cod [f, g]) = [( cod f), ( cod g)] by Th22;

      

      hence ( [f9, g9] (*) [f, g]) = ( |:the Comp of C, the Comp of D:| . ( [f9, g9], [f, g])) by A1, A2, CAT_1: 16

      .= [(the Comp of C . (f9,f)), (the Comp of D . (g9,g))] by A3, FUNCT_4:def 3

      .= [(f9 (*) f), (the Comp of D . (g9,g))] by A1, CAT_1: 16

      .= [(f9 (*) f), (g9 (*) g)] by A2, CAT_1: 16;

    end;

    theorem :: CAT_2:30

    

     Th24: for f,f9 be Morphism of C holds for g,g9 be Morphism of D st ( dom [f9, g9]) = ( cod [f, g]) holds ( [f9, g9] (*) [f, g]) = [(f9 (*) f), (g9 (*) g)]

    proof

      let f,f9 be Morphism of C;

      let g,g9 be Morphism of D such that

       A1: ( dom [f9, g9]) = ( cod [f, g]);

       [( dom f9), ( dom g9)] = ( dom [f9, g9]) & ( cod [f, g]) = [( cod f), ( cod g)] by Th22;

      then ( dom f9) = ( cod f) & ( dom g9) = ( cod g) by A1, XTUPLE_0: 1;

      hence thesis by Th23;

    end;

    theorem :: CAT_2:31

    

     Th25: for c be Object of C, d be Object of D holds ( id [c, d]) = [( id c), ( id d)]

    proof

      let c be Object of C;

      let d be Object of D;

      

       A1: ( dom [( id c), ( id d)]) = [( dom ( id c)), ( dom ( id d))] by Th22

      .= [c, ( dom ( id d))]

      .= [c, d];

      ( cod [( id c), ( id d)]) = [( cod ( id c)), ( cod ( id d))] by Th22

      .= [c, ( cod ( id d))]

      .= [c, d];

      then

      reconsider m = [( id c), ( id d)] as Morphism of [c, d], [c, d] by A1, CAT_1: 4;

      for b be Object of [:C, D:] holds (( Hom ( [c, d],b)) <> {} implies for f be Morphism of [c, d], b holds (f (*) [( id c), ( id d)]) = f) & (( Hom (b, [c, d])) <> {} implies for f be Morphism of b, [c, d] holds ( [( id c), ( id d)] (*) f) = f)

      proof

        let b be Object of [:C, D:];

        thus ( Hom ( [c, d],b)) <> {} implies for f be Morphism of [c, d], b holds (f (*) [( id c), ( id d)]) = f

        proof

          assume

           A2: ( Hom ( [c, d],b)) <> {} ;

          let f be Morphism of [c, d], b;

          consider fc be Morphism of C, fd be Morphism of D such that

           A3: f = [fc, fd] by DOMAIN_1: 1;

          

           A4: [c, d] = ( dom f) by A2, CAT_1: 5

          .= [( dom fc), ( dom fd)] by A3, Th22;

          then

           A5: c = ( dom fc) by XTUPLE_0: 1;

          then

           A6: ( cod ( id c)) = ( dom fc);

          

           A7: d = ( dom fd) by A4, XTUPLE_0: 1;

          then ( cod ( id d)) = ( dom fd);

          

          hence (f (*) [( id c), ( id d)]) = [(fc (*) ( id c)), (fd (*) ( id d))] by A3, A6, Th23

          .= [fc, (fd (*) ( id d))] by A5, CAT_1: 22

          .= f by A3, A7, CAT_1: 22;

        end;

        assume

         A8: ( Hom (b, [c, d])) <> {} ;

        let f be Morphism of b, [c, d];

        consider fc be Morphism of C, fd be Morphism of D such that

         A9: f = [fc, fd] by DOMAIN_1: 1;

        

         A10: [c, d] = ( cod f) by A8, CAT_1: 5

        .= [( cod fc), ( cod fd)] by A9, Th22;

        then

         A11: c = ( cod fc) by XTUPLE_0: 1;

        then

         A12: ( dom ( id c)) = ( cod fc);

        

         A13: d = ( cod fd) by A10, XTUPLE_0: 1;

        then ( dom ( id d)) = ( cod fd);

        

        hence ( [( id c), ( id d)] (*) f) = [(( id c) (*) fc), (( id d) (*) fd)] by A9, A12, Th23

        .= [fc, (( id d) (*) fd)] by A11, CAT_1: 21

        .= f by A9, A13, CAT_1: 21;

      end;

      then m = ( id [c, d]) by CAT_1:def 12;

      hence thesis;

    end;

    theorem :: CAT_2:32

    for c,c9 be Object of C, d,d9 be Object of D holds ( Hom ( [c, d], [c9, d9])) = [:( Hom (c,c9)), ( Hom (d,d9)):]

    proof

      let c,c9 be Object of C, d,d9 be Object of D;

      now

        let x be object;

        thus x in ( Hom ( [c, d], [c9, d9])) implies x in [:( Hom (c,c9)), ( Hom (d,d9)):]

        proof

          assume

           A1: x in ( Hom ( [c, d], [c9, d9]));

          then

          reconsider fg = x as Morphism of [c, d], [c9, d9] by CAT_1:def 5;

          

           A2: ( dom fg) = [c, d] by A1, CAT_1: 1;

          

           A3: ( cod fg) = [c9, d9] by A1, CAT_1: 1;

          consider x1,x2 be object such that

           A4: x1 in the carrier' of C and

           A5: x2 in the carrier' of D and

           A6: fg = [x1, x2] by ZFMISC_1:def 2;

          reconsider g = x2 as Morphism of D by A5;

          reconsider f = x1 as Morphism of C by A4;

          

           A7: ( cod fg) = [( cod f), ( cod g)] by A6, Th22;

          then

           A8: ( cod f) = c9 by A3, XTUPLE_0: 1;

          

           A9: ( cod g) = d9 by A3, A7, XTUPLE_0: 1;

          

           A10: ( dom fg) = [( dom f), ( dom g)] by A6, Th22;

          then ( dom g) = d by A2, XTUPLE_0: 1;

          then

           A11: g in ( Hom (d,d9)) by A9;

          ( dom f) = c by A2, A10, XTUPLE_0: 1;

          then f in ( Hom (c,c9)) by A8;

          hence thesis by A6, A11, ZFMISC_1: 87;

        end;

        assume x in [:( Hom (c,c9)), ( Hom (d,d9)):];

        then

        consider x1,x2 be object such that

         A12: x1 in ( Hom (c,c9)) and

         A13: x2 in ( Hom (d,d9)) and

         A14: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider g = x2 as Morphism of d, d9 by A13, CAT_1:def 5;

        reconsider f = x1 as Morphism of c, c9 by A12, CAT_1:def 5;

        ( cod f) = c9 & ( cod g) = d9 by A12, A13, CAT_1: 1;

        then

         A15: ( cod [f, g]) = [c9, d9] by Th22;

        ( dom f) = c & ( dom g) = d by A12, A13, CAT_1: 1;

        then ( dom [f, g]) = [c, d] by Th22;

        hence x in ( Hom ( [c, d], [c9, d9])) by A14, A15;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: CAT_2:33

    for c,c9 be Object of C, f be Morphism of c, c9, d,d9 be Object of D, g be Morphism of d, d9 st ( Hom (c,c9)) <> {} & ( Hom (d,d9)) <> {} holds [f, g] is Morphism of [c, d], [c9, d9]

    proof

      let c,c9 be Object of C, f be Morphism of c, c9, d,d9 be Object of D, g be Morphism of d, d9;

      assume

       A1: ( Hom (c,c9)) <> {} & ( Hom (d,d9)) <> {} ;

      then ( cod f) = c9 & ( cod g) = d9 by CAT_1: 5;

      then

       A2: ( cod [f, g]) = [c9, d9] by Th22;

      ( dom f) = c & ( dom g) = d by A1, CAT_1: 5;

      then ( dom [f, g]) = [c, d] by Th22;

      hence thesis by A2, CAT_1: 4;

    end;

    definition

      let C, C9, D;

      let S be Functor of [:C, C9:], D;

      let m be Morphism of C;

      let m9 be Morphism of C9;

      :: original: .

      redefine

      func S . (m,m9) -> Morphism of D ;

      coherence

      proof

        (S . (m,m9)) = (S . [m, m9]);

        hence thesis;

      end;

    end

    theorem :: CAT_2:34

    

     Th28: for S be Functor of [:C, C9:], D, c be Object of C holds (( curry S) . ( id c)) is Functor of C9, D

    proof

      let S be Functor of [:C, C9:], D, c be Object of C;

      reconsider S9 = S as Function of [:the carrier' of C, the carrier' of C9:], the carrier' of D;

      reconsider T = (( curry S9) . ( id c)) as Function of the carrier' of C9, the carrier' of D;

      now

        thus for c9 be Object of C9 holds ex d be Object of D st (T . ( id c9)) = ( id d)

        proof

          let c9 be Object of C9;

          consider d be Object of D such that

           A1: (S . ( id [c, c9])) = ( id d) by CAT_1: 62;

          take d;

          

          thus (T . ( id c9)) = (S . (( id c),( id c9))) by FUNCT_5: 69

          .= ( id d) by A1, Th25;

        end;

        

         A2: ( dom ( id c)) = c & ( cod ( id c)) = c;

        thus for f be Morphism of C9 holds (T . ( id ( dom f))) = ( id ( dom (T . f))) & (T . ( id ( cod f))) = ( id ( cod (T . f)))

        proof

          let f be Morphism of C9;

          

          thus (T . ( id ( dom f))) = (S . (( id c),( id ( dom f)))) by FUNCT_5: 69

          .= (S . ( id [c, ( dom f)])) by Th25

          .= (S . ( id [( dom ( id c)), ( dom f)]))

          .= (S . ( id ( dom [( id c), f]))) by Th22

          .= ( id ( dom (S . (( id c),f)))) by CAT_1: 63

          .= ( id ( dom (T . f))) by FUNCT_5: 69;

          

          thus (T . ( id ( cod f))) = (S . (( id c),( id ( cod f)))) by FUNCT_5: 69

          .= (S . ( id [c, ( cod f)])) by Th25

          .= (S . ( id [( cod ( id c)), ( cod f)]))

          .= (S . ( id ( cod [( id c), f]))) by Th22

          .= ( id ( cod (S . (( id c),f)))) by CAT_1: 63

          .= ( id ( cod (T . f))) by FUNCT_5: 69;

        end;

        let f,g be Morphism of C9 such that

         A3: ( dom g) = ( cod f);

        ( Hom (c,c)) <> {} ;

        then

         A4: (( id c) * ( id c)) = (( id c) (*) ( id c)) by CAT_1:def 13;

        

         A5: ( dom [( id c), g]) = [( dom ( id c)), ( dom g)] & ( cod [( id c), f]) = [( cod ( id c)), ( cod f)] by Th22;

        

        thus (T . (g (*) f)) = (S . ((( id c) * ( id c)),(g (*) f))) by FUNCT_5: 69

        .= (S . ( [( id c), g] (*) [( id c), f])) by A3, A2, A4, Th23

        .= ((S . (( id c),g)) (*) (S . (( id c),f))) by A3, A5, CAT_1: 64

        .= ((T . g) (*) (S . (( id c),f))) by FUNCT_5: 69

        .= ((T . g) (*) (T . f)) by FUNCT_5: 69;

      end;

      hence thesis by CAT_1: 61;

    end;

    theorem :: CAT_2:35

    

     Th29: for S be Functor of [:C, C9:], D, c9 be Object of C9 holds (( curry' S) . ( id c9)) is Functor of C, D

    proof

      let S be Functor of [:C, C9:], D, c9 be Object of C9;

      reconsider S9 = S as Function of [:the carrier' of C, the carrier' of C9:], the carrier' of D;

      reconsider T = (( curry' S9) . ( id c9)) as Function of the carrier' of C, the carrier' of D;

      now

        thus for c be Object of C holds ex d be Object of D st (T . ( id c)) = ( id d)

        proof

          let c be Object of C;

          consider d be Object of D such that

           A1: (S . ( id [c, c9])) = ( id d) by CAT_1: 62;

          take d;

          

          thus (T . ( id c)) = (S . (( id c),( id c9))) by FUNCT_5: 70

          .= ( id d) by A1, Th25;

        end;

        

         A2: ( dom ( id c9)) = c9 & ( cod ( id c9)) = c9;

        thus for f be Morphism of C holds (T . ( id ( dom f))) = ( id ( dom (T . f))) & (T . ( id ( cod f))) = ( id ( cod (T . f)))

        proof

          let f be Morphism of C;

          

          thus (T . ( id ( dom f))) = (S . (( id ( dom f)),( id c9))) by FUNCT_5: 70

          .= (S . ( id [( dom f), c9])) by Th25

          .= (S . ( id [( dom f), ( dom ( id c9))]))

          .= (S . ( id ( dom [f, ( id c9)]))) by Th22

          .= ( id ( dom (S . (f,( id c9))))) by CAT_1: 63

          .= ( id ( dom (T . f))) by FUNCT_5: 70;

          

          thus (T . ( id ( cod f))) = (S . (( id ( cod f)),( id c9))) by FUNCT_5: 70

          .= (S . ( id [( cod f), c9])) by Th25

          .= (S . ( id [( cod f), ( cod ( id c9))]))

          .= (S . ( id ( cod [f, ( id c9)]))) by Th22

          .= ( id ( cod (S . (f,( id c9))))) by CAT_1: 63

          .= ( id ( cod (T . f))) by FUNCT_5: 70;

        end;

        let f,g be Morphism of C such that

         A3: ( dom g) = ( cod f);

        ( Hom (c9,c9)) <> {} ;

        then

         A4: (( id c9) * ( id c9)) = (( id c9) (*) ( id c9)) by CAT_1:def 13;

        

         A5: ( dom [g, ( id c9)]) = [( dom g), ( dom ( id c9))] & ( cod [f, ( id c9)]) = [( cod f), ( cod ( id c9))] by Th22;

        

        thus (T . (g (*) f)) = (S . ((g (*) f),(( id c9) * ( id c9)))) by FUNCT_5: 70

        .= (S . ( [g, ( id c9)] (*) [f, ( id c9)])) by A3, A2, A4, Th23

        .= ((S . (g,( id c9))) (*) (S . (f,( id c9)))) by A3, A5, CAT_1: 64

        .= ((T . g) (*) (S . (f,( id c9)))) by FUNCT_5: 70

        .= ((T . g) (*) (T . f)) by FUNCT_5: 70;

      end;

      hence thesis by CAT_1: 61;

    end;

    definition

      let C, C9, D;

      let S be Functor of [:C, C9:], D, c be Object of C;

      :: CAT_2:def8

      func S ?- c -> Functor of C9, D equals (( curry S) . ( id c));

      coherence by Th28;

    end

    theorem :: CAT_2:36

    for S be Functor of [:C, C9:], D, c be Object of C, f be Morphism of C9 holds ((S ?- c) . f) = (S . (( id c),f)) by FUNCT_5: 69;

    theorem :: CAT_2:37

    for S be Functor of [:C, C9:], D, c be Object of C, c9 be Object of C9 holds (( Obj (S ?- c)) . c9) = (( Obj S) . (c,c9))

    proof

      let S be Functor of [:C, C9:], D, c be Object of C, c9 be Object of C9;

      ((S ?- c) . ( id c9)) = (S . (( id c),( id c9))) by FUNCT_5: 69

      .= (S . ( id [c, c9])) by Th25

      .= ( id (( Obj S) . [c, c9])) by CAT_1: 68;

      hence thesis by CAT_1: 67;

    end;

    definition

      let C, C9, D;

      let S be Functor of [:C, C9:], D, c9 be Object of C9;

      :: CAT_2:def9

      func S -? c9 -> Functor of C, D equals (( curry' S) . ( id c9));

      coherence by Th29;

    end

    theorem :: CAT_2:38

    for S be Functor of [:C, C9:], D, c9 be Object of C9, f be Morphism of C holds ((S -? c9) . f) = (S . (f,( id c9))) by FUNCT_5: 70;

    theorem :: CAT_2:39

    for S be Functor of [:C, C9:], D, c be Object of C, c9 be Object of C9 holds (( Obj (S -? c9)) . c) = (( Obj S) . (c,c9))

    proof

      let S be Functor of [:C, C9:], D, c be Object of C, c9 be Object of C9;

      ((S -? c9) . ( id c)) = (S . (( id c),( id c9))) by FUNCT_5: 70

      .= (S . ( id [c, c9])) by Th25

      .= ( id (( Obj S) . [c, c9])) by CAT_1: 68;

      hence thesis by CAT_1: 67;

    end;

    theorem :: CAT_2:40

    for L be Function of the carrier of C, ( Funct (B,D)), M be Function of the carrier of B, ( Funct (C,D)) st (for c be Object of C, b be Object of B holds ((M . b) . ( id c)) = ((L . c) . ( id b))) & (for f be Morphism of B holds for g be Morphism of C holds (((M . ( cod f)) . g) (*) ((L . ( dom g)) . f)) = (((L . ( cod g)) . f) (*) ((M . ( dom f)) . g))) holds ex S be Functor of [:B, C:], D st for f be Morphism of B holds for g be Morphism of C holds (S . (f,g)) = (((L . ( cod g)) . f) (*) ((M . ( dom f)) . g))

    proof

      deffunc Mor( Category) = the carrier' of $1;

      let L be Function of the carrier of C, ( Funct (B,D)), M be Function of the carrier of B, ( Funct (C,D)) such that

       A1: for c be Object of C, b be Object of B holds ((M . b) . ( id c)) = ((L . c) . ( id b)) and

       A2: for f be Morphism of B holds for g be Morphism of C holds (((M . ( cod f)) . g) (*) ((L . ( dom g)) . f)) = (((L . ( cod g)) . f) (*) ((M . ( dom f)) . g));

      deffunc F( Element of Mor(B), Element of Mor(C)) = (((L . ( cod $2)) . $1) (*) ((M . ( dom $1)) . $2));

      consider S be Function of [: Mor(B), Mor(C):], Mor(D) such that

       A3: for f be Morphism of B holds for g be Morphism of C holds (S . (f,g)) = F(f,g) from BINOP_1:sch 4;

      reconsider T = S as Function of Mor([:), Mor(D);

      now

        thus for bc be Object of [:B, C:] holds ex d be Object of D st (T . ( id bc)) = ( id d)

        proof

          let bc be Object of [:B, C:];

          consider b be Object of B, c be Object of C such that

           A4: bc = [b, c] by DOMAIN_1: 1;

          consider d be Object of D such that

           A5: ((L . c) . ( id b)) = ( id d) by CAT_1: 62;

          take d;

          ( Hom (d,d)) <> {} ;

          then

           A6: (( id d) * ( id d)) = (( id d) (*) ( id d)) by CAT_1:def 13;

          

           A7: ( cod ( id c)) = c & ( dom ( id b)) = b;

          ((L . c) . ( id b)) = ((M . b) . ( id c)) by A1;

          then (T . (( id b),( id c))) = ( id d) by A3, A5, A6, A7;

          hence thesis by A4, Th25;

        end;

        thus for fg be Morphism of [:B, C:] holds (T . ( id ( dom fg))) = ( id ( dom (T . fg))) & (T . ( id ( cod fg))) = ( id ( cod (T . fg)))

        proof

          let fg be Morphism of [:B, C:];

          consider f be Morphism of B, g be Morphism of C such that

           A8: fg = [f, g] by DOMAIN_1: 1;

          set b = ( dom f), c = ( dom g);

          set g9 = ( id c), f9 = ( id b);

          

           A9: ( Hom (( dom ((M . b) . g)),( dom ((M . b) . g)))) <> {} ;

          ( id ( dom ((L . ( cod g)) . f))) = ((L . ( cod g)) . ( id ( dom f))) by CAT_1: 63

          .= ((M . ( dom f)) . ( id ( cod g))) by A1

          .= ( id ( cod ((M . ( dom f)) . g))) by CAT_1: 63;

          then

           A10: ( dom ((L . ( cod g)) . f)) = ( cod ((M . ( dom f)) . g)) by CAT_1: 59;

          

          thus (T . ( id ( dom fg))) = (S . ( id [b, c])) by A8, Th22

          .= (S . (( id b),( id c))) by Th25

          .= (((L . ( cod g9)) . f9) (*) ((M . ( dom f9)) . g9)) by A3

          .= (((L . c) . f9) (*) ((M . ( dom f9)) . g9))

          .= (((L . c) . f9) (*) ((M . b) . g9))

          .= (((M . b) . g9) (*) ((M . b) . g9)) by A1

          .= (( id ( dom ((M . b) . g))) (*) ((M . b) . g9)) by CAT_1: 63

          .= (( id ( dom ((M . b) . g))) (*) ( id ( dom ((M . b) . g)))) by CAT_1: 63

          .= (( id ( dom ((M . b) . g))) * ( id ( dom ((M . b) . g)))) by A9, CAT_1:def 13

          .= ( id ( dom (((L . ( cod g)) . f) (*) ((M . ( dom f)) . g)))) by A10, CAT_1: 17

          .= ( id ( dom (S . (f,g)))) by A3

          .= ( id ( dom (T . fg))) by A8;

          set b = ( cod f), c = ( cod g);

          set g9 = ( id c), f9 = ( id b);

          

           A11: ( Hom (( cod ((L . c) . f)),( cod ((L . c) . f)))) <> {} ;

          

          thus (T . ( id ( cod fg))) = (S . ( id [b, c])) by A8, Th22

          .= (S . (( id b),( id c))) by Th25

          .= (((L . ( cod g9)) . f9) (*) ((M . ( dom f9)) . g9)) by A3

          .= (((L . c) . f9) (*) ((M . ( dom f9)) . g9))

          .= (((L . c) . f9) (*) ((M . ( cod f)) . g9))

          .= (((L . c) . f9) (*) ((L . c) . f9)) by A1

          .= (( id ( cod ((L . c) . f))) (*) ((L . c) . f9)) by CAT_1: 63

          .= (( id ( cod ((L . c) . f))) (*) ( id ( cod ((L . c) . f)))) by CAT_1: 63

          .= (( id ( cod ((L . c) . f))) * ( id ( cod ((L . c) . f)))) by A11, CAT_1:def 13

          .= ( id ( cod (((L . ( cod g)) . f) (*) ((M . ( dom f)) . g)))) by A10, CAT_1: 17

          .= ( id ( cod (S . (f,g)))) by A3

          .= ( id ( cod (T . fg))) by A8;

        end;

        let fg1,fg2 be Morphism of [:B, C:] such that

         A12: ( dom fg2) = ( cod fg1);

        consider f1 be Morphism of B, g1 be Morphism of C such that

         A13: fg1 = [f1, g1] by DOMAIN_1: 1;

        consider f2 be Morphism of B, g2 be Morphism of C such that

         A14: fg2 = [f2, g2] by DOMAIN_1: 1;

        

         A15: [( cod f1), ( cod g1)] = ( cod fg1) by A13, Th22;

        set L1 = (L . ( cod g1)), L2 = (L . ( cod g2)), M1 = (M . ( dom f1)), M2 = (M . ( dom f2));

        

         A16: [( dom f2), ( dom g2)] = ( dom fg2) by A14, Th22;

        then

         A17: ( dom f2) = ( cod f1) by A12, A15, XTUPLE_0: 1;

        then

         A18: ( dom (L2 . f2)) = ( cod (L2 . f1)) by CAT_1: 64;

        ( id ( dom (L1 . f1))) = (L1 . ( id ( dom f1))) by CAT_1: 63

        .= (M1 . ( id ( cod g1))) by A1

        .= ( id ( cod (M1 . g1))) by CAT_1: 63;

        then

         A19: ( dom (L1 . f1)) = ( cod (M1 . g1)) by CAT_1: 59;

        then

         A20: ( cod ((L1 . f1) (*) (M1 . g1))) = ( cod (L1 . f1)) by CAT_1: 17;

        

         A21: ( dom g2) = ( cod g1) by A12, A16, A15, XTUPLE_0: 1;

        then

         A22: ( dom (M1 . g2)) = ( cod (M1 . g1)) by CAT_1: 64;

        then

         A23: ( cod ((M1 . g2) (*) (M1 . g1))) = ( cod (M1 . g2)) by CAT_1: 17;

        ( id ( dom (M2 . g2))) = (M2 . ( id ( dom g2))) by CAT_1: 63

        .= (L1 . ( id ( cod f1))) by A1, A17, A21

        .= ( id ( cod (L1 . f1))) by CAT_1: 63;

        then

         A24: ( dom (M2 . g2)) = ( cod (L1 . f1)) by CAT_1: 59;

        ( id ( dom (L2 . f2))) = (L2 . ( id ( dom f2))) by CAT_1: 63

        .= (M2 . ( id ( cod g2))) by A1

        .= ( id ( cod (M2 . g2))) by CAT_1: 63;

        then

         A25: ( dom (L2 . f2)) = ( cod (M2 . g2)) by CAT_1: 59;

        set f = (f2 (*) f1), g = (g2 (*) g1);

        ( id ( dom (L2 . f1))) = (L2 . ( id ( dom f1))) by CAT_1: 63

        .= (M1 . ( id ( cod g2))) by A1

        .= ( id ( cod (M1 . g2))) by CAT_1: 63;

        then

         A26: ( dom (L2 . f1)) = ( cod (M1 . g2)) by CAT_1: 59;

        

        thus (T . (fg2 (*) fg1)) = (S . (f,g)) by A12, A13, A14, Th24

        .= (((L . ( cod g)) . f) (*) ((M . ( dom f)) . g)) by A3

        .= (((L . ( cod g2)) . f) (*) ((M . ( dom f)) . g)) by A21, CAT_1: 17

        .= (((L . ( cod g2)) . f) (*) ((M . ( dom f1)) . g)) by A17, CAT_1: 17

        .= (((L2 . f2) (*) (L2 . f1)) (*) (M1 . g)) by A17, CAT_1: 64

        .= (((L2 . f2) (*) (L2 . f1)) (*) ((M1 . g2) (*) (M1 . g1))) by A21, CAT_1: 64

        .= ((L2 . f2) (*) ((L2 . f1) (*) ((M1 . g2) (*) (M1 . g1)))) by A18, A23, A26, CAT_1: 18

        .= ((L2 . f2) (*) (((L2 . f1) (*) (M1 . g2)) (*) (M1 . g1))) by A22, A26, CAT_1: 18

        .= ((L2 . f2) (*) (((M2 . g2) (*) (L1 . f1)) (*) (M1 . g1))) by A2, A17, A21

        .= ((L2 . f2) (*) ((M2 . g2) (*) ((L1 . f1) (*) (M1 . g1)))) by A19, A24, CAT_1: 18

        .= (((L2 . f2) (*) (M2 . g2)) (*) ((L1 . f1) (*) (M1 . g1))) by A24, A25, A20, CAT_1: 18

        .= (((L2 . f2) (*) (M2 . g2)) (*) (S . (f1,g1))) by A3

        .= ((S . (f2,g2)) (*) (T . fg1)) by A3, A13

        .= ((T . fg2) (*) (T . fg1)) by A14;

      end;

      then

      reconsider T as Functor of [:B, C:], D by CAT_1: 61;

      take T;

      thus thesis by A3;

    end;

    theorem :: CAT_2:41

    for L be Function of the carrier of C, ( Funct (B,D)), M be Function of the carrier of B, ( Funct (C,D)) st ex S be Functor of [:B, C:], D st for c be Object of C, b be Object of B holds (S -? c) = (L . c) & (S ?- b) = (M . b) holds for f be Morphism of B holds for g be Morphism of C holds (((M . ( cod f)) . g) (*) ((L . ( dom g)) . f)) = (((L . ( cod g)) . f) (*) ((M . ( dom f)) . g))

    proof

      let L be Function of the carrier of C, ( Funct (B,D)), M be Function of the carrier of B, ( Funct (C,D));

      given S be Functor of [:B, C:], D such that

       A1: for c be Object of C, b be Object of B holds (S -? c) = (L . c) & (S ?- b) = (M . b);

      let f be Morphism of B;

      let g be Morphism of C;

      ( dom ( id ( cod f))) = ( cod f);

      then

       A2: ( dom [( id ( cod f)), g]) = [( cod f), ( dom g)] by Th22;

      ( cod ( id ( dom g))) = ( dom g);

      then

       A3: ( cod [f, ( id ( dom g))]) = [( cod f), ( dom g)] by Th22;

      ( cod ( id ( dom f))) = ( dom f);

      then

       A4: ( cod [( id ( dom f)), g]) = [( dom f), ( cod g)] by Th22;

      ( dom ( id ( cod g))) = ( cod g);

      then

       A5: ( dom [f, ( id ( cod g))]) = [( dom f), ( cod g)] by Th22;

      

      thus (((M . ( cod f)) . g) (*) ((L . ( dom g)) . f)) = (((S ?- ( cod f)) . g) (*) ((L . ( dom g)) . f)) by A1

      .= (((S ?- ( cod f)) . g) (*) ((S -? ( dom g)) . f)) by A1

      .= ((S . (( id ( cod f)),g)) (*) ((S -? ( dom g)) . f)) by FUNCT_5: 69

      .= ((S . (( id ( cod f)),g)) (*) (S . (f,( id ( dom g))))) by FUNCT_5: 70

      .= (S . ( [( id ( cod f)), g] (*) [f, ( id ( dom g))])) by A2, A3, CAT_1: 64

      .= (S . [(( id ( cod f)) (*) f), (g (*) ( id ( dom g)))]) by A2, A3, Th24

      .= (S . [f, (g (*) ( id ( dom g)))]) by CAT_1: 21

      .= (S . [f, g]) by CAT_1: 22

      .= (S . [(f (*) ( id ( dom f))), g]) by CAT_1: 22

      .= (S . [(f (*) ( id ( dom f))), (( id ( cod g)) (*) g)]) by CAT_1: 21

      .= (S . ( [f, ( id ( cod g))] (*) [( id ( dom f)), g])) by A5, A4, Th24

      .= ((S . (f,( id ( cod g)))) (*) (S . [( id ( dom f)), g])) by A5, A4, CAT_1: 64

      .= (((S -? ( cod g)) . f) (*) (S . (( id ( dom f)),g))) by FUNCT_5: 70

      .= (((S -? ( cod g)) . f) (*) ((S ?- ( dom f)) . g)) by FUNCT_5: 69

      .= (((L . ( cod g)) . f) (*) ((S ?- ( dom f)) . g)) by A1

      .= (((L . ( cod g)) . f) (*) ((M . ( dom f)) . g)) by A1;

    end;

    definition

      let C, D;

      :: CAT_2:def10

      func pr1 (C,D) -> Functor of [:C, D:], C equals ( pr1 (the carrier' of C,the carrier' of D));

      coherence

      proof

        reconsider T = ( pr1 (the carrier' of C,the carrier' of D)) as Function of the carrier' of [:C, D:], the carrier' of C;

        now

          thus for cd be Object of [:C, D:] holds ex c be Object of C st (T . ( id cd)) = ( id c)

          proof

            let cd be Object of [:C, D:];

            consider c be Object of C, d be Object of D such that

             A1: cd = [c, d] by DOMAIN_1: 1;

            

             A2: (T . (( id c),( id d))) = ( id c) by FUNCT_3:def 4;

            ( id cd) = [( id c), ( id d)] by A1, Th25;

            hence thesis by A2;

          end;

          thus for fg be Morphism of [:C, D:] holds (T . ( id ( dom fg))) = ( id ( dom (T . fg))) & (T . ( id ( cod fg))) = ( id ( cod (T . fg)))

          proof

            let fg be Morphism of [:C, D:];

            consider f be Morphism of C, g be Morphism of D such that

             A3: fg = [f, g] by DOMAIN_1: 1;

            (T . (f,g)) = (T . fg) by A3;

            then

             A4: (T . fg) = f by FUNCT_3:def 4;

            ( dom [f, g]) = [( dom f), ( dom g)] by Th22;

            

            hence (T . ( id ( dom fg))) = (T . (( id ( dom f)),( id ( dom g)))) by A3, Th25

            .= ( id ( dom (T . fg))) by A4, FUNCT_3:def 4;

            ( cod [f, g]) = [( cod f), ( cod g)] by Th22;

            

            hence (T . ( id ( cod fg))) = (T . (( id ( cod f)),( id ( cod g)))) by A3, Th25

            .= ( id ( cod (T . fg))) by A4, FUNCT_3:def 4;

          end;

          let fg,fg9 be Morphism of [:C, D:] such that

           A5: ( dom fg9) = ( cod fg);

          consider f be Morphism of C, g be Morphism of D such that

           A6: fg = [f, g] by DOMAIN_1: 1;

          (T . (f,g)) = (T . fg) by A6;

          then

           A7: (T . fg) = f by FUNCT_3:def 4;

          consider f9 be Morphism of C, g9 be Morphism of D such that

           A8: fg9 = [f9, g9] by DOMAIN_1: 1;

          (T . (f9,g9)) = (T . fg9) by A8;

          then

           A9: (T . fg9) = f9 by FUNCT_3:def 4;

          ( dom [f9, g9]) = [( dom f9), ( dom g9)] & ( cod [f, g]) = [( cod f), ( cod g)] by Th22;

          then ( dom f9) = ( cod f) & ( dom g9) = ( cod g) by A5, A6, A8, XTUPLE_0: 1;

          

          hence (T . (fg9 (*) fg)) = (T . ((f9 (*) f),(g9 (*) g))) by A6, A8, Th23

          .= ((T . fg9) (*) (T . fg)) by A9, A7, FUNCT_3:def 4;

        end;

        hence thesis by CAT_1: 61;

      end;

      :: CAT_2:def11

      func pr2 (C,D) -> Functor of [:C, D:], D equals ( pr2 (the carrier' of C,the carrier' of D));

      coherence

      proof

        reconsider T = ( pr2 (the carrier' of C,the carrier' of D)) as Function of the carrier' of [:C, D:], the carrier' of D;

        now

          thus for cd be Object of [:C, D:] holds ex d be Object of D st (T . ( id cd)) = ( id d)

          proof

            let cd be Object of [:C, D:];

            consider c be Object of C, d be Object of D such that

             A10: cd = [c, d] by DOMAIN_1: 1;

            

             A11: (T . (( id c),( id d))) = ( id d) by FUNCT_3:def 5;

            ( id cd) = [( id c), ( id d)] by A10, Th25;

            hence thesis by A11;

          end;

          thus for fg be Morphism of [:C, D:] holds (T . ( id ( dom fg))) = ( id ( dom (T . fg))) & (T . ( id ( cod fg))) = ( id ( cod (T . fg)))

          proof

            let fg be Morphism of [:C, D:];

            consider f be Morphism of C, g be Morphism of D such that

             A12: fg = [f, g] by DOMAIN_1: 1;

            (T . (f,g)) = (T . fg) by A12;

            then

             A13: (T . fg) = g by FUNCT_3:def 5;

            ( dom [f, g]) = [( dom f), ( dom g)] by Th22;

            

            hence (T . ( id ( dom fg))) = (T . (( id ( dom f)),( id ( dom g)))) by A12, Th25

            .= ( id ( dom (T . fg))) by A13, FUNCT_3:def 5;

            ( cod [f, g]) = [( cod f), ( cod g)] by Th22;

            

            hence (T . ( id ( cod fg))) = (T . (( id ( cod f)),( id ( cod g)))) by A12, Th25

            .= ( id ( cod (T . fg))) by A13, FUNCT_3:def 5;

          end;

          let fg,fg9 be Morphism of [:C, D:] such that

           A14: ( dom fg9) = ( cod fg);

          consider f be Morphism of C, g be Morphism of D such that

           A15: fg = [f, g] by DOMAIN_1: 1;

          (T . (f,g)) = (T . fg) by A15;

          then

           A16: (T . fg) = g by FUNCT_3:def 5;

          consider f9 be Morphism of C, g9 be Morphism of D such that

           A17: fg9 = [f9, g9] by DOMAIN_1: 1;

          (T . (f9,g9)) = (T . fg9) by A17;

          then

           A18: (T . fg9) = g9 by FUNCT_3:def 5;

          ( dom [f9, g9]) = [( dom f9), ( dom g9)] & ( cod [f, g]) = [( cod f), ( cod g)] by Th22;

          then ( dom f9) = ( cod f) & ( dom g9) = ( cod g) by A14, A15, A17, XTUPLE_0: 1;

          

          hence (T . (fg9 (*) fg)) = (T . ((f9 (*) f),(g9 (*) g))) by A15, A17, Th23

          .= ((T . fg9) (*) (T . fg)) by A18, A16, FUNCT_3:def 5;

        end;

        hence thesis by CAT_1: 61;

      end;

    end

    ::$Canceled

    theorem :: CAT_2:44

    for c be Object of C, d be Object of D holds (( Obj ( pr1 (C,D))) . (c,d)) = c

    proof

      let c be Object of C, d be Object of D;

      ( id [c, d]) = [( id c), ( id d)] & (( pr1 (C,D)) . (( id c),( id d))) = ( id c) by Th25, FUNCT_3:def 4;

      hence thesis by CAT_1: 67;

    end;

    theorem :: CAT_2:45

    for c be Object of C, d be Object of D holds (( Obj ( pr2 (C,D))) . (c,d)) = d

    proof

      let c be Object of C, d be Object of D;

      ( id [c, d]) = [( id c), ( id d)] & (( pr2 (C,D)) . (( id c),( id d))) = ( id d) by Th25, FUNCT_3:def 5;

      hence thesis by CAT_1: 67;

    end;

    definition

      let C, D, D9;

      let T be Functor of C, D, T9 be Functor of C, D9;

      :: original: <:

      redefine

      func <:T,T9:> -> Functor of C, [:D, D9:] ;

      coherence

      proof

        reconsider S = <:T, T9:> as Function of the carrier' of C, the carrier' of [:D, D9:];

        now

          thus for c be Object of C holds ex dd9 be Object of [:D, D9:] st (S . ( id c)) = ( id dd9)

          proof

            let c be Object of C;

            set d = (( Obj T) . c), d9 = (( Obj T9) . c);

            take dd9 = [d, d9];

            

            thus (S . ( id c)) = [(T . ( id c)), (T9 . ( id c))] by FUNCT_3: 59

            .= [( id d), (T9 . ( id c))] by CAT_1: 68

            .= [( id d), ( id d9)] by CAT_1: 68

            .= ( id dd9) by Th25;

          end;

          thus for f be Morphism of C holds (S . ( id ( dom f))) = ( id ( dom (S . f))) & (S . ( id ( cod f))) = ( id ( cod (S . f)))

          proof

            let f be Morphism of C;

            (T . ( id ( dom f))) = ( id ( dom (T . f))) & (T9 . ( id ( dom f))) = ( id ( dom (T9 . f))) by CAT_1: 63;

            

            hence (S . ( id ( dom f))) = [( id ( dom (T . f))), ( id ( dom (T9 . f)))] by FUNCT_3: 59

            .= ( id [( dom (T . f)), ( dom (T9 . f))]) by Th25

            .= ( id ( dom [(T . f), (T9 . f)])) by Th22

            .= ( id ( dom (S . f))) by FUNCT_3: 59;

            (T . ( id ( cod f))) = ( id ( cod (T . f))) & (T9 . ( id ( cod f))) = ( id ( cod (T9 . f))) by CAT_1: 63;

            

            hence (S . ( id ( cod f))) = [( id ( cod (T . f))), ( id ( cod (T9 . f)))] by FUNCT_3: 59

            .= ( id [( cod (T . f)), ( cod (T9 . f))]) by Th25

            .= ( id ( cod [(T . f), (T9 . f)])) by Th22

            .= ( id ( cod (S . f))) by FUNCT_3: 59;

          end;

          let f,g be Morphism of C;

          assume

           A1: ( dom g) = ( cod f);

          then

           A2: ( dom (T . g)) = ( cod (T . f)) & ( dom (T9 . g)) = ( cod (T9 . f)) by CAT_1: 64;

          (T . (g (*) f)) = ((T . g) (*) (T . f)) & (T9 . (g (*) f)) = ((T9 . g) (*) (T9 . f)) by A1, CAT_1: 64;

          

          hence (S . (g (*) f)) = [((T . g) (*) (T . f)), ((T9 . g) (*) (T9 . f))] by FUNCT_3: 59

          .= ( [(T . g), (T9 . g)] (*) [(T . f), (T9 . f)]) by A2, Th23

          .= ((S . g) (*) [(T . f), (T9 . f)]) by FUNCT_3: 59

          .= ((S . g) (*) (S . f)) by FUNCT_3: 59;

        end;

        hence thesis by CAT_1: 61;

      end;

    end

    ::$Canceled

    theorem :: CAT_2:47

    for T be Functor of C, D, T9 be Functor of C, D9, c be Object of C holds (( Obj <:T, T9:>) . c) = [(( Obj T) . c), (( Obj T9) . c)]

    proof

      let T be Functor of C, D, T9 be Functor of C, D9, c be Object of C;

      

       A1: (T . ( id c)) = ( id (( Obj T) . c)) & (T9 . ( id c)) = ( id (( Obj T9) . c)) by CAT_1: 68;

      ( <:T, T9:> . ( id c)) = [(T . ( id c)), (T9 . ( id c))] & [( id (( Obj T) . c)), ( id (( Obj T9) . c))] = ( id [(( Obj T) . c), (( Obj T9) . c)]) by Th25, FUNCT_3: 59;

      hence thesis by A1, CAT_1: 67;

    end;

    theorem :: CAT_2:48

    

     Th39: for T be Functor of C, D, T9 be Functor of C9, D9 holds [:T, T9:] = <:(T * ( pr1 (C,C9))), (T9 * ( pr2 (C,C9))):>

    proof

      let T be Functor of C, D, T9 be Functor of C9, D9;

      ( dom T) = the carrier' of C & ( dom T9) = the carrier' of C9 by FUNCT_2:def 1;

      hence thesis by FUNCT_3: 66;

    end;

    definition

      let C, C9, D, D9;

      let T be Functor of C, D, T9 be Functor of C9, D9;

      :: original: [:

      redefine

      func [:T,T9:] -> Functor of [:C, C9:], [:D, D9:] ;

      coherence

      proof

         [:T, T9:] = <:(T * ( pr1 (C,C9))), (T9 * ( pr2 (C,C9))):> by Th39;

        hence thesis;

      end;

    end

    ::$Canceled

    theorem :: CAT_2:50

    for T be Functor of C, D, T9 be Functor of C9, D9, c be Object of C, c9 be Object of C9 holds (( Obj [:T, T9:]) . (c,c9)) = [(( Obj T) . c), (( Obj T9) . c9)]

    proof

      let T be Functor of C, D, T9 be Functor of C9, D9;

      let c be Object of C, c9 be Object of C9;

      

       A1: (T . ( id c)) = ( id (( Obj T) . c)) & (T9 . ( id c9)) = ( id (( Obj T9) . c9)) by CAT_1: 68;

      

       A2: [( id (( Obj T) . c)), ( id (( Obj T9) . c9))] = ( id [(( Obj T) . c), (( Obj T9) . c9)]) by Th25;

      ( [:T, T9:] . (( id c),( id c9))) = [(T . ( id c)), (T9 . ( id c9))] & [( id c), ( id c9)] = ( id [c, c9]) by Th25, FUNCT_3: 75;

      hence thesis by A1, A2, CAT_1: 67;

    end;