:: Category Ens
::  by Czes{\l}aw Byli\'nski
::
:: Received August 1, 1991
:: Copyright (c) 1991-2012 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, TARSKI, FUNCT_1, RELAT_1, ZFMISC_1,
      MCART_1, GRAPH_1, PARTFUN1, CAT_1, STRUCT_0, QC_LANG1, CLASSES2,
      FUNCOP_1, FUNCT_4, CAT_2, OPPCAT_1, FUNCT_5, ARYTM_0, ENS_1, MONOID_0,
      RELAT_2, BINOP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1,
      XTUPLE_0, SUBSET_1, MCART_1, DOMAIN_1, RELAT_1,
      FUNCT_1, FUNCT_2, BINOP_1, PARTFUN1, FUNCT_4, CLASSES2,
      FUNCOP_1, FUNCT_5, STRUCT_0, GRAPH_1, CAT_1, CAT_2, OPPCAT_1;
 constructors PARTFUN1, DOMAIN_1, CLASSES2, CAT_2, OPPCAT_1, FUNCOP_1,
      RELSET_1, FUNCT_5, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, RELSET_1, STRUCT_0,
      PARTFUN1, RELAT_1, CAT_1, XTUPLE_0, OPPCAT_1, CAT_2;
 requirements SUBSET, BOOLE;
 definitions TARSKI, FUNCT_1, CAT_1, CAT_2, BINOP_1, RELAT_1, GRAPH_1,
      OPPCAT_1, XTUPLE_0;
 theorems TARSKI, ENUMSET1, ZFMISC_1, MCART_1, DOMAIN_1, FUNCT_1, FUNCT_2,
      PARTFUN1, FUNCOP_1, FUNCT_4, CLASSES2, CAT_1, CAT_2, OPPCAT_1, GRFUNC_1,
      RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, BINOP_1, FUNCT_5, XTUPLE_0;
 schemes FUNCT_2, BINOP_1, FUNCT_1;

begin :: Mappings

reserve V for non empty set,
  A,B,A9,B9 for Element of V;

definition
  let V;
  func Funcs(V) -> set equals
  union { Funcs(A,B): not contradiction };
  coherence;
end;

registration
  let V;
  cluster Funcs(V) -> functional non empty;
  coherence
  proof
    set F = { Funcs(A,B): not contradiction};
    set A = the Element of V;
    id A in Funcs(A,A) & Funcs(A,A) in F by FUNCT_2:9;
    then reconsider UF = union F as non empty set by TARSKI:def 4;
    now
      let f be set;
      assume f in UF;
      then consider C being set such that
A1:   f in C and
A2:   C in F by TARSKI:def 4;
      ex A,B st C = Funcs(A,B) by A2;
      hence f is Function by A1;
    end;
    hence thesis by FUNCT_1:def 13;
  end;
end;

theorem Th1:
  for f being set holds f in Funcs(V) iff ex A,B st (B={} implies A
  ={}) & f is Function of A,B
proof
  let f be set;
  set F = { Funcs(A,B): not contradiction};
  thus f in Funcs(V) implies ex A,B st (B={} implies A={}) & f is Function of
  A,B
  proof
    assume f in Funcs(V);
    then consider C being set such that
A1: f in C and
A2: C in F by TARSKI:def 4;
    consider A,B such that
A3: C = Funcs(A,B) by A2;
    take A,B;
    thus thesis by A1,A3,FUNCT_2:66;
  end;
  given A,B such that
A4: ( B={} implies A={})& f is Function of A,B;
A5: Funcs(A,B) in F;
  f in Funcs(A,B) by A4,FUNCT_2:8;
  hence thesis by A5,TARSKI:def 4;
end;

theorem
  Funcs(A,B) c= Funcs(V)
proof
  let x be set;
  assume
A1: x in Funcs(A,B);
  then
A2: x is Function of A,B by FUNCT_2:66;
  B={} implies A={} by A1;
  hence thesis by A2,Th1;
end;

theorem Th3:
  for W be non empty Subset of V holds Funcs W c= Funcs V
proof
  let W be non empty Subset of V;
  let f be set;
  assume f in Funcs W;
  then ex A,B being Element of W st(B={} implies A={}) & f is Function of A,B
  by Th1;
  hence thesis by Th1;
end;

reserve f,f9 for Element of Funcs(V);

definition
  let V;
  func Maps(V) -> set equals
  { [[A,B],f]: (B={} implies A={}) & f is Function
  of A,B};
  coherence;
end;

registration
  let V;
  cluster Maps(V) -> non empty;
  coherence
  proof
    set FV = { [[A,B],f]: (B={} implies A={}) & f is Function of A,B};
    set A = the Element of V;
    now
      set f = id A;
      take m = [[A,A],f];
A1:   A = {} implies A = {};
      f in Funcs(V) by Th1;
      hence m in FV by A1;
    end;
    hence thesis;
  end;
end;

reserve m,m1,m2,m3,m9 for Element of Maps V;

theorem Th4:
  ex f,A,B st m = [[A,B],f] & (B = {} implies A = {}) & f is Function of A,B
proof
  m in { [[A,B],f]: (B={} implies A={}) & f is Function of A,B};
  then ex A,B,f st m = [[A,B],f] & (B={} implies A={}) & f is Function of A,B;
  hence thesis;
end;

theorem Th5:
  for f being Function of A,B st B={} implies A={} holds [[A,B],f] in Maps V
proof
  let f be Function of A,B;
  assume
A1: B = {} implies A = {};
  then f in Funcs(V) by Th1;
  hence thesis by A1;
end;

theorem
  Maps V c= [:[:V,V:],Funcs V:]
proof
  let m be set;
  assume m in Maps V;
  then ex A,B,f st m = [[A,B],f] & (B={} implies A={}) & f is Function of A,B;
  hence thesis;
end;

theorem Th7:
  for W be non empty Subset of V holds Maps W c= Maps V
proof
  let W be non empty Subset of V;
  let x be set;
  assume x in Maps W;
  then consider A,B be Element of W, f be Element of Funcs(W) such that
A1: x = [[A,B],f] &( B = {} implies A = {}) & f is Function of A,B;
  Funcs W c= Funcs V & f in Funcs(W) by Th3;
  hence thesis by A1;
end;

Lm1: for x1,y1,x2,y2,x3,y3 being set st [[x1,x2],x3] = [[y1,y2],y3] holds x1 =
y1 & x2 = y2
proof
  let x1,y1,x2,y2,x3,y3 be set;
  assume [[x1,x2],x3] = [[y1,y2],y3];
  then [x1,x2] = [y1,y2] by XTUPLE_0:1;
  hence thesis by XTUPLE_0:1;
end;

registration
  let V be non empty set, m be Element of Maps V;
  cluster m`2 -> Function-like Relation-like;
  coherence
  proof
    ex f be Element of Funcs(V), A,B be Element of V st m = [[ A,B],f] &( B
    = {} implies A = {})& f is Function of A,B by Th4;
    hence thesis by MCART_1:7;
  end;
end;

definition
  let V,m;

  func dom m -> Element of V equals
  m`1`1;
  coherence
  proof
    consider f,A,B such that
A1: m = [[A,B],f] and
    B = {} implies A = {} and
    f is Function of A,B by Th4;
    [A,B] = m`1 by A1,MCART_1:7;
    hence thesis by MCART_1:7;
  end;
  func cod m -> Element of V equals
  m`1`2;
  coherence
  proof
    consider f,A,B such that
A2: m = [[A,B],f] and
    B = {} implies A = {} and
    f is Function of A,B by Th4;
    [A,B] = m`1 by A2,MCART_1:7;
    hence thesis by MCART_1:7;
  end;
end;

theorem Th8:
  m = [[dom m,cod m],m`2]
proof
 consider f,A,B such that
A1: m = [[A,B],f] &( B = {} implies A = {})& f is Function of A,B
  by Th4;
   m`1 = [A,B] by A1,MCART_1:7;
   then m`1 = [dom m,cod m] by MCART_1:8;
  hence thesis by A1,MCART_1:8;
end;

Lm2: m`2 = m9`2 & dom m = dom m9 & cod m = cod m9 implies m = m9
proof
  m = [[dom m,cod m],m`2] by Th8;
  hence thesis by Th8;
end;

theorem Th9:
  (cod m <> {} or dom m = {}) & m`2 is Function of dom m,cod m
proof
  consider f, A,B such that
A1: m = [[A,B],f] and
A2: ( B = {} implies A = {})& f is Function of A,B by Th4;
A3: m = [[dom m,cod m],m`2] by Th8;
  then f = m`2 & A = dom m by A1,Lm1,XTUPLE_0:1;
  hence thesis by A1,A2,A3,Lm1;
end;

Lm3: dom m`2 = dom m & rng m`2 c= cod m
proof
A1: m`2 is Function of dom m,cod m by Th9;
  cod m <> {} or dom m = {} by Th9;
  hence thesis by A1,FUNCT_2:def 1,RELAT_1:def 19;
end;

theorem Th10:
  for f being Function, A,B being set st [[A,B],f] in Maps(V)
  holds (B = {} implies A = {}) & f is Function of A,B
proof
  let f be Function, A,B be set;
  assume [[A,B],f] in Maps(V);
  then consider f9,A9,B9 such that
A1: [[A,B],f] = [[A9,B9],f9] and
A2: ( B9 = {} implies A9 = {})& f9 is Function of A9,B9 by Th4;
  f = f9 & A = A9 by A1,Lm1,XTUPLE_0:1;
  hence thesis by A1,A2,Lm1;
end;

definition
  let V,A;
  func id$ A -> Element of Maps V equals
  [[A,A],id A];
  coherence by Th5;
end;

theorem Th11:
  (id$ A)`2 = id A & dom id$ A = A & cod id$ A = A
proof
  [[dom id$ A,cod id$ A],(id$ A)`2] = [[A,A],id A] by Th8;
  hence thesis by Lm1,XTUPLE_0:1;
end;

definition
  let V,m1,m2;
  assume
A1: cod m1 = dom m2;
  func m2*m1 -> Element of Maps V equals
  :Def6:
  [[dom m1,cod m2],m2`2*m1`2];
  coherence
  proof
A2: cod m2 <> {} or dom m2 = {} by Th9;
A3: cod m1 <> {} or dom m1 = {} by Th9;
    m1`2 is Function of dom m1,cod m1 & m2`2 is Function of dom m2,cod m2
    by Th9;
    then m2`2*m1`2 is Function of dom m1,cod m2 by A1,A3,FUNCT_2:13;
    hence thesis by A1,A3,A2,Th5;
  end;
end;

theorem Th12:
  dom m2 = cod m1 implies (m2*m1)`2 = m2`2*m1`2 & dom(m2*m1) = dom
  m1 & cod(m2*m1) = cod m2
proof
  assume dom m2 = cod m1;
  then [[dom m1,cod m2],m2`2*m1`2] = m2*m1 by Def6
    .= [[dom(m2*m1),cod(m2*m1)],(m2*m1)`2] by Th8;
  hence thesis by Lm1,XTUPLE_0:1;
end;

theorem Th13:
  dom m2 = cod m1 & dom m3 = cod m2 implies m3*(m2*m1) = (m3*m2)* m1
proof
  assume that
A1: dom m2 = cod m1 and
A2: dom m3 = cod m2;
A3: cod(m2*m1) = cod m2 by A1,Th12;
  (m2*m1)`2 = m2`2*m1`2 by A1,Th12;
  then
A4: (m3*(m2*m1))`2 = m3`2*(m2`2*m1`2) by A2,A3,Th12;
A5: dom(m3*m2) = dom m2 by A2,Th12;
  then
A6: dom((m3*m2)*m1) = dom m1 by A1,Th12;
  dom(m2*m1) = dom m1 by A1,Th12;
  then
A7: dom(m3*(m2*m1)) = dom m1 by A2,A3,Th12;
  cod(m3*m2) = cod m3 by A2,Th12;
  then
A8: cod((m3*m2)*m1) = cod m3 by A1,A5,Th12;
  (m3*m2)`2 = m3`2*m2`2 by A2,Th12;
  then
A9: ((m3*m2)*m1)`2 = (m3`2*m2`2)*m1`2 by A1,A5,Th12;
  cod(m3*(m2*m1)) = cod m3 by A2,A3,Th12;
  hence thesis by A4,A7,A9,A6,A8,Lm2,RELAT_1:36;
end;

theorem Th14:
  m*(id$ dom m) = m & (id$ cod m)*m = m
proof
  set i1 = id$ dom m, i2 = id$ cod m;
A1: i1`2 = id dom m & dom i1 = dom m by Th11;
A2: m`2 is Function of dom m,cod m by Th9;
  then
A3: rng m`2 c= cod m by RELAT_1:def 19;
  cod m <> {} or dom m = {} by Th9;
  then
A4: dom m`2 = dom m by A2,FUNCT_2:def 1;
A5: cod i1 = dom m by Th11;
  then
A6: cod(m*i1) = cod m by Th12;
  (m*i1)`2 = m`2*i1`2 & dom(m*i1) = dom i1 by A5,Th12;
  hence m*i1 = m by A4,A1,A6,Lm2,RELAT_1:52;
A7: i2`2 = id cod m & cod i2 = cod m by Th11;
A8: dom i2 = cod m by Th11;
  then
A9: cod(i2*m) = cod i2 by Th12;
  (i2*m)`2 = i2`2*m`2 & dom(i2*m) = dom m by A8,Th12;
  hence thesis by A3,A7,A9,Lm2,RELAT_1:53;
end;

definition
  let V,A,B;
  func Maps(A,B) -> set equals
  { [[A,B],f] where f is Element of Funcs V: [[A,
  B],f] in Maps V };
  correctness;
end;

theorem Th15:
  for f being Function of A,B st B = {} implies A = {} holds [[A,B
  ],f] in Maps(A,B)
proof
  let f be Function of A,B;
  assume B = {} implies A = {};
  then f in Funcs(V) & [[A,B],f] in Maps(V) by Th1,Th5;
  hence thesis;
end;

theorem Th16:
  m in Maps(A,B) implies m = [[A,B],m`2]
proof
  assume m in Maps(A,B);
  then
A1: ex f being Element of Funcs(V) st m = [[A,B],f] & [[A,B],f] in Maps( V);
  m = [[dom m,cod m],m`2] by Th8;
  hence thesis by A1,XTUPLE_0:1;
end;

theorem Th17:
  Maps(A,B) c= Maps V
proof
  let z be set;
  assume z in Maps(A,B);
  then ex f being Element of Funcs(V) st z = [[A,B],f] & [[A,B],f] in Maps(V);
  hence thesis;
end;

Lm4: for f being Function st [[A,B],f] in Maps(A,B) holds (B = {} implies A =
{}) & f is Function of A,B
proof
A1: Maps(A,B) c= Maps V by Th17;
  let f be Function;
  assume [[A,B],f] in Maps(A,B);
  hence thesis by A1,Th10;
end;

theorem
  Maps V = union { Maps(A,B): not contradiction }
proof
  set M = { Maps(A,B): not contradiction };
  now
    let z be set;
    thus z in Maps V implies z in union M
    proof
      assume z in Maps V;
      then consider
      f being Element of Funcs(V),A,B being Element of V such that
A1:   z = [[A,B],f] &( B = {} implies A = {}) & f is Function of A,B by Th4;
A2:   Maps(A,B) in M;
      z in Maps(A,B) by A1,Th15;
      hence thesis by A2,TARSKI:def 4;
    end;
    assume z in union M;
    then consider C being set such that
A3: z in C and
A4: C in M by TARSKI:def 4;
    consider A,B such that
A5: C = Maps(A,B) by A4;
    ex f being Element of Funcs(V) st z = [[A,B],f] & [[A,B],f] in Maps(V
    ) by A3,A5;
    hence z in Maps(V);
  end;
  hence thesis by TARSKI:1;
end;

theorem Th19:
  m in Maps(A,B) iff dom m = A & cod m = B
proof
A1: m`2 is Function of dom m,cod m by Th9;
  thus m in Maps(A,B) implies dom m = A & cod m = B
  proof
    assume m in Maps(A,B);
    then
A2: m = [[A,B],m`2] by Th16;
    m = [[dom m,cod m],m`2] by Th8;
    hence thesis by A2,Lm1;
  end;
  cod m <> {} or dom m = {} by Th9;
  then [[dom m,cod m],m`2] in Maps(dom m,cod m) by A1,Th15;
  hence thesis by Th8;
end;

theorem Th20:
  m in Maps(A,B) implies m`2 in Funcs(A,B)
proof
  assume
A1: m in Maps(A,B);
  then
A2: m = [[A,B],m`2] by Th16;
  then
A3: m`2 is Function of A,B by A1,Lm4;
  B = {} implies A = {} by A1,A2,Lm4;
  hence thesis by A3,FUNCT_2:8;
end;

Lm5: for W being non empty Subset of V, A,B being Element of W, A9,B9 being
Element of V st A = A9 & B = B9 holds Maps(A,B) = Maps(A9,B9)
proof
  let W be non empty Subset of V;
  let A,B be Element of W, A9,B9 be Element of V such that
A1: A = A9 & B = B9;
  now
    let x be set;
    thus x in Maps(A,B) implies x in Maps(A9,B9)
    proof
A2:   Maps W c= Maps V by Th7;
      assume
A3:   x in Maps(A,B);
A4:   Maps(A,B) c= Maps W by Th17;
      then reconsider m = x as Element of Maps W by A3;
A5:   m = [[dom m,cod m],m`2] by Th8;
      x in Maps W by A3,A4;
      then reconsider m9 = x as Element of Maps V by A2;
A6:   dom m = dom m9 & cod m = cod m9;
      m = [[A,B],m `2 ] by A3,Th16;
      then dom m = A & cod m = B by A5,Lm1;
      hence thesis by A1,A6,Th19;
    end;
    assume
A7: x in Maps(A9,B9);
    Maps(A9,B9) c= Maps V by Th17;
    then reconsider m9 = x as Element of Maps V by A7;
A8: m9 = [[A9,B9],m9`2] by A7,Th16;
    then
A9: m9`2 is Function of A9,B9 by A7,Lm4;
    B9 = {} implies A9 = {} by A7,A8,Lm4;
    hence x in Maps(A,B) by A1,A8,A9,Th15;
  end;
  hence thesis by TARSKI:1;
end;

definition
  let V,m;
  attr m is surjective means
  rng m`2 = cod(m);
end;

begin  :: Category Ens

definition
  let V;
  func fDom V -> Function of Maps V,V means
  :Def9:
  for m holds it.m = dom m;
  existence
  proof
    deffunc F(Element of Maps V) = dom $1;
    ex F being Function of Maps V,V st for m holds F.m = F(m) from FUNCT_2
    :sch 4;
    hence thesis;
  end;
  uniqueness
  proof
    let h1,h2 be Function of Maps V,V such that
A1: for m holds h1.m = dom m and
A2: for m holds h2.m = dom m;
    now
      let m;
      thus h1.m = dom m by A1
        .= h2.m by A2;
    end;
    hence thesis by FUNCT_2:63;
  end;
  func fCod V -> Function of Maps V,V means
  :Def10:
  for m holds it.m = cod m;
  existence
  proof
    deffunc F(Element of Maps V) = cod $1;
    ex F being Function of Maps V,V st for m holds F.m = F(m) from FUNCT_2
    :sch 4;
    hence thesis;
  end;
  uniqueness
  proof
    let h1,h2 be Function of Maps V,V such that
A3: for m holds h1.m = cod m and
A4: for m holds h2.m = cod m;
    now
      let m;
      thus h1.m = cod m by A3
        .= h2.m by A4;
    end;
    hence thesis by FUNCT_2:63;
  end;
  func fComp V -> PartFunc of [:Maps V,Maps V:],Maps V means
  :Def11:
  (for m2,
m1 holds [m2,m1] in dom it iff dom m2 = cod m1) & for m2,m1 st dom m2 = cod m1
  holds it.[m2,m1] = m2*m1;
  existence
  proof
    defpred P[set,set,set] means for m2,m1 st m2=$1 & m1=$2 holds dom m2 = cod
    m1 & $3 = m2*m1;
A5: for x,y,z1,z2 being set st x in Maps(V) & y in Maps(V) & P[x,y,z1] &
    P[x,y,z2] holds z1 = z2
    proof
      let x,y,z1,z2 be set;
      assume x in Maps(V) & y in Maps(V);
      then reconsider m2 = x, m1 = y as Element of Maps(V);
      assume that
A6:   P[x,y,z1] and
A7:   P[x,y,z2];
      z1 = m2*m1 by A6;
      hence thesis by A7;
    end;
A8: for x,y,z being set st x in Maps(V) & y in Maps(V) & P[x,y,z] holds z
    in Maps(V)
    proof
      let x,y,z be set;
      assume x in Maps(V) & y in Maps(V);
      then reconsider m2 = x, m1 = y as Element of Maps(V);
      assume P[x,y,z];
      then z = m2*m1;
      hence thesis;
    end;
    consider h being PartFunc of [:Maps(V),Maps(V):],Maps(V) such that
A9: for x,y being set holds [x,y] in dom h iff x in Maps(V) & y in
    Maps(V) & ex z being set st P[x,y,z] and
A10: for x,y being set st [x,y] in dom h holds P[x,y,h.(x,y)] from
    BINOP_1:sch 5(A8,A5);
    take h;
    thus
A11: for m2,m1 holds [m2,m1] in dom h iff dom m2 = cod m1
    proof
      let m2,m1;
      thus [m2,m1] in dom h implies dom m2 = cod m1
      proof
        assume [m2,m1] in dom h;
        then ex z being set st P[m2,m1,z] by A9;
        hence thesis;
      end;
      assume dom m2 = cod m1;
      then P[m2,m1,m2*m1];
      hence thesis by A9;
    end;
    let m2,m1;
    assume dom m2 = cod m1;
    then [m2,m1] in dom h by A11;
    then P[m2,m1,h.(m2,m1)] by A10;
    hence thesis;
  end;
  uniqueness
  proof
    let h1,h2 be PartFunc of [:Maps V,Maps V:],Maps V such that
A12: for m2,m1 holds [m2,m1] in dom h1 iff dom m2 = cod m1 and
A13: for m2,m1 st dom m2 = cod m1 holds h1.[m2,m1] = m2*m1 and
A14: for m2,m1 holds [m2,m1] in dom h2 iff dom m2 = cod m1 and
A15: for m2,m1 st dom m2 = cod m1 holds h2.[m2,m1] = m2*m1;
A16: dom h2 c= [:Maps V,Maps V:] by RELAT_1:def 18;
A17: dom h1 c= [:Maps V,Maps V:] by RELAT_1:def 18;
A18: dom h1 = dom h2
    proof
      let x,y be set;
      thus [x,y] in dom h1 implies [x,y] in dom h2
      proof
        assume
A19:    [x,y] in dom h1;
        then reconsider m2 = x, m1 = y as Element of Maps V by A17,ZFMISC_1:87
;
        dom m2 = cod m1 by A12,A19;
        hence thesis by A14;
      end;
      assume
A20:  [x,y] in dom h2;
      then reconsider m2 = x, m1 = y as Element of Maps V by A16,ZFMISC_1:87;
      dom m2 = cod m1 by A14,A20;
      hence thesis by A12;
    end;
    now
      let m be Element of [:Maps V,Maps V:];
      consider m2,m1 such that
A21:  m = [m2,m1] by DOMAIN_1:1;
      assume m in dom h1;
      then
A22:  dom m2 = cod m1 by A12,A21;
      then h1.[m2,m1] = m2*m1 by A13;
      hence h1.m = h2.m by A15,A21,A22;
    end;
    hence thesis by A18,PARTFUN1:5;
  end;
end;

definition
 canceled;
  let V;
  func Ens(V) -> non empty non void strict CatStr equals
  CatStr(# V,Maps V,fDom V,fCod V,fComp V#);
  coherence;
end;

registration
  let V;
  cluster Ens(V) -> Category-like
   reflexive transitive associative with_identities;
  coherence
proof
  set M = Maps V, d = fDom V, c = fCod V, p = fComp V;
  reconsider C = CatStr(#V,M,d,c,p#) as non empty non void CatStr;
A1:  C is Category-like
  proof
      let ff,gg be Morphism of C;
       reconsider f=ff, g=gg as Element of M;
      d.g = dom g & c.f = cod f by Def9,Def10;
      hence thesis by Def11;
  end;
A2: C is transitive
  proof
      let ff,gg be Morphism of C such that
A3:   dom gg=cod ff;
      [gg,ff] in dom the Comp of C by A3,A1,CAT_1:def 6;
      then
A4:    (the Comp of C).(gg,ff) = gg(*)ff by CAT_1:def 1;
      reconsider f=ff, g=gg as Element of M;
A5:   d.g = dom g & c.f = cod f by Def9,Def10;
      then
A6:   p.[g,f] = g*f by A3,Def11;
A7:   d.f = dom f & c.g = cod g by Def9,Def10;
      dom(g*f) = dom f & cod(g*f) = cod g by A3,A5,Th12;
      hence thesis by A6,A7,Def9,Def10,A4;
    end;
A8: C is associative
   proof
      let ff,gg,hh be Morphism of C such that
A9:   dom hh = cod gg and
A10:   dom gg = cod ff;
      reconsider f=ff, g=gg, h=hh as Element of M;
A11:   dom h = d.h & cod g = c.g by Def9,Def10;
      then
A12:   dom(h*g) = dom g by A9,Th12;
A13:   dom g = d.g & cod f = c.f by Def9,Def10;
      then
A14:  cod(g*f) = dom h by A9,A10,A11,Th12;
       [hh,gg] in dom the Comp of C by A9,A1,CAT_1:def 6;
       then
A15:     hh(*)gg =(the Comp of C).(hh,gg) by CAT_1:def 1;
       dom(hh(*)gg) = dom gg by A2,CAT_1:def 7,A9;
       then
A16:     [hh(*)gg,ff] in dom the Comp of C by A1,CAT_1:def 6,A10;
       [gg,ff] in dom the Comp of C by A10,A1,CAT_1:def 6;
       then
A17:     gg(*)ff =(the Comp of C).(gg,ff) by CAT_1:def 1;
       cod(gg(*)ff) = cod gg by A2,CAT_1:def 7,A10;
       then [hh,gg(*)ff] in dom the Comp of C by A1,CAT_1:def 6,A9;
      hence hh(*)(gg(*)ff)
         = (the Comp of C).(hh,(the Comp of C).(gg,ff)) by A17,CAT_1:def 1
        .= p.[h,g*f] by A10,A13,Def11
        .= h*(g*f) by A14,Def11
        .= (h*g)*f by A9,A10,A11,A13,Th13
        .= p.[h*g,f] by A10,A13,A12,Def11
        .= (the Comp of C).((the Comp of C).(hh,gg),ff) by A9,A11,Def11
        .= hh(*)gg(*)ff by A16,A15,CAT_1:def 1;
    end;
A18: C is reflexive
    proof let a be Element of C;
      reconsider aa=a as Element of V;
      reconsider ii = id$aa as Morphism of C;
A19:    cod ii = cod id$ aa by Def10
        .= a by Th11;
      dom ii = dom id$ aa by Def9
         .= a by Th11;
      then ii in Hom(a,a) by A19;
     hence Hom(a,a)<>{};
    end;
 C is with_identities
   proof let a be Element of C;
     reconsider aa=a as Element of V;
     reconsider ii = id$ aa as Morphism of C;
A20:   cod ii = cod id$ aa by Def10
        .= a by Th11;
A21:    dom ii = dom id$ aa by Def9
         .= a by Th11;
     then reconsider ii as Morphism of a,a by A20,CAT_1:4;
    take ii;
    let b be Element of C;
    thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g
     proof assume
A22:     Hom(a,b)<>{};
      let g be Morphism of a,b;
       reconsider gg = g as Element of Maps V;
A23:     dom gg = dom g by Def9
          .= aa by A22,CAT_1:5;
       then
A24:     cod id$ aa = dom gg by Th11;
       dom g = a by A22,CAT_1:5;
       then [g,ii] in dom p by A20,A1,CAT_1:def 6;
      hence g(*)ii = p.(g,ii) by CAT_1:def 1
           .= gg*(id$ aa) by A24,Def11
           .= g by A23,Th14;
     end;
      assume
A25:     Hom(b,a)<>{};
      let g be Morphism of b,a;
       reconsider gg = g as Element of Maps V;
A26:     cod gg = cod g by Def10
          .= aa by A25,CAT_1:5;
       then
A27:     dom id$ aa = cod gg by Th11;
       cod g = a by A25,CAT_1:5;
       then [ii,g] in dom p by A21,A1,CAT_1:def 6;
      hence ii(*)g = p.(ii,g) by CAT_1:def 1
           .= (id$ aa)*gg by A27,Def11
           .= g by A26,Th14;
  end;
  hence thesis by A1,A2,A8,A18;
end;
end;

reserve a,b for Object of Ens(V);

canceled;

theorem
  A is Object of Ens(V);

definition
  let V,A;
  func @A -> Object of Ens(V) equals
  A;
  coherence;
end;

theorem
  a is Element of V;

definition
  let V,a;
  func @a -> Element of V equals
  a;
  coherence;
end;

reserve f,g,f1,f2 for Morphism of Ens(V);

theorem
  m is Morphism of Ens(V);

definition
  let V,m;
  func @m -> Morphism of Ens(V) equals
  m;
  coherence;
end;

theorem
  f is Element of Maps(V);

definition
  let V,f;
  func @f -> Element of Maps(V) equals
  f;
  coherence;
end;

theorem
  dom f = dom(@f) & cod f = cod(@f) by Def9,Def10;

theorem Th27:
  Hom(a,b) = Maps(@a,@b)
proof
  now
    let x be set;
    thus x in Hom(a,b) implies x in Maps(@a,@b)
    proof
      assume
A1:   x in Hom(a,b);
      then reconsider f = x as Morphism of Ens(V);
      cod(f) = b by A1,CAT_1:1;
      then
A2:   cod(@f) = @b by Def10;
      dom(f) = a by A1,CAT_1:1;
      then dom(@f) = @a by Def9;
      hence thesis by A2,Th19;
    end;
    assume
A3: x in Maps(@a,@b);
    Maps(@a,@b) c= Maps V by Th17;
    then reconsider m = x as Element of Maps V by A3;
    cod(m) = @b by A3,Th19;
    then
A4: cod(@m) = b by Def10;
    dom(m) = @a by A3,Th19;
    then dom(@m) = a by Def9;
    hence x in Hom(a,b) by A4;
  end;
  hence thesis by TARSKI:1;
end;

Lm6: Hom(a,b) <> {} implies Funcs(@a,@b) <> {}
proof
  set m = the Element of Maps(@a,@b);
  assume Hom(a,b) <> {};
  then
A1: Maps(@a,@b) <> {} by Th27;
  reconsider m as Element of Maps(V) by A1,TARSKI:def 3,Th17;
  m`2 in Funcs(@a,@b) by A1,Th20;
  hence thesis;
end;

theorem Th28:
  dom g = cod f implies g(*)f = (@g)*(@f)
proof
  assume
A1: dom g = cod f;
  then dom(@g) = cod f by Def9;
  then
A2: dom(@g) = cod(@f) by Def10;
  thus g(*)f = (the Comp of Ens(V)).(@g,f) by A1,CAT_1:16
    .= (@g)*(@f) by A2,Def11;
end;

theorem Th29:
  id a = id$ @a
proof
     reconsider aa=a as Element of V;
     reconsider ii = id$ aa as Morphism of Ens V;
A1:   cod ii = cod id$ aa by Def10
        .= a by Th11;
A2:    dom ii = dom id$ aa by Def9
         .= a by Th11;
     then reconsider ii as Morphism of a,a by A1,CAT_1:4;
  for b being Object of Ens V 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 Element of Ens V;
     set p = the Comp of Ens V;
    thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g
     proof assume
A3:     Hom(a,b)<>{};
      let g be Morphism of a,b;
       reconsider gg = g as Element of Maps V;
A4:     dom gg = dom g by Def9
          .= aa by A3,CAT_1:5;
       then
A5:     cod id$ aa = dom gg by Th11;
       dom g = a by A3,CAT_1:5;
       then [g,ii] in dom p by A1,CAT_1:def 6;
      hence g(*)ii = p.(g,ii) by CAT_1:def 1
           .= gg*(id$ aa) by A5,Def11
           .= g by A4,Th14;
     end;
      assume
A6:     Hom(b,a)<>{};
      let g be Morphism of b,a;
       reconsider gg = g as Element of Maps V;
A7:     cod gg = cod g by Def10
          .= aa by A6,CAT_1:5;
       then
A8:     dom id$ aa = cod gg by Th11;
       cod g = a by A6,CAT_1:5;
       then [ii,g] in dom p by A2,CAT_1:def 6;
      hence ii(*)g = p.(ii,g) by CAT_1:def 1
           .= (id$ aa)*gg by A8,Def11
           .= g by A7,Th14;
  end;

 hence thesis by CAT_1:def 12;
end;

theorem
  a = {} implies a is initial
proof
  assume
A1: a = {};
  let b;
  Maps(@a,@b) <> {} by A1,Th15;
  hence
A2: Hom(a,b)<>{} by Th27;
  set m = [[@a,@b],{}];
  {} is Function of @a,@b by A1,RELSET_1:12;
  then
 m in Maps(@a,@b) by A1,Th15;
  then m in Hom(a,b) by Th27;
  then reconsider f = m as Morphism of a,b by CAT_1:def 5;
  take f;
  let g be Morphism of a,b;
  reconsider m9 = g as Element of Maps(V);
  g in Hom(a,b) by A2,CAT_1:def 5;
  then
A3: g in Maps(@a,@b) by Th27;
  then
A4: m9 = [[@a,@b],m9`2] by Th16;
  then m9`2 is Function of @a,@b by A3,Lm4;
  hence thesis by A1,A4;
end;

theorem Th31:
  {} in V & a is initial implies a = {}
proof
  assume {} in V;
  then reconsider B = {} as Element of V;
  set b = @B;
  assume a is initial;
  then Hom(a,b) <> {} by CAT_1:def 19;
  then Funcs(@a,@b) <> {} by Lm6;
  hence thesis;
end;

theorem
  for W being Universe, a being Object of Ens(W) st a is initial holds a
  = {} by Th31,CLASSES2:56;

theorem
  (ex x being set st a = {x}) implies a is terminal
proof
  given x being set such that
A1: a = {x};
  let b;
  set h = the Function of @b,@a;
  set m = [[@b,@a],h];
A2: m in Maps(@b,@a) by A1,Th15;
  hence
A3: Hom(b,a)<>{} by Th27;
  m in Hom(b,a) by A2,Th27;
  then reconsider f = m as Morphism of b,a by CAT_1:def 5;
  take f;
  let g be Morphism of b,a;
  reconsider m9 = g as Element of Maps(V);
  g in Hom(b,a) by A3,CAT_1:def 5;
  then
A4: g in Maps(@b,@a) by Th27;
  then
A5: m9 = [[@b,@a],m9`2] by Th16;
  then m9`2 is Function of @b,@a by A4,Lm4;
  hence thesis by A1,A5,FUNCT_2:51;
end;

theorem Th34:
  V <> {{}} & a is terminal implies ex x being set st a = {x}
proof
  assume that
A1: V <> {{}} and
A2: a is terminal;
  set x = the Element of @a;
A3: now
    assume
A4: @a = {};
    now
      consider C being set such that
A5:   C in V and
A6:   C <> {} by A1,ZFMISC_1:35;
      reconsider C as Element of V by A5;
      set b = @C;
      Hom(b,a) <> {} by A2,CAT_1:def 18;
      then Funcs(@b,@a) <> {} by Lm6;
      hence contradiction by A4,A6;
    end;
    hence contradiction;
  end;
  now
    assume a <> {x};
    then consider y being set such that
A7: y in @a and
A8: y <> x by A3,ZFMISC_1:35;
    reconsider fy = @a --> y as Function of @a,@a by A7,FUNCOP_1:45;
    reconsider fx = @a --> x as Function of @a,@a by A7,FUNCOP_1:45;
    fx.y = x by A7,FUNCOP_1:7;
    then
A9: fx <> fy by A7,A8,FUNCOP_1:7;
A10: ([[@a,@a],fx]) in Maps(@a,@a) by Th15;
A11: ([[@a,@a],fy]) in Maps(@a,@a) by Th15;
    Maps(@a,@a) c= Maps V by Th17;
    then reconsider
    m1 = [[@a,@a],fx],m2 = [[@a,@a],fy] as Element of Maps(V) by A10,A11;
A12: m2 in Hom(a,a) by A11,Th27;
    m1 in Hom(a,a) by A10,Th27;
    then reconsider f = @m1,g = @m2 as Morphism of a,a by A12,CAT_1:def 5;
    consider h being Morphism of a,a such that
A13: for h9 being Morphism of a,a holds h = h9 by A2,CAT_1:def 18;
    f = h by A13
      .= g by A13;
    hence contradiction by A9,XTUPLE_0:1;
  end;
  hence thesis;
end;

theorem
  for W being Universe, a being Object of Ens(W) st a is terminal ex x
  being set st a = {x}
proof
  let W be Universe, a be Object of Ens(W);
  now
A1: {{}} in W by CLASSES2:56,57;
    assume W = {{}};
    hence contradiction by A1;
  end;
  hence thesis by Th34;
end;

theorem
 for a,b being Object of Ens(V), f being Morphism of a,b st Hom(a,b) <> {}
  holds f is monic iff (@f)`2 is one-to-one
proof
 let a,b be Object of Ens(V), f be Morphism of a,b such that
A1: Hom(a,b) <> {};
  set m = @f;
A2: dom m = dom f by Def9;
  then
A3: dom m`2 = dom f by Lm3;
  thus f is monic implies (@f)`2 is one-to-one
  proof
    set A = dom (@f)`2;
    assume
A4: f is monic;
    let x1,x2 be set such that
A5: x1 in A and
A6: x2 in A and
A7: (@f)`2.x1 = (@f)`2.x2;
A8: A = dom(@f) by Lm3;
    then reconsider A as Element of V;
A9: dom f = A by A8,Def9;
    reconsider fx1 = A --> x1, fx2 = A --> x2 as Function of A,A by A5,A6,
FUNCOP_1:45;
    reconsider m1 = [[A,A],fx1],m2 = [[A,A],fx2] as Element of Maps(V) by Th5;
    set f1 = @m1, f2 = @m2;
    set h1 = (@f)`2*(@f1)`2, h2 = (@f)`2*(@f2)`2;
    set ff1 = (@f)*(@f1), ff2 = (@f)*(@f2);
A10: m2 = [[dom m2,cod m2],m2`2] by Th8;
    then
A11: dom m2 = A by Lm1;
A12: cod m2 = A by A10,Lm1;
    then
A13: (ff2)`2 = h2 & dom(ff2) = dom(@f2) by A8,Th12;
    cod(ff2) = cod(@f) by A8,A12,Th12;
    then
A14: ff2=[[dom(@f2),cod(@f)],h2] by A13,Th8;
    dom(@f2) = A by A10,Lm1;
    then
A15: dom f2 = A by Def9;
    cod(@f2) = A by A10,Lm1;
    then
A16: cod f2 = A by Def10;
    then
A17: f(*)(f2) = ff2 by A9,Th28;
A18: m1 = [[dom m1,cod m1],m1`2] by Th8;
    then
A19: cod m1 = A by Lm1;
    then
A20: (ff1)`2 = h1 & dom(ff1) = dom(@f1) by A8,Th12;
A21: dom m1 = A by A18,Lm1;
    now
      thus
A22:  dom(h1) = A & dom(h2) = A by A21,A11,A20,A13,Lm3;
      let x be set;
      assume
A23:  x in A;
      fx1 = m1`2 by A18,XTUPLE_0:1;
      then (@f1)`2.x = x1 by A23,FUNCOP_1:7;
      then
A24:  h1.x = (@f)`2.x1 by A22,A23,FUNCT_1:12;
      fx2 = m2`2 by A10,XTUPLE_0:1;
      then (@f2)`2.x = x2 by A23,FUNCOP_1:7;
      hence h1.x = h2.x by A7,A22,A23,A24,FUNCT_1:12;
    end;
    then
A25: h1 = h2 by FUNCT_1:2;
    cod(ff1) = cod(@f) by A8,A19,Th12;
    then
A26: ff1=[[dom(@f1),cod(@f)],h1] by A20,Th8;
    dom(@f1) = A by A18,Lm1;
    then
A27: dom f1 = A by Def9;
    cod(@f1) = A by A18,Lm1;
    then
A28: cod f1 = A by Def10;
    reconsider A as Object of Ens(V);
A29: dom f = a by A1,CAT_1:5;
    then
A30: f1 in Hom(A,a) & f2 in Hom(A,a) by A27,A9,A28,A15,A16;
    then reconsider f1,f2 as Morphism of A,a by CAT_1:def 5;
A31: f*f1 = f(*)f1 by A1,A30,CAT_1:def 13
      .= f(*)f2 by A21,A11,A26,A14,A25,A17,A28,A9,Th28
      .= f*f2 by A1,A30,CAT_1:def 13;
    Hom(A,a) <> {} by A29,A9;
    then f1 = f2 by A4,A31,CAT_1:def 14;
    then fx1 = fx2 by XTUPLE_0:1;
    hence x1 = fx2.x1 by A5,FUNCOP_1:7
      .= x2 by A5,FUNCOP_1:7;
  end;
  assume
A32: m`2 is one-to-one;
  thus Hom(a,b) <> {} by A1;
  let c be Object of Ens(V) such that
A33: Hom(c,a) <> {};
  let f1,f2 be Morphism of c,a;
A34: dom f1 = c by A33,CAT_1:5 .= dom f2 by A33,CAT_1:5;
A35: cod f1 = a by A33,CAT_1:5 .= dom f by A1,CAT_1:5;
A36: cod f2 = a by A33,CAT_1:5 .= dom f by A1,CAT_1:5;
  assume
A37: f*f1 = f*f2;
  set m1 = @f1, m2 = @f2;
A38: m*m1 = f(*)f1 by A35,Th28
     .= f*f1 by A33,A1,CAT_1:def 13;
A39: m*m2 = f(*)f2 by A36,Th28
     .= f*f2 by A33,A1,CAT_1:def 13;
A40: m1=[[dom m1,cod m1],m1`2] by Th8;
A41: dom m2 = dom f2 by Def9;
  then
A42: dom m2`2 = dom f2 by Lm3;
A43: cod m1 = cod f1 by Def10;
  then
A44: rng m1`2 c= cod f1 by Lm3;
A45: cod m2 = cod f2 by Def10;
  then
A46: rng m2`2 c= cod f2 by Lm3;
A47: m*m2 = [[dom m2,cod m],m`2*m2`2] by A36,A45,A2,Def6;
  m*m1 = [[dom m1,cod m],m`2*m1`2] by A35,A43,A2,Def6;
  then
A48: (m`2)*(m1`2) = (m`2)*(m2`2) by A39,A37,A38,A47,XTUPLE_0:1;
A49: dom m1 = dom f1 by Def9;
  then dom m1`2 = dom f1 by Lm3;
  then m1`2 = m2`2 by A32,A34,A35,A36,A42,A3,A44,A46,A48,FUNCT_1:27;
  hence thesis by A34,A35,A36,A49,A41,A43,A45,A40,Th8;
end;

theorem Th37:
 for a,b being Object of Ens(V), f being Morphism of a,b
   st Hom(a,b) <> {}
  holds f is epi & (ex A st ex x1,x2 being set st x1 in A & x2 in A & x1
  <> x2) implies @f is surjective
proof
 let a,b be Object of Ens(V), f be Morphism of a,b such that
A1: Hom(a,b) <> {};
  assume
A2: f is epi;
  given B being Element of V, x1,x2 being set such that
A3: x1 in B and
A4: x2 in B and
A5: x1 <> x2;
A6: cod(@f) c= rng (@f)`2
  proof
    set A = cod(@f);
    reconsider g1 = A --> x1 as Function of A,B by A3,FUNCOP_1:45;
    let x be set;
    assume that
A7: x in A and
A8: not x in rng (@f)`2;
    set h = {x} --> x2, g2 = g1 +* h;
A9: dom h = {x} by FUNCOP_1:13;
A10: rng h = {x2} by FUNCOP_1:8;
    rng g1 = {x1} by A7,FUNCOP_1:8;
    then rng g2 c= {x1} \/ {x2} by A10,FUNCT_4:17;
    then
A11: rng g2 c= {x1,x2} by ENUMSET1:1;
    {x1,x2} c= B by A3,A4,ZFMISC_1:32;
    then
A12: rng g2 c= B by A11,XBOOLE_1:1;
    dom g1 = A by FUNCOP_1:13;
    then dom g2 = A \/ {x} by A9,FUNCT_4:def 1
      .= A by A7,ZFMISC_1:40;
    then reconsider g2 as Function of A,B by A3,A12,FUNCT_2:def 1,RELSET_1:4;
A13: cod f = A by Def10;
A14: x in {x} by TARSKI:def 1;
    then h.x = x2 by FUNCOP_1:7;
    then
A15: g2.x = x2 by A14,A9,FUNCT_4:13;
A16: g1.x = x1 by A7,FUNCOP_1:7;
    reconsider m1 = [[A,B],g1], m2 = [[A,B],g2] as Element of Maps(V) by A3,Th5
;
    set f1 = @m1, f2 = @m2;
    set h1 = (@f1)`2*(@f)`2, h2 = (@f2)`2*(@f)`2;
    set f1f = (@f1)*(@f), f2f = (@f2)*(@f);
A17: m1 = [[dom m1,cod m1],m1`2] by Th8;
    then
A18: g1 = m1`2 by XTUPLE_0:1;
A19: dom m1 = A by A17,Lm1;
    then
A20: (f1f)`2 = h1 & dom(f1f) = dom(@f) by Th12;
A21: m2 = [[dom m2,cod m2],m2`2] by Th8;
    then
A22: dom m2 = A by Lm1;
    then
A23: (f2f)`2 = h2 & dom(f2f) = dom(@f) by Th12;
    cod(@f2) = B by A21,Lm1;
    then
A24: cod f2 = B by Def10;
    dom(@f2) = A by A21,Lm1;
    then
A25: dom f2 = A by Def9;
    then
A26: f2(*)f = f2f by A13,Th28;
A27: g2 = m2`2 by A21,XTUPLE_0:1;
    now
      thus
A28:  dom(h1) = dom(@f) & dom(h2) = dom(@f) by A20,A23,Lm3;
      let z be set;
      set y = (@f)`2.z;
      assume
A29:  z in dom(@f);
      then z in dom (@f)`2 by Lm3;
      then y in rng (@f)`2 by FUNCT_1:def 3;
      then
A30:  not y in {x} by A8,TARSKI:def 1;
      h1.z = g1.y & h2.z = g2.y by A18,A27,A28,A29,FUNCT_1:12;
      hence h1.z = h2.z by A9,A30,FUNCT_4:11;
    end;
    then
A31: h1 = h2 by FUNCT_1:2;
    cod(f1f) = cod(@f1) by A19,Th12;
    then
A32: f1f=[[dom(@f),cod(@f1)],h1] by A20,Th8;
    cod(f2f) = cod(@f2) by A22,Th12;
    then
A33: f2f=[[dom(@f),cod(@f2)],h2] by A23,Th8;
    cod m1 = B by A17,Lm1;
    then
A34: f1f = f2f by A21,A32,A33,A31,Lm1;
    cod(@f1) = B by A17,Lm1;
    then
A35: cod f1 = B by Def10;
    dom(@f1) = A by A17,Lm1;
    then
A36: dom f1 = A by Def9;
   reconsider B as Object of Ens(V);
A37:  cod f = b by A1,CAT_1:5;
   then
A38:  f1 in Hom(b,B) by A13,A35,A36;
    then reconsider f1 as Morphism of b,B by CAT_1:def 5;
    f2 in Hom(b,B) by A13,A24,A25,A37;
    then reconsider f2 as Morphism of b,B by CAT_1:def 5;
    f1*f = f1(*)f by A1,A38,CAT_1:def 13
     .= f2(*)f by A34,A26,A36,A13,Th28
     .= f2*f by A1,A38,CAT_1:def 13;
    then f1 = f2 by A2,A38,CAT_1:def 15;
    hence contradiction by A5,A16,A15,XTUPLE_0:1;
  end;
  rng (@f)`2 c= cod(@f) by Lm3;
  hence rng (@f)`2 = cod(@f) by A6,XBOOLE_0:def 10;
end;

theorem
 for a,b being Object of Ens(V) st Hom(a,b) <> {}
 for f being Morphism of a,b st  @f is surjective
  holds f is epi
proof
 let a,b be Object of Ens(V) such that
A1: Hom(a,b) <> {};
 let f be Morphism of a,b;
  set m = @f;
  assume
A2: rng m`2 = cod m;
  thus Hom(a,b) <> {} by A1;
  let c be Object of Ens(V) such that
A3: Hom(b,c) <> {};
  let f1,f2 be Morphism of b,c;
A4: dom f1 = b by A3,CAT_1:5 .=  cod f by A1,CAT_1:5;
A5: dom f2 = b by A3,CAT_1:5 .= cod f by A1,CAT_1:5;
A6: cod f1 = c by A3,CAT_1:5 .= cod f2 by A3,CAT_1:5;
  assume
A7: f1*f=f2*f;
  set m1 = @f1, m2 = @f2;
A8: m1*m = f1(*)f by A4,Th28
      .= f1*f by A1,A3,CAT_1:def 13;
A9: m2*m = f2(*)f by A5,Th28
      .= f2*f by A1,A3,CAT_1:def 13;
A10: m1=[[dom m1,cod m1],m1`2] by Th8;
A11: cod m1 = cod f1 & cod m2 = cod f2 by Def10;
A12: dom m2 = dom f2 by Def9;
  then
A13: dom m2`2 = dom f2 by Lm3;
A14: cod m = cod f by Def10;
  then
A15: m2*m = [[dom m,cod m2],m2`2*m`2] by A5,A12,Def6;
A16: dom m1 = dom f1 by Def9;
  then m1*m = [[dom m,cod m1],m1`2*m`2] by A4,A14,Def6;
  then
A17: (m1`2)*(m`2) = (m2`2)*(m`2) by A7,A8,A15,A9,XTUPLE_0:1;
  dom m1`2 = dom f1 by A16,Lm3;
  then m1`2 = m2`2 by A2,A4,A5,A14,A17,A13,FUNCT_1:86;
  hence thesis by A4,A5,A6,A16,A12,A11,A10,Th8;
end;

theorem
  for W being Universe, a,b being Object of Ens(W) st Hom(a,b) <> {}
  for f being Morphism of a,b st f is epi holds @f
  is surjective
proof
  let W be Universe, a,b being Object of Ens(W) such that
A1: Hom(a,b) <> {};
  let f be Morphism of a,b;
  {} in W & {{}} in W by CLASSES2:56,57;
  then
A2: {{},{{}}} in W by CLASSES2:58;
  {} in {{},{{}}} & {{}} in {{},{{}}} by TARSKI:def 2;
  hence thesis by A2,Th37,A1;
end;

Lm7:
  for W being non empty Subset of V
   holds Ens W is Subcategory of Ens V
proof
  let W be non empty Subset of V;
A1: for a,b being Object of Ens(W), a9,b9 being Object of Ens(V) st a = a9 &
  b = b9 holds Hom(a,b) = Hom(a9,b9)
  proof
    let a,b be Object of Ens(W), a9,b9 be Object of Ens(V);
    assume
A2: a = a9 & b = b9;
    Hom(a,b) = Maps(@a,@b) & Hom(a9,b9) = Maps(@a9,@b9) by Th27;
    hence thesis by A2,Lm5;
  end;
    set w = the Comp of Ens(W), v = the Comp of Ens(V);
    thus the carrier of Ens(W) c= the carrier of Ens(V);
    thus for a,b being Object of Ens(W), a9,b9 being Object of Ens(V) st a =
    a9 & b = b9 holds Hom(a,b) c= Hom(a9,b9) by A1;
    now
A3:   dom w c= [:Maps W,Maps W:] by RELAT_1:def 18;
      thus
A4:   dom w c= dom v
      proof
        let x,y be set;
        assume
A5:     [x,y] in dom w;
        then consider m2,m1 being Element of Maps W such that
A6:     [x,y] = [m2,m1] by A3,DOMAIN_1:1;
        reconsider m19 = m1, m29 = m2 as Element of Maps V by Th7,TARSKI:def 3;
A7:     dom m29 = dom m2 & cod m19 = cod m1;
        dom m2 = cod m1 by A5,A6,Def11;
        hence thesis by A6,A7,Def11;
      end;
      let x be set;
      assume
A8:   x in dom w;
      then consider m2,m1 being Element of Maps W such that
A9:  x = [m2,m1] by A3,DOMAIN_1:1;
      reconsider m19 = m1, m29 = m2 as Element of Maps V by Th7,TARSKI:def 3;
A10:  dom m29 = cod m19 by A4,A8,A9,Def11;
A11:  dom m2 = cod m1 by A8,A9,Def11;
      then
A12:  m2*m1=[[dom m1,cod m2],m2`2*m1`2] by Def6;
      dom m1 = dom m19 & cod m2 = cod m29;
      then m29*m19=[[dom m1,cod m2], m2`2*m1`2] by A10,Def6;
      hence w.x = m29*m19 by A9,A11,A12,Def11
        .= v.x by A9,A10,Def11;
    end;
    hence the Comp of Ens(W) c= the Comp of Ens(V) by GRFUNC_1:2;
    let a be Object of Ens(W), a9 be Object of Ens(V);
A13: id$(@a) = [[@a,@a],id(@a)];
    assume a = a9;
    hence id a = id$(@a9) by A13,Th29
      .= id a9 by Th29;
end;

theorem
  for W being non empty Subset of V
   holds Ens W is full Subcategory of Ens V
proof
  let W be non empty Subset of V;
   reconsider E = Ens W as Subcategory of Ens V by Lm7;
 for a,b being Object of E, a9,b9 being Object of Ens(V) st a = a9 &
  b = b9 holds Hom(a,b) = Hom(a9,b9)
  proof
    let a,b be Object of E, a9,b9 be Object of Ens(V);
    assume
A1: a = a9 & b = b9;
    reconsider aa=a, bb=b as Element of Ens W;
    Hom(aa,bb) = Maps(@aa,@bb) & Hom(a9,b9) = Maps(@a9,@b9) by Th27;
    hence thesis by A1,Lm5;
  end;
  hence thesis by CAT_2:def 6;
end;

begin :: Representable Functors

reserve C for Category,
  a,b,a9,b9,c for Object of C,
  f,g,h,f9,g9 for Morphism of C;

definition
  let C;
  func Hom(C) -> set equals
  { Hom(a,b): not contradiction };
  coherence;
end;

registration
  let C;
  cluster Hom(C) -> non empty;
  coherence
  proof
    set a = the Object of C;
    Hom(a,a) in { Hom(a9,b9): not contradiction };
    hence thesis;
  end;
end;

theorem
  Hom(a,b) in Hom(C);

:: hom-functors

theorem
  (Hom(a,cod f) = {} implies Hom(a,dom f) = {}) & (Hom(dom f,a) = {}
  implies Hom(cod f,a) = {})
proof
  Hom(dom f,cod f) <> {} by CAT_1:2;
  hence thesis by CAT_1:24;
end;

definition
  let C,a,f;
  func hom(a,f) -> Function of Hom(a,dom f),Hom(a,cod f) means
  :Def19:
  for g st g in Hom(a,dom f) holds it.g = f(*)g;
  existence
  proof
    defpred P[set,set] means for g st g = $1 holds $2 = f(*)g;
    set X = Hom(a,dom f), Y = Hom(a,cod f);
A1: for x being set st x in X ex y being set st y in Y & P[x,y]
    proof
      let x be set;
      assume
A2:   x in X;
      then reconsider g = x as Morphism of a,dom f by CAT_1:def 5;
      take f(*)g;
      Hom(dom f,cod f) <> {} & f is Morphism of dom f,cod f by CAT_1:1,4;
      hence thesis by A2,CAT_1:23;
    end;
    consider h being Function such that
A3: dom h = X & rng h c= Y and
A4: for x being set st x in X holds P[x,h.x] from FUNCT_1:sch 5(A1);
    Hom(dom f,cod f) <> {} by CAT_1:2;
    then Y = {} implies X = {} by CAT_1:24;
    then reconsider h as Function of X,Y by A3,FUNCT_2:def 1,RELSET_1:4;
    take h;
    thus thesis by A4;
  end;
  uniqueness
  proof
    set X = Hom(a,dom f), Y = Hom(a,cod f);
    let h1,h2 be Function of X,Y such that
A5: for g st g in X holds h1.g = f(*)g and
A6: for g st g in X holds h2.g = f(*)g;
    now
      let x be set;
      assume
A7:   x in X;
      then reconsider g = x as Morphism of C;
      thus h1.x = f(*)g by A5,A7
        .= h2.x by A6,A7;
    end;
    hence thesis by FUNCT_2:12;
  end;
  func hom(f,a) -> Function of Hom(cod f,a),Hom(dom f,a) means
  :Def20:
  for g st g in Hom(cod f,a) holds it.g = g(*)f;
  existence
  proof
    defpred P[set,set] means for g st g = $1 holds $2 = g(*)f;
    set X = Hom(cod f,a), Y = Hom(dom f,a);
A8: for x being set st x in X ex y being set st y in Y & P[x,y]
    proof
      let x be set;
      assume
A9:   x in X;
      then reconsider g = x as Morphism of cod f,a by CAT_1:def 5;
      take g(*)f;
      Hom(dom f,cod f) <> {} & f is Morphism of dom f,cod f by CAT_1:2,4;
      hence thesis by A9,CAT_1:23;
    end;
    consider h being Function such that
A10: dom h = X & rng h c= Y and
A11: for x being set st x in X holds P[x,h.x] from FUNCT_1:sch 5(A8);
    Hom(dom f,cod f) <> {} by CAT_1:2;
    then Y = {} implies X = {} by CAT_1:24;
    then reconsider h as Function of X,Y by A10,FUNCT_2:def 1,RELSET_1:4;
    take h;
    thus thesis by A11;
  end;
  uniqueness
  proof
    set X = Hom(cod f,a), Y = Hom(dom f,a);
    let h1,h2 be Function of X,Y such that
A12: for g st g in X holds h1.g = g(*)f and
A13: for g st g in X holds h2.g = g(*)f;
    now
      let x be set;
      assume
A14:  x in X;
      then reconsider g = x as Morphism of C;
      thus h1.x = g(*)f by A12,A14
        .= h2.x by A13,A14;
    end;
    hence thesis by FUNCT_2:12;
  end;
end;

theorem Th43:
  hom(a,id c) = id Hom(a,c)
proof
  set A = Hom(a,c);
  now
    A = {} implies A = {};
    hence dom hom(a,id c) = A by FUNCT_2:def 1;
    let x be set;
    assume
A1: x in A;
    then reconsider g = x as Morphism of C;
A2: cod g = c by A1,CAT_1:1;
    thus hom(a,id c).x = id(c)(*)g by A1,Def19
      .= x by A2,CAT_1:21;
  end;
  hence thesis by FUNCT_1:17;
end;

theorem Th44:
  hom(id c,a) = id Hom(c,a)
proof
  set A = Hom(c,a);
  now
    A = {} implies A = {};
    hence dom hom(id c,a) = A by FUNCT_2:def 1;
    let x be set;
    assume
A1: x in A;
    then reconsider g = x as Morphism of C;
A2: dom g = c by A1,CAT_1:1;
    thus hom(id(c),a).x = g(*)id(c) by A1,Def20
      .= x by A2,CAT_1:22;
  end;
  hence thesis by FUNCT_1:17;
end;

theorem Th45:
  dom g = cod f implies hom(a,g(*)f) = hom(a,g)*hom(a,f)
proof
  assume
A1: dom g = cod f;
  then
A2: dom(g(*)f) = dom f by CAT_1:17;
A3: cod(g(*)f) = cod g by A1,CAT_1:17;
  now
    set h = hom(a,g(*)f), h2 = hom(a,g), h1 = hom(a,f);
A4: Hom(dom f,cod f) <> {} by CAT_1:2;
    then
A5: Hom(a,cod f) = {} implies Hom(a,dom f) = {} by CAT_1:24;
    Hom(dom g,cod g) <> {} by CAT_1:2;
    then
A6: Hom(a,cod g) = {} implies Hom(a,dom g) = {} by CAT_1:24;
    hence dom h = Hom(a,dom f) by A1,A2,A3,A5,FUNCT_2:def 1;
    thus
A7: dom(h2*h1) = Hom(a,dom f) by A1,A5,A6,FUNCT_2:def 1;
    let x be set;
    assume
A8: x in Hom(a,dom f);
    then reconsider f9 = x as Morphism of C;
A9: cod f9 = dom f by A8,CAT_1:1;
A10: h1.x in Hom(a,dom g) by A1,A4,A8,CAT_1:24,FUNCT_2:5;
    then reconsider g9 = h1.x as Morphism of C;
    thus h.x = g(*)f(*)f9 by A2,A8,Def19
      .= g(*)(f(*)f9) by A1,A9,CAT_1:18
      .= g(*)g9 by A8,Def19
      .= h2.g9 by A10,Def19
      .= (h2*h1).x by A7,A8,FUNCT_1:12;
  end;
  hence thesis by FUNCT_1:2;
end;

theorem Th46:
  dom g = cod f implies hom(g(*)f,a) = hom(f,a)*hom(g,a)
proof
  assume
A1: dom g = cod f;
  then
A2: cod(g(*)f) = cod g by CAT_1:17;
A3: dom(g(*)f) = dom f by A1,CAT_1:17;
  now
    set h = hom(g(*)f,a), h2 = hom(g,a), h1 = hom(f,a);
A4: Hom(dom g,cod g) <> {} by CAT_1:2;
    then
A5: Hom(dom g,a) = {} implies Hom(cod g,a) = {} by CAT_1:24;
    Hom(dom f,cod f) <> {} by CAT_1:2;
    then
A6: Hom(dom f,a) = {} implies Hom(cod f,a) = {} by CAT_1:24;
    hence dom h = Hom(cod g,a) by A1,A3,A2,A5,FUNCT_2:def 1;
    thus
A7: dom(h1*h2) = Hom(cod g,a) by A1,A6,A5,FUNCT_2:def 1;
    let x be set;
    assume
A8: x in Hom(cod g,a);
    then reconsider f9 = x as Morphism of C;
A9: dom f9 = cod g by A8,CAT_1:1;
A10: h2.x in Hom(cod f,a) by A1,A4,A8,CAT_1:24,FUNCT_2:5;
    then reconsider g9 = h2.x as Morphism of C;
    thus h.x = f9(*)(g(*)f) by A2,A8,Def20
      .= f9(*)g(*)f by A1,A9,CAT_1:18
      .= g9(*)f by A8,Def20
      .= h1.g9 by A10,Def20
      .= (h1*h2).x by A7,A8,FUNCT_1:12;
  end;
  hence thesis by FUNCT_1:2;
end;

theorem Th47:
  [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] is Element of Maps(Hom(C) )
proof
  Hom(dom f,cod f) <> {} by CAT_1:2;
  then
A1: Hom(a,cod f) = {} implies Hom(a,dom f) = {} by CAT_1:24;
  Hom(a,dom f) in Hom(C) & Hom(a,cod f) in Hom(C);
  hence thesis by A1,Th5;
end;

theorem Th48:
  [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] is Element of Maps(Hom(C) )
proof
  Hom(dom f,cod f) <> {} by CAT_1:2;
  then
A1: Hom(dom f,a) = {} implies Hom(cod f,a) = {} by CAT_1:24;
  Hom(dom f,a) in Hom(C) & Hom(cod f,a) in Hom(C);
  hence thesis by A1,Th5;
end;

definition
  let C,a;
  func hom?-(a) -> Function of the carrier' of C, Maps(Hom(C)) means
  :Def21:
  for f holds it.f = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)];
  existence
  proof
    defpred P[set,set] means for f st f = $1 holds $2 = [[Hom(a,dom f),Hom(a,
    cod f)],hom(a,f)];
    set X = the carrier' of C, Y = Maps(Hom(C));
A1: for x being set st x in X ex y being set st y in Y & P[x,y]
    proof
      let x be set;
      assume x in X;
      then reconsider f = x as Morphism of C;
      take y = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)];
      y is Element of Y by Th47;
      hence thesis;
    end;
    consider h being Function such that
A2: dom h = X & rng h c= Y and
A3: for x being set st x in X holds P[x,h.x] from FUNCT_1:sch 5(A1);
    reconsider h as Function of X,Y by A2,FUNCT_2:def 1,RELSET_1:4;
    take h;
    thus thesis by A3;
  end;
  uniqueness
  proof
    let h1,h2 be Function of the carrier' of C, Maps(Hom(C)) such that
A4: for f holds h1.f = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] and
A5: for f holds h2.f = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)];
    now
      let f;
      thus h1.f = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] by A4
        .= h2.f by A5;
    end;
    hence thesis by FUNCT_2:63;
  end;
  func hom-?(a) -> Function of the carrier' of C, Maps(Hom(C)) means
  :Def22:
  for f holds it.f = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)];
  existence
  proof
    defpred P[set,set] means for f st f = $1 holds $2 = [[Hom(cod f,a),Hom(dom
    f,a)],hom(f,a)];
    set X = the carrier' of C, Y = Maps(Hom(C));
A6: for x being set st x in X ex y being set st y in Y & P[x,y]
    proof
      let x be set;
      assume x in X;
      then reconsider f = x as Morphism of C;
      take y = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)];
      y is Element of Y by Th48;
      hence thesis;
    end;
    consider h being Function such that
A7: dom h = X & rng h c= Y and
A8: for x being set st x in X holds P[x,h.x] from FUNCT_1:sch 5(A6);
    reconsider h as Function of X,Y by A7,FUNCT_2:def 1,RELSET_1:4;
    take h;
    thus thesis by A8;
  end;
  uniqueness
  proof
    let h1,h2 be Function of the carrier' of C, Maps(Hom(C)) such that
A9: for f holds h1.f = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] and
A10: for f holds h2.f = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)];
    now
      let f;
      thus h1.f = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] by A9
        .= h2.f by A10;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

Lm8: for T being Function of the carrier' of C, Maps(Hom(C)) st Hom(C) c= V
holds T is Function of the carrier' of C, the carrier' of Ens V
proof
  let T be Function of the carrier' of C, Maps(Hom(C));
  assume Hom(C) c= V;
  then Maps(Hom(C)) c= Maps(V) by Th7;
  hence thesis by FUNCT_2:7;
end;

Lm9: Hom(C) c= V implies for d being Object of Ens(V) st d = Hom(a,c) holds (
hom?-(a)).(id c) = id d
proof
A1: Hom(a,c) in Hom(C);
  assume Hom(C) c= V;
  then reconsider A = Hom(a,c) as Element of V by A1;
A2: hom(a,id c) = id A by Th43;
  let d be Object of Ens(V);
  assume d = Hom(a,c);
  hence (hom?-(a)).(id c) = id$ @d by A2,Def21
    .= id d by Th29;
end;

Lm10: Hom(C) c= V implies for d being Object of Ens(V) st d = Hom(c,a) holds (
hom-?(a)).(id c) = id d
proof
A1: Hom(c,a) in Hom(C);
  assume Hom(C) c= V;
  then reconsider A = Hom(c,a) as Element of V by A1;
A2: hom(id(c),a) = id A by Th44;
  let d be Object of Ens(V);
  assume d = Hom(c,a);
  hence (hom-?(a)).(id c) = id$ @d by A2,Def22
    .= id d by Th29;
end;

theorem Th49:
  Hom(C) c= V implies hom?-(a) is Functor of C,Ens(V)
proof
  assume
A1: Hom(C) c= V;
  then reconsider
  T = hom?-(a) as Function of the carrier' of C, the carrier' of
  Ens V by Lm8;
  now
    thus for c being Object of C ex d being Object of Ens V st T.(id c) = id d
    proof
      let c be Object of C;
      Hom(a,c) in Hom(C);
      then reconsider A = Hom(a,c) as Element of V by A1;
      take d = @A;
      thus thesis by A1,Lm9;
    end;
    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;
      set b = dom f, c = cod f;
      set g = T.f;
      Hom(a,b) in Hom(C) & Hom(a,c) in Hom(C);
      then reconsider A = Hom(a,b), B = Hom(a,c) as Element of V by A1;
A2:   [[Hom(a,b),Hom(a,c)],hom(a,f)] = @g by Def21
        .= [[dom(@g), cod(@g)],(@g)`2] by Th8
        .= [[dom g, cod(@g)],(@g)`2] by Def9
        .= [[dom g, cod g],(@g)`2] by Def10;
      thus T.(id b) = id @A by A1,Lm9
        .= id dom (T.f) by A2,Lm1;
      thus T.(id c) = id @B by A1,Lm9
        .= id cod (T.f) by A2,Lm1;
    end;
    let f,g be Morphism of C such that
A3: dom g = cod f;
A4: [[Hom(a,dom g),Hom(a,cod g)],hom(a,g)] = @(T.g) by Def21
      .= [[dom(@(T.g)),cod(@(T.g))],(@(T.g))`2] by Th8
      .= [[dom(T.g),cod(@(T.g))],(@(T.g))`2] by Def9
      .= [[dom(T.g),cod(T.g)],(@(T.g))`2] by Def10;
    then
A5: (@(T.g))`2=hom(a,g) by XTUPLE_0:1;
    cod(T.g)=Hom(a,cod g ) by A4,Lm1;
    then
A6: cod(@(T.g))=Hom(a,cod g) by Def10;
A7: dom(T.g)=Hom(a,dom g) by A4,Lm1;
    then
A8: dom(@(T.g))=Hom(a,dom g) by Def9;
A9: [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] = @(T.f) by Def21
      .= [[dom(@(T.f)),cod(@(T.f))],(@(T.f))`2] by Th8
      .= [[dom(T.f),cod(@(T.f))],(@(T.f))`2] by Def9
      .= [[dom(T.f),cod(T.f)],(@(T.f))`2] by Def10;
    then
A10: (@(T.f))`2=hom(a,f) by XTUPLE_0:1;
    dom(T.f)=Hom(a,dom f) by A9,Lm1;
    then
A11: dom(@(T.f))=Hom(a,dom f) by Def9;
A12: cod(T.f)=Hom(a,cod f ) by A9,Lm1;
    then
A13: cod(@(T.f))=Hom(a,cod f) by Def10;
    dom(g(*)f) = dom f & cod(g(*)f) = cod g by A3,CAT_1:17;
    hence T.(g(*)f) = [[Hom(a,dom(f)),Hom(a,cod(g))],hom(a,g(*)f)] by Def21
      .= [[Hom(a,dom(f)),Hom(a,cod(g))],hom(a,g)*hom(a,f)] by A3,Th45
      .= (@(T.g))*(@(T.f)) by A3,A10,A11,A13,A5,A8,A6,Def6
      .= (T.g)(*)(T.f) by A3,A12,A7,Th28;
  end;
  hence thesis by CAT_1:61;
end;

theorem Th50:
  Hom(C) c= V implies hom-?(a) is Contravariant_Functor of C,Ens(V )
proof
  assume
A1: Hom(C) c= V;
  then reconsider
  T = hom-?(a) as Function of the carrier' of C, the carrier' of
  Ens V by Lm8;
  now
    thus for c being Object of C ex d being Object of Ens V st T.(id c) = id d
    proof
      let c be Object of C;
      Hom(c,a) in Hom(C);
      then reconsider A = Hom(c,a) as Element of V by A1;
      take d = @A;
      thus thesis by A1,Lm10;
    end;
    thus for f being Morphism of C holds T.(id dom f) = id cod (T.f) & T.(id
    cod f) = id dom (T.f)
    proof
      let f be Morphism of C;
      set b = cod f, c = dom f;
      set g = T.f;
      Hom(b,a) in Hom(C) & Hom(c,a) in Hom(C);
      then reconsider A = Hom(b,a), B = Hom(c,a) as Element of V by A1;
A2:   [[Hom(b,a),Hom(c,a)],hom(f,a)] = @g by Def22
        .= [[dom(@g), cod(@g)],(@g)`2] by Th8
        .= [[dom g, cod(@g)],(@g)`2] by Def9
        .= [[dom g, cod g],(@g)`2] by Def10;
      thus T.(id c) = id @B by A1,Lm10
        .= id cod (T.f) by A2,Lm1;
      thus T.(id b) = id @A by A1,Lm10
        .= id dom (T.f) by A2,Lm1;
    end;
    let f,g be Morphism of C such that
A3: dom g = cod f;
A4: [[Hom(cod g,a),Hom(dom g,a)],hom(g,a)] = @(T.g) by Def22
      .= [[dom(@(T.g)),cod(@(T.g))],(@(T.g))`2] by Th8
      .= [[dom(T.g),cod(@(T.g))],(@(T.g))`2] by Def9
      .= [[dom(T.g),cod(T.g)],(@(T.g))`2] by Def10;
    then
A5: (@(T.g))`2=hom(g,a) by XTUPLE_0:1;
    dom(T.g)=Hom(cod g,a) by A4,Lm1;
    then
A6: dom(@(T.g))=Hom(cod g,a) by Def9;
A7: cod(T.g)=Hom(dom g,a ) by A4,Lm1;
    then
A8: cod(@(T.g))=Hom(dom g,a) by Def10;
A9: [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] = @(T.f) by Def22
      .= [[dom(@(T.f)),cod(@(T.f))],(@(T.f))`2] by Th8
      .= [[dom(T.f),cod(@(T.f))],(@(T.f))`2] by Def9
      .= [[dom(T.f),cod(T.f)],(@(T.f))`2] by Def10;
    then
A10: (@(T.f))`2=hom(f,a) by XTUPLE_0:1;
    cod(T.f)=Hom(dom f,a ) by A9,Lm1;
    then
A11: cod(@(T.f))=Hom(dom f,a) by Def10;
A12: dom(T.f)=Hom(cod f,a) by A9,Lm1;
    then
A13: dom(@(T.f))=Hom(cod f,a) by Def9;
    dom(g(*)f) = dom f & cod(g(*)f) = cod g by A3,CAT_1:17;
    hence T.(g(*)f) = [[Hom(cod(g),a),Hom(dom(f),a)],hom(g(*)f,a)] by Def22
      .= [[Hom(cod(g),a),Hom(dom(f),a)],hom(f,a)*hom(g,a)] by A3,Th46
      .= (@(T.f))*(@(T.g)) by A3,A10,A13,A11,A5,A6,A8,Def6
      .= (T.f)(*)(T.g) by A3,A12,A7,Th28;
  end;
  hence thesis by OPPCAT_1:def 9;
end;

:: hom-bifunctor

theorem Th51:
  Hom(dom f,cod f9) = {} implies Hom(cod f,dom f9) = {}
proof
  assume that
A1: Hom(dom f,cod f9) = {} and
A2: Hom(cod f,dom f9) <> {};
A3: Hom(dom f9,cod f9) <> {} by CAT_1:2;
  Hom(dom f,cod f) <> {} by CAT_1:2;
  then Hom(dom f,dom f9) <> {} by A2,CAT_1:24;
  hence contradiction by A1,A3,CAT_1:24;
end;

definition
  let C,f,g;
  func hom(f,g) -> Function of Hom(cod f,dom g),Hom(dom f,cod g) means
  :Def23:
  for h st h in Hom(cod f,dom g) holds it.h = g(*)h(*)f;
  existence
  proof
    defpred P[set,set] means for h st h = $1 holds $2 = g(*)h(*)f;
    set X = Hom(cod f,dom g), Y = Hom(dom f,cod g);
A1: for x being set st x in X ex y being set st y in Y & P[x,y]
    proof
      let x be set;
A2:   Hom(dom f,cod f) <> {} & f is Morphism of dom f,cod f by CAT_1:2,4;
      assume
A3:   x in X;
      then reconsider h = x as Morphism of cod f,dom g by CAT_1:def 5;
      take g(*)h(*)f;
      Hom(dom g,cod g) <> {} & g is Morphism of dom g,cod g by CAT_1:2,4;
      then
A4:   g(*)h in Hom(cod f,cod g) by A3,CAT_1:23;
      then g(*)h is Morphism of cod f,cod g by CAT_1:def 5;
      hence thesis by A4,A2,CAT_1:23;
    end;
    consider h being Function such that
A5: dom h = X & rng h c= Y and
A6: for x being set st x in X holds P[x,h.x] from FUNCT_1:sch 5(A1);
    Y = {} implies X = {} by Th51;
    then reconsider h as Function of X,Y by A5,FUNCT_2:def 1,RELSET_1:4;
    take h;
    thus thesis by A6;
  end;
  uniqueness
  proof
    set X = Hom(cod f,dom g), Y = Hom(dom f,cod g);
    let h1,h2 be Function of X,Y such that
A7: for h st h in X holds h1.h = g(*)h(*)f and
A8: for h st h in X holds h2.h = g(*)h(*)f;
    now
      let x be set;
      assume
A9:   x in X;
      then reconsider h = x as Morphism of C;
      thus h1.x = g(*)h(*)f by A7,A9
        .= h2.x by A8,A9;
    end;
    hence thesis by FUNCT_2:12;
  end;
end;

theorem Th52:
  [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)] is Element of Maps(Hom(C))
proof
A1: Hom(dom f,cod g) in Hom(C) & Hom(cod f,dom g) in Hom(C);
  Hom(dom f,cod g) = {} implies Hom(cod f,dom g) = {} by Th51;
  hence thesis by A1,Th5;
end;

theorem Th53:
  hom(id a,f) = hom(a,f) & hom(f,id a) = hom(f,a)
proof
A1: cod id a = a;
  now
    Hom(dom f,cod f) <> {} by CAT_1:2;
    then Hom(a,cod f) = {} implies Hom(a,dom f) = {} by CAT_1:24;
    hence
    dom hom(id a,f) = Hom(a,dom f) & dom hom(a,f) = Hom(a,dom f)
    by FUNCT_2:def 1;
    let x be set;
    assume
A2: x in Hom(a,dom f);
    then reconsider g = x as Morphism of C;
A3: dom g = a by A2,CAT_1:1;
A4: cod g = dom f by A2,CAT_1:1;
    thus hom(id a,f).x = f(*)g(*)(id a) by A2,Def23
      .= f(*)(g(*)(id a)) by A1,A3,A4,CAT_1:18
      .= f(*)g by A3,CAT_1:22
      .= hom(a,f).x by A2,Def19;
  end;
  hence hom(id a,f) = hom(a,f) by FUNCT_1:2;
  now
    Hom(dom f,cod f) <> {} by CAT_1:2;
    then Hom(dom f,a) = {} implies Hom(cod f,a) = {} by CAT_1:24;
    hence
    dom hom(f,id a) = Hom(cod f,a) & dom hom(f,a) = Hom(cod f,a)
    by FUNCT_2:def 1;
    let x be set;
    assume
A5: x in Hom(cod f,a);
    then reconsider g = x as Morphism of C;
A6: cod g = a by A5,CAT_1:1;
    thus hom(f,id a).x = (id a)(*)g(*)f by A5,Def23
      .= g(*)f by A6,CAT_1:21
      .= hom(f,a).x by A5,Def20;
  end;
  hence thesis by FUNCT_1:2;
end;

theorem Th54:
  hom(id a,id b) = id Hom(a,b)
proof
  thus hom(id a,id b) = hom(a,id b) by Th53
    .= id Hom(a,b) by Th43;
end;

theorem
  hom(f,g) = hom(dom f,g)*hom(f,dom g)
proof
  now
A1: Hom(dom f,cod g) = {} implies Hom(cod f,dom g) = {} by Th51;
    hence dom hom(f,g) = Hom(cod f,dom g) by FUNCT_2:def 1;
    Hom(dom f,cod f) <> {} by CAT_1:2;
    then Hom(dom f,dom g) = {} implies Hom(cod f,dom g) = {} by CAT_1:24;
    hence
A2: dom(hom(dom f,g)*hom(f,dom g)) = Hom(cod f,dom g) by A1,FUNCT_2:def 1;
    let x be set;
    assume
A3: x in Hom(cod f,dom g);
    then reconsider h = x as Morphism of C;
A4: dom h = cod f by A3,CAT_1:1;
    then
A5: dom(h(*)f) = dom f by CAT_1:17;
A6: cod h = dom g by A3,CAT_1:1;
    then cod(h(*)f) = dom g by A4,CAT_1:17;
    then
A7: h(*)f in Hom(dom f,dom g) by A5;
    thus hom(f,g).x = g(*)h(*)f by A3,Def23
      .= g(*)(h(*)f) by A4,A6,CAT_1:18
      .= hom(dom f,g).(h(*)f) by A7,Def19
      .= hom(dom f,g).((hom(f,dom g)).h) by A3,Def20
      .= (hom(dom f,g)*hom(f,dom g)).x by A2,A3,FUNCT_1:12;
  end;
  hence thesis by FUNCT_1:2;
end;

theorem Th56:
  cod g = dom f & dom g9 = cod f9 implies
    hom(f(*)g,g9(*)f9) = hom(g, g9)*hom(f,f9)
proof
  assume that
A1: cod g = dom f and
A2: dom g9 = cod f9;
A3: dom(g9(*)f9) = dom f9 by A2,CAT_1:17;
A4: cod(f(*)g) = cod f by A1,CAT_1:17;
A5: cod(g9(*)f9) = cod g9 & dom(f(*)g) = dom g by A1,A2,CAT_1:17;
  now
    set h = hom(f(*)g,g9(*)f9), h2 = hom(g,g9), h1 = hom(f,f9);
A6: Hom(dom f,cod f9) = {} implies Hom(cod f,dom f9) = {} by Th51;
A7: Hom(dom g,cod g9) = {} implies Hom(cod g,dom g9) = {} by Th51;
    hence dom h = Hom(cod f,dom f9) by A1,A2,A3,A5,A4,A6,FUNCT_2:def 1;
    thus
A8: dom(h2*h1) = Hom(cod f,dom f9) by A1,A2,A7,A6,FUNCT_2:def 1;
    let x be set;
    assume
A9: x in Hom(cod f,dom f9);
    then reconsider k = x as Morphism of C;
A10: h1.x in Hom(cod g,dom g9) by A1,A2,A9,Th51,FUNCT_2:5;
    then reconsider l = h1.x as Morphism of C;
A11: dom k = cod f by A9,CAT_1:1;
    then
A12: cod(k(*)(f(*)g)) = cod k by A4,CAT_1:17;
A13: cod k = dom f9 by A9,CAT_1:1;
    then
A14: dom(f9(*)k) = dom k by CAT_1:17;
    then
A15: dom (f9(*)k(*)f) = dom f by A11,CAT_1:17;
    cod(f9(*)k) = cod f9 by A13,CAT_1:17;
    then
A16: cod(f9(*)k(*)f) = cod f9 by A11,A14,CAT_1:17;
    thus h.x = (g9(*)f9)(*)k(*)(f(*)g) by A3,A4,A9,Def23
      .= (g9(*)f9)(*)(k(*)(f(*)g)) by A3,A4,A13,A11,CAT_1:18
      .= g9(*)(f9(*)(k(*)(f(*)g))) by A2,A13,A12,CAT_1:18
      .= g9(*)(f9(*)k(*)(f(*)g)) by A4,A13,A11,CAT_1:18
      .= g9(*)(f9(*)k(*)f(*)g) by A1,A11,A14,CAT_1:18
      .= g9(*)(f9(*)k(*)f)(*)g by A1,A2,A15,A16,CAT_1:18
      .= g9(*)l(*)g by A9,Def23
      .= h2.l by A10,Def23
      .= (h2*h1).x by A8,A9,FUNCT_1:12;
  end;
  hence thesis by FUNCT_1:2;
end;

definition
  let C;
  func hom??(C) -> Function of the carrier' of [:C,C:], Maps(Hom(C)) means
  :
  Def24: for
 f,g holds it.[f,g] = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)];
  existence
  proof
    defpred P[set,set] means for f,g st $1=[f,g] holds $2=[[Hom(cod f,dom g),
    Hom(dom f,cod g)],hom(f,g)];
    set X = the carrier' of [:C,C:], Y = Maps(Hom(C));
A1: for x being set st x in X ex y being set st y in Y & P[x,y]
    proof
      let x be set;
      assume x in X;
      then consider f,g such that
A2:   x = [f,g] by DOMAIN_1:1;
      take y = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)];
      y is Element of Y by Th52;
      hence y in Y;
      let f9,g9;
      assume x = [f9,g9];
      then f9 = f & g9 = g by A2,XTUPLE_0:1;
      hence thesis;
    end;
    consider h being Function such that
A3: dom h = X & rng h c= Y and
A4: for x being set st x in X holds P[x,h.x] from FUNCT_1:sch 5(A1);
    reconsider h as Function of X,Y by A3,FUNCT_2:def 1,RELSET_1:4;
    take h;
    thus thesis by A4;
  end;
  uniqueness
  proof
    let h1,h2 be Function of the carrier' of [:C,C:], Maps(Hom(C)) such that
A5: for f,g holds h1.[f,g] = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom
    (f,g)] and
A6: for f,g holds h2.[f,g] = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom (f,g)];
    now
      thus the carrier' of [:C,C:] = [:the carrier' of C,the carrier' of C:];
      let f,g;
      thus h1.(f,g) = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)] by A5
        .= h2.(f,g) by A6;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

theorem Th57:
  hom?-(a) = (curry (hom??(C))).(id a) & hom-?(a) = (curry' (hom?? (C))).(id a)
proof
  reconsider T = hom??(C) as Function of [:the carrier' of C,the carrier' of C
  :],Maps(Hom(C));
  now
    let f;
    thus ((curry T).(id a)).f = T.(id a,f) by FUNCT_5:69
      .= [[Hom(cod id a,dom f),Hom(dom id a,cod f)],hom(id a,f)] by Def24
      .= [[Hom(cod id a,dom f),Hom(dom id a,cod f)],hom(a,f)] by Th53
      .= [[Hom(a,dom f),Hom(dom id a,cod f)],hom(a,f)]
      .= [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)]
      .= (hom?-(a)).f by Def21;
  end;
  hence hom?-(a) = (curry (hom??(C))).(id a) by FUNCT_2:63;
  now
    let f;
    thus ((curry' T).(id a)).f = T.(f,id a) by FUNCT_5:70
      .= [[Hom(cod f,dom id a),Hom(dom f,cod id a)],hom(f,id a)] by Def24
      .= [[Hom(cod f,dom id a),Hom(dom f,cod id a)],hom(f,a)] by Th53
      .= [[Hom(cod f,a),Hom(dom f,cod id a)],hom(f,a)]
      .= [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)]
      .= (hom-?(a)).f by Def22;
  end;
  hence thesis by FUNCT_2:63;
end;

Lm11: Hom(C) c= V implies for d being Object of Ens(V) st d = Hom(a,b) holds (
hom??(C)).[id a,id b] = id d
proof
A1: Hom(a,b) in Hom(C);
  assume Hom(C) c= V;
  then reconsider A = Hom(a,b) as Element of V by A1;
A2: hom(id a,id b) = id A by Th54;
  let d be Object of Ens(V);
  assume d = Hom(a,b);
  hence (hom??(C)).[id a,id b] = id$ @d by A2,Def24
    .= id d by Th29;
end;

theorem Th58:
  Hom(C) c= V implies hom??(C) is Functor of [:C opp,C:],Ens(V)
proof
  assume
A1: Hom(C) c= V;
  then C opp = CatStr (#the carrier of C, the carrier' of C, the Target of C,
the Source of C, ~(the Comp of C)#) & Maps(Hom(C)) c= Maps(V) by
Th7;
  then reconsider T = hom??(C) as Function of the carrier' of [:C opp,C:], the
  carrier' of Ens V by FUNCT_2:7;
  now
    thus for c being Object of [:C opp,C:] ex d being Object of Ens V st T.(id
    c) = id d
    proof
      let c be Object of [:C opp,C:];
      consider a being Object of C opp, b such that
A2:   c = [a,b] by DOMAIN_1:1;
      Hom(opp a,b) in Hom(C);
      then reconsider A = Hom(opp a,b) as Element of V by A1;
      take d = @A;
A3: id opp a = id a by OPPCAT_1:72;

      id c = [id opp a,id b] by A3,A2,CAT_2:31;
      hence thesis by A1,Lm11;
    end;
    thus for fg being Morphism of [:C opp,C:] holds T.(id dom fg) = id dom (T.
    fg) & T.(id cod fg) = id cod (T.fg)
    proof
      let fg be Morphism of [:C opp,C:];
      consider f being (Morphism of C opp), g such that
A4:   fg = [f,g] by DOMAIN_1:1;
      Hom(cod opp f,dom g) in Hom(C) & Hom(dom opp f,cod g) in Hom(C);
      then reconsider
      A=Hom(cod opp f,dom g), B=Hom(dom opp f,cod g) as Element of
      V by A1;
      set h = T.fg;
A5: id opp dom f = id dom f by OPPCAT_1:72;
A6: id opp cod f = id cod f by OPPCAT_1:72;
A7:   [[Hom(cod opp f,dom g),Hom(dom opp f,cod g)],hom(opp f,g)] = @h by A4
,Def24
        .= [[dom(@h), cod(@h)],(@h)`2] by Th8
        .= [[dom h, cod(@h)],(@h)`2] by Def9
         .= [[dom h, cod h],(@h)`2] by Def10;
      thus T.(id dom fg) = T.(id [dom f,dom g]) by A4,CAT_2:28
        .= T.[id dom f,id dom g] by CAT_2:31
        .= id @A by A1,Lm11,A5
        .= id dom (T.fg) by A7,Lm1;
      thus T.(id cod fg) = T.(id [cod f,cod g]) by A4,CAT_2:28
        .= T.[id cod f,id cod g] by CAT_2:31
        .= id @B by A1,Lm11,A6
        .= id cod (T.fg) by A7,Lm1;
    end;
    let ff,gg be Morphism of [:C opp,C:] such that
A8: dom gg = cod ff;
    consider g being (Morphism of C opp), g9 such that
A9: gg = [g,g9] by DOMAIN_1:1;
A10: [[Hom(cod opp g,dom g9),Hom(dom opp g,cod g9)],hom(opp g,g9)] = @(T.
    gg) by A9,Def24
      .= [[dom(@(T.gg)),cod(@(T.gg))],(@(T.gg))`2] by Th8
      .= [[dom(T.gg),cod(@(T.gg))],(@(T.gg))`2] by Def9
      .= [[dom(T.gg),cod(T.gg)],(@(T.gg))`2] by Def10;
    then
A11: (@(T.gg))`2=hom(opp g,g9) by XTUPLE_0:1;
    cod(T.gg)=Hom(dom opp g,cod g9) by A10,Lm1;
    then
A12: cod(@(T.gg))=Hom(dom opp g, cod g9) by Def10;
A13: dom(T.gg)=Hom(cod opp g,dom g9) by A10,Lm1;
    then
A14: dom(@(T.gg))=Hom(cod opp g,dom g9) by Def9;
    consider f being (Morphism of C opp), f9 such that
A15: ff = [f,f9] by DOMAIN_1:1;
A16: [[Hom(cod opp f,dom f9),Hom(dom opp f,cod f9)],hom(opp f,f9)] = @(T.
    ff) by A15,Def24
      .= [[dom(@(T.ff)),cod(@(T.ff))],(@(T.ff))`2] by Th8
      .= [[dom(T.ff),cod(@(T.ff))],(@(T.ff))`2] by Def9
      .= [[dom(T.ff),cod(T.ff)],(@(T.ff))`2] by Def10;
    then
A17: (@(T.ff))`2=hom(opp f,f9) by XTUPLE_0:1;
    dom(T.ff)=Hom(cod opp f,dom f9) by A16,Lm1;
    then
A18: dom(@(T.ff))=Hom(cod opp f,dom f9) by Def9;
A19: cod(T.ff)=Hom(dom opp f,cod f9) by A16,Lm1;
    then
A20: cod(@(T.ff))=Hom(dom opp f, cod f9) by Def10;
A21: cod ff = [cod f,cod f9] by A15,CAT_2:28;
A22: dom gg = [dom g,dom g9] by A9,CAT_2:28;
    then
A23: cod opp g = dom opp f by A8,A21,XTUPLE_0:1;
    then
A24: dom((opp f)(*)(opp g)) = dom opp g & cod((opp f)(*)(opp g)) = cod opp f
    by CAT_1:17;
A25: dom g = cod f by A8,A22,A21,XTUPLE_0:1;
A26: dom g9 = cod f9 by A8,A22,A21,XTUPLE_0:1;
    then
A27: dom(g9(*)f9) = dom f9 & cod(g9(*)f9) = cod g9 by CAT_1:17;
    thus T.(gg(*)ff)
       = T.([opp (g(*)f),g9(*)f9]) by A8,A15,A9,CAT_2:30
      .= T.([(opp f)(*)(opp g),g9(*)f9]) by A25,OPPCAT_1:18
      .= [[Hom(cod((opp f)(*)(opp g)),dom(g9(*)f9)),
                  Hom(dom((opp f)(*)(opp g)),
    cod(g9(*)f9))], hom((opp f)(*)(opp g),g9(*)f9)] by Def24
      .= [[Hom(cod opp f,dom f9),Hom(dom opp g,cod g9)], hom(opp g,g9)*hom(
    opp f,f9)] by A23,A26,A27,A24,Th56
      .= (@(T.gg))*(@(T.ff)) by A17,A18,A20,A11,A14,A12,A23,A26,Def6
      .= (T.gg)(*)(T.ff) by A19,A13,A23,A26,Th28;
  end;
  hence thesis by CAT_1:61;
end;

definition
  let V,C,a;
  assume
A1: Hom(C) c= V;
  func hom?-(V,a) -> Functor of C,Ens(V) equals
  :Def25:
  hom?-(a);
  coherence by A1,Th49;
  func hom-?(V,a) -> Contravariant_Functor of C,Ens(V) equals
  :Def26:
  hom-?(a);
  coherence by A1,Th50;
end;

definition
  let V,C;
  assume
A1: Hom(C) c= V;
  func hom??(V,C) -> Functor of [:C opp,C:],Ens(V) equals
  :Def27:
  hom??(C);
  coherence by A1,Th58;
end;

theorem
  Hom(C) c= V implies (hom?-(V,a)).f = [[Hom(a,dom f),Hom(a,cod f)],hom(
  a, f ) ]
proof
  assume Hom(C) c= V;
  hence (hom?-(V,a)).f = (hom?-(a)).f by Def25
    .= [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] by Def21;
end;

theorem
  Hom(C) c= V implies (Obj (hom?-(V,a))).b = Hom(a,b)
proof
  assume
A1: Hom(C) c= V;
  Hom(a,b) in Hom(C);
  then reconsider A = Hom(a,b) as Element of V by A1;
  set d = @A;
  (hom?-(V,a)).(id b) = (hom?-(a)).(id b) by A1,Def25
    .= id d by A1,Lm9;
  hence thesis by CAT_1:67;
end;

theorem
  Hom(C) c= V implies (hom-?(V,a)).f = [[Hom(cod f,a),Hom(dom f,a)],hom(
  f, a ) ]
proof
  assume Hom(C) c= V;
  hence (hom-?(V,a)).f = (hom-?(a)).f by Def26
    .= [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] by Def22;
end;

theorem
  Hom(C) c= V implies (Obj (hom-?(V,a))).b = Hom(b,a)
proof
  assume
A1: Hom(C) c= V;
  Hom(b,a) in Hom(C);
  then reconsider A = Hom(b,a) as Element of V by A1;
  set d = @A;
  (hom-?(V,a)).(id b) = (hom-?(a)).(id b) by A1,Def26
    .= id d by A1,Lm10;
  hence thesis by OPPCAT_1:30;
end;

theorem
  Hom(C) c= V implies hom??(V,C).[f opp,g] = [[Hom(cod f,dom g),Hom(dom
  f,cod g)],hom(f,g)]
proof
  assume
A1: Hom(C) c= V;
  thus (hom??(V,C)).[f opp,g] = (hom??(C)).[f,g] by A1,Def27
    .= [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)] by Def24;
end;

theorem
  Hom(C) c= V implies (Obj (hom??(V,C))).[a opp,b] = Hom(a,b)
proof
  assume
A1: Hom(C) c= V;
  Hom(a,b) in Hom(C);
  then reconsider A = Hom(a,b) as Element of V by A1;
A2: id(a opp) = id a by OPPCAT_1:71;
  set d = @A;
  (hom??(V,C)).(id[a opp,b]) = (hom??(V,C)).[id(a opp),id b] by CAT_2:31
    .= (hom??(C)).[id a,id b] by A1,Def27,A2
    .= id d by A1,Lm11;
  hence thesis by CAT_1:67;
end;

theorem
  Hom(C) c= V implies hom??(V,C)?-(a opp) = hom?-(V,a)
proof
  assume
A1: Hom(C) c= V;
A2: id(a opp) = id a by OPPCAT_1:71;
  thus hom??(V,C)?-(a opp)
     = (curry hom??(C)).(id a) by A1,Def27,A2
    .= hom?-(a) by Th57
    .= hom?-(V,a) by A1,Def25;
end;

theorem
  Hom(C) c= V implies hom??(V,C)-?a = hom-?(V,a)
proof
  assume
A1: Hom(C) c= V;
  hence hom??(V,C)-?a = (curry' hom??(C)).(id a) by Def27
    .= hom-?(a) by Th57
    .= hom-?(V,a) by A1,Def26;
end;