:: Subcategories and Products of Categories
::  by Czes{\l}aw Byli\'nski
::
:: Received May 31, 1990
:: Copyright (c) 1990-2018 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, SUBSET_1, FUNCT_2, FUNCT_1, ZFMISC_1, FUNCT_5, RELAT_1,
      TARSKI, CAT_1, FUNCOP_1, STRUCT_0, GRAPH_1, FUNCT_3, REALSET1, PARTFUN1,
      FUNCT_4, MCART_1, CAT_2, MONOID_0, RELAT_2, BINOP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1,
      FUNCT_2, BINOP_1, PARTFUN1, FUNCT_3, FUNCT_4, FUNCT_5, REALSET1,
      FUNCOP_1, STRUCT_0, GRAPH_1, CAT_1;
 constructors PARTFUN1, BINOP_1, FUNCT_3, FUNCT_4, FUNCT_5, REALSET1, CAT_1,
      FUNCOP_1, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, CAT_1, STRUCT_0,
      RELAT_1, XTUPLE_0;
 requirements SUBSET, BOOLE;
 definitions TARSKI, CAT_1;
 equalities CAT_1, REALSET1, FUNCOP_1, BINOP_1, GRAPH_1;
 expansions CAT_1;
 theorems TARSKI, ZFMISC_1, MCART_1, DOMAIN_1, FUNCT_1, FUNCT_2, FUNCT_3,
      FUNCT_4, FUNCT_5, PARTFUN1, FUNCOP_1, CAT_1, GRFUNC_1, RELAT_1, RELSET_1,
      XBOOLE_0, XBOOLE_1, XTUPLE_0;
 schemes XBOOLE_0, BINOP_1;

begin

::$CT 4

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

:: Auxiliary theorems on Functors

definition
  let B,C;
  let c be Object of C;
  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 being Object of B ex d being Object of C st T.(id b) = id d
      by FUNCOP_1:7;
      thus for f being 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
  for c being Object of C, b being 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;
  func Funct(C,D) -> set means
  :Def2:
  for x being 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 being set such that
A1: for x being 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 being set holds x in F1 iff x is Functor of C,D and
A4: for x being 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;
  mode FUNCTOR-DOMAIN of C,D -> non empty set means
    :Def3:
    for x being 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;
  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;
  redefine func T.x -> Element of F;
  coherence
  proof
    thus T.x is Element of F;
  end;
end;

definition
  let C,D;
  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;

::   Subcategory

definition
  let C;
  mode Subcategory of C -> Category means
    :Def4:
    the carrier of it c= the carrier of C &
     (for a,b being Object of it, a9,b9 being 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 being Object of it, a9 being 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 being Object of E, a9,b9 being 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 Th2:
  for e being 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 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 Th4:
  for f being 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 Th5:
  for f being (Morphism of E), f9 being 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
  for a,b being Object of E, a9,b9 being Object of C,f being 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 Th7:
  for f,g being (Morphism of E), f9,g9 being 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,16;
  hence thesis by A1,A3,A4,GRFUNC_1:2;
end;

theorem Th8:
  C is Subcategory of C
proof
  thus the carrier of C c= the carrier of C;
  thus thesis;
end;

theorem 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 being Object of E ex c being 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 being 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;
  func incl(E) -> Functor of E,C equals
  id E;
  coherence by Th9;
end;

theorem Th10:
  for a being 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
  for a being Object of E holds (incl E).a = a by Th10;

theorem
  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 Th13:
  incl E is full iff for a,b being Object of E, a9,b9 being 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 being Object of E, a9,b9 being Object of C st
  a = a9 & b = b9 holds Hom(a,b) = Hom(a9,b9)
  proof
    assume
A1: for a,b being Object of E st Hom(T.a,T.b) <> {} for g being
Morphism of T.a,T.b holds Hom(a,b) <> {} & ex f being 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 being 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 being Object of E, a9,b9 being 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;
  attr C is full means
:Def6:  for c1,c2 being Object of C, d1,d2 being 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 being Object of D;
   assume c1 = d1 & c2 = d2;
   hence Hom(c1,c2) = Hom(d1,d2);
  end;
end;

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

theorem Th15:
  for O being non empty Subset of the carrier of C holds union{Hom
  (a,b) where a is Object of C,b is 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 is Object of C, b is 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 being set such that
A2: x in X and
A3: X in H by TARSKI:def 4;
    ex a,b being 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 being set st f in M;
  end;
  hence thesis by A1;
end;

theorem Th16:
  for O being non empty Subset of the carrier of C, M being non
empty set st M = union{Hom(a,b) where a is Object of C,b is 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 is Object of C, b is 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 being set such that
A4: f in X and
A5: X in H by A2,TARSKI:def 4;
    ex a,b being 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 being 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 being 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 being 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 being 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 being Function of M,O, p being PartFunc of [:
  M,M:],M;
  cluster CatStr(#O,M,d,c,p#) -> non void non empty;
  coherence;
end;

Lm1:
  for O being non empty Subset of the carrier of C, M being non empty
set, d,c being Function of M,O, p being PartFunc of [:M,M:],M, i being Function
of O,M st M = union{Hom(a,b) where a is Object of C,b is 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 is Object of C, b is 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 being set such that
A6: f in X and
A7: X in H by A1,TARSKI:def 4;
    ex a,b being 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 being 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 being 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 being 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 being 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 being 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 being non empty Subset of the carrier of C, M being non empty
set, d,c being Function of M,O, p being PartFunc of [:M,M:],M, i being Function
of O,M st M = union{Hom(a,b) where a is Object of C,b is 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 is Object of C, b is 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 being set such that
A6: f in X and
A7: X in H by A1,TARSKI:def 4;
    ex a,b being 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 being Object of B, a9,b9 being 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 being 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 being Object of B holds
        (Hom(a,b) <> {} implies
       for f being Morphism of a,b holds f(*)ii = f)
      & (Hom(b,a) <> {} implies
       for f being 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 being 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 being Object of B, a9,b9 being 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
  for O being non empty Subset of the carrier of C, M being non empty
set, d,c being Function of M,O, p being PartFunc of [:M,M:],M, i being Function
of O,M st M = union{Hom(a,b) where a is Object of C,b is 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 is Object of C, b is 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 being set such that
A6: f in X and
A7: X in H by A1,TARSKI:def 4;
    ex a,b being 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 being Object of B, a9,b9 being 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
  for O being non empty Subset of the carrier of C, M being non empty
  set , d,c being Function of M,O, p being 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 is Object of C,b is 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 is Object of C, b is 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 being 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 being set such that
A3: x in X and
A4: X in H by TARSKI:def 4;
    consider a9,b9 being 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 being 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 being 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,16
      .= p9.x by A9,A13,A14,FUNCT_1:47;
  end;
  hence p = (the Comp of C)||M by FUNCT_1:2;
end;

:: Product of Categories

definition
  let C,D;
  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 being 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 being 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 being Morphism of B
      holds [g,f] in dom(the Comp of B) iff dom g = cod f by A6;
A11: for f,g being 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 being 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 being 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
  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;
  redefine func [c,d] -> Object of [:C,D:];
  coherence
    proof
     thus [c,d] is Object of [:C,D:];
    end;
end;

::$CT

theorem
  for cd being Object of [:C,D:] ex c being Object of C, d being 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;
  redefine func [f,g] -> Morphism of [:C,D:];
  coherence
   proof
    thus [f,g] is Morphism of [:C,D:];
   end;
end;

::$CT

theorem
  for fg being Morphism of [:C,D:] ex f being (Morphism of C), g being
  Morphism of D st fg = [f,g] by DOMAIN_1:1;

theorem Th22:
  for f being Morphism of C for g being 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 Th23:
  for f,f9 being Morphism of C for g,g9 being 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 Th24:
  for f,f9 being Morphism of C for g,g9 being 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 Th25:
  for c being Object of C, d being Object of D holds id [c,d] = [id c,id d]
proof
  let c being Object of C;
  let d being 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 being Object of [:C,D:] holds
     (Hom([c,d],b) <> {} implies
       for f being Morphism of [c,d],b holds f(*)[id c,id d] = f)
   & (Hom(b,[c,d]) <> {} implies
     for f being 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 being 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 being (Morphism of C), fd being 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 being (Morphism of C), fd being 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
  for c,c9 being Object of C, d,d9 being 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 being 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 being 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
  for c,c9 being Object of C, f being Morphism of c,c9, d,d9 being
  Object of D, g being 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;

:: Bifunctors

definition
  let C,C9,D;
  let S being Functor of [:C,C9:],D;
  let m be Morphism of C;
  let m9 be Morphism of C9;
  redefine func S.(m,m9) -> Morphism of D;
  coherence
  proof
    S.(m,m9) = S.[m,m9];
    hence thesis;
  end;
end;

theorem Th28:
  for S being Functor of [:C,C9:],D, c being 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 being Object of C9 ex d being Object of D st T.(id c9) = id d
    proof
      let c9 be Object of C9;
      consider d being 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 being 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 Th29:
  for S being Functor of [:C,C9:],D, c9 being 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 being Object of C ex d being Object of D st T.(id c) = id d
    proof
      let c be Object of C;
      consider d being 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 being 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;

:: Partial Functors

definition
  let C,C9,D;
  let S be Functor of [:C,C9:],D, c be Object of C;
  func S?-c -> Functor of C9,D equals
  (curry S).(id c);
  coherence by Th28;
end;

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

theorem
  for S being Functor of [:C,C9:],D, c being Object of C, c9 being
  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;
  func S-?c9 -> Functor of C,D equals
  (curry' S).(id c9);
  coherence by Th29;
end;

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

theorem
  for S being Functor of [:C,C9:],D, c being Object of C, c9 being
  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
  for L being Function of the carrier of C,Funct(B,D), M being Function
of the carrier of B,Funct(C,D) st ( for c being Object of C,b being Object of B
  holds (M.b).(id c) = (L.c).(id b) ) & ( for f being Morphism of B for g being
Morphism of C
  holds ((M.(cod f)).g)(*)((L.(dom g)).f) = ((L.(cod g)).f)(*)((M.(dom
  f)).g) ) ex S being Functor of [:B,C:],D st for f being Morphism of B for g
  being 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 being Object of C, b being Object of B holds (M.b).(id c) = (L
  .c).(id b) and
A2: for f being Morphism of B for g being 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 being Function of [:Mor(B),Mor(C):],Mor(D) such that
A3: for f being Morphism of B for g being Morphism of C holds S.(f,g) =
  F(f,g) from BINOP_1:sch 4;
  reconsider T = S as Function of Mor([:B,C:]),Mor(D);
  now
    thus for bc being Object of [:B,C:] ex d being Object of D st T.(id bc) =
    id d
    proof
      let bc be Object of [:B,C:];
      consider b being Object of B, c being Object of C such that
A4:   bc = [b,c] by DOMAIN_1:1;
      consider d being 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 being 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 being (Morphism of B), g being 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 being (Morphism of B), g1 being Morphism of C such that
A13: fg1 = [f1,g1] by DOMAIN_1:1;
    consider f2 being (Morphism of B), g2 being 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
  for L being Function of the carrier of C,Funct(B,D),
      M being Function of the carrier of B,Funct(C,D)
   st ex S being Functor of [:B,C:],D st
    for c being Object of C,b being Object of B
     holds S-?c = L.c & S?-b = M.b
  for f being Morphism of B for g being 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 being Object of C, b being 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;
  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 being Object of [:C,D:] ex c being Object of C st T.(id cd) =
    id c
    proof
      let cd be Object of [:C,D:];
      consider c being Object of C,d being 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 being 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 being (Morphism of C), g being 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 being (Morphism of C), g being 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 being (Morphism of C), g9 being 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;
  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 being Object of [:C,D:] ex d being Object of D st T.(id cd) =
    id d
    proof
      let cd be Object of [:C,D:];
      consider c being Object of C,d being 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 being 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 being (Morphism of C), g being 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 being (Morphism of C), g being 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 being (Morphism of C), g9 being 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;

::$CT 2

theorem
  for c being Object of C, d being 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
  for c being Object of C, d being 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;
  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 being Object of C ex dd9 being 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 being 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;

::$CT

theorem
  for T being Functor of C,D, T9 being Functor of C,D9, c being 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 Th39:
  for T being Functor of C,D, T9 being 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;
  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;

::$CT

theorem
  for T being Functor of C,D, T9 being Functor of C9,D9, c being Object
of C, c9 being 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;