The Mizar article:

Category Ens

by
Czeslaw Bylinski

Received August 1, 1991

Copyright (c) 1991 Association of Mizar Users

MML identifier: ENS_1
[ MML identifier index ]


environ

 vocabulary FUNCT_2, TARSKI, FRAENKEL, FUNCT_1, BOOLE, MCART_1, RELAT_1, CAT_1,
      PARTFUN1, QC_LANG1, CLASSES2, FUNCOP_1, FUNCT_4, CAT_2, OPPCAT_1,
      FUNCT_5, ENS_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, DOMAIN_1, RELAT_1,
      FUNCT_1, FUNCT_2, PARTFUN1, FUNCT_4, FUNCT_5, FRAENKEL, CLASSES2,
      FUNCOP_1, CAT_1, CAT_2, OPPCAT_1;
 constructors DOMAIN_1, CLASSES2, CAT_2, OPPCAT_1, PARTFUN1, MEMBERED,
      XBOOLE_0;
 clusters RELAT_1, FUNCT_1, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, FUNCT_2,
      XBOOLE_0;
 requirements SUBSET, BOOLE;
 definitions TARSKI, FUNCT_1, CAT_1, CAT_2;
 theorems TARSKI, ENUMSET1, ZFMISC_1, MCART_1, DOMAIN_1, FUNCT_1, FUNCT_2,
      PARTFUN1, FUNCOP_1, FUNCT_4, FRAENKEL, CLASSES2, CAT_1, CAT_2, OPPCAT_1,
      GRFUNC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1;
 schemes FUNCT_2, PARTFUN1, COMPTS_1;

begin :: Mappings

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

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

definition let V;
  cluster Funcs(V) -> functional non empty;
   coherence
 proof set F = { Funcs(A,B): not contradiction};
A1:Funcs V = union F by Def1;
  consider A;
    id A in Funcs(A,A) & Funcs(A,A) in F by FUNCT_2:12;
  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
A2:  f in C and
A3:  C in F by TARSKI:def 4;
     ex A,B st C = Funcs(A,B) by A3;
   hence f is Function by A2,FUNCT_2:121;
  end;
  hence thesis by A1,FRAENKEL:def 1;
 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};
A1:  Funcs V = union F by Def1;
  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
A2:  f in C and
A3:  C in F by A1,TARSKI:def 4;
    consider A,B such that
A4:  C = Funcs(A,B) by A3;
    take A,B;
    thus thesis by A2,A4,FUNCT_2:14,121;
   end;
  given A,B such that
A5:  (B={} implies A={}) & f is Function of A,B;
    f in Funcs(A,B) & Funcs(A,B) in F by A5,FUNCT_2:11;
  hence thesis by A1,TARSKI:def 4;
 end;

theorem
     Funcs(A,B) c= Funcs(V)
 proof let x be set;
  assume
    x in Funcs(A,B);
  then (B={} implies A={}) & x is Function of A,B by FUNCT_2:14,121;
  hence thesis by 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,f' for Element of Funcs(V);

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

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

reserve m,m1,m2,m3,m' 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 Maps V;
  then m in { [[A,B],f]: (B={} implies A={}) & f is Function of A,B} by Def2;
  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;
  then [[A,B],f] in {[[A',B'],f']:(B'={} implies A'={}
) & f' is Function of A',B'}
   by A1;
  hence thesis by Def2;
 end;

theorem
     Maps V c= [:[:V,V:],Funcs V:]
 proof let m be set;
  assume m in Maps V;
  then m in { [[A,B],f]: (B={} implies A={}) & f is Function of A,B} by Def2;
  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 x in { [[A,B],f]
      where A is Element of W, B is Element of W, f is Element of Funcs(W)
         : (B={} implies A={}) & f is Function of A,B }
   by Def2;
  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;
  then x in {[[A',B'],f']:(B'={} implies A'={}
) & f' is Function of A',B'} by A1;
  hence thesis by Def2;
 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 ZFMISC_1:33;
  hence thesis by ZFMISC_1:33;
 end;

definition let V be non empty set, m be Element of Maps V;
  cluster m`2 -> Function-like Relation-like;
  coherence
 proof
  consider f be Element of Funcs(V),
           A,B be Element of V such that
A1: m = [[A,B],f] and (B = {} implies A = {}) and
A2: f is Function of A,B by Th4;
  thus thesis by A1,A2,MCART_1:7;
 end;
end;

definition let V,m;
 canceled;

 func dom m -> Element of V equals
:Def4:  m`1`1;
  coherence
 proof
  consider f,A,B such that
A1: m = [[A,B],f] and (B = {} implies A = {}) & 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
:Def5:  m`1`2;
  coherence
 proof
  consider f,A,B such that
A2: m = [[A,B],f] and (B = {} implies A = {}) & 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] and (B = {} implies A = {}) & f is Function of A,B by Th4;
     dom m = m`1`1 & cod m = m`1`2 & [A,B] = m`1 by A1,Def4,Def5,MCART_1:7;
   then m`1 = [dom m,cod m] & m`2 = m`2 by MCART_1:8;
   hence thesis by A1,MCART_1:8;
 end;

Lm2: m`2 = m'`2 & dom m = dom m' & cod m = cod m' implies m = m'
 proof m = [[dom m,cod m],m`2] & m' = [[dom m',cod m'],m'`2] by Th8;
  hence thesis;
 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;
    m = [[dom m,cod m],m`2] by Th8;
  then f = m`2 & A = dom m & B = cod m by A1,Lm1,ZFMISC_1:33;
  hence thesis by A2;
 end;

Lm3: dom m`2 = dom m & rng m`2 c= cod m
 proof (cod m <> {} or dom m = {}) & m`2 is Function of dom m,cod m by Th9;
  hence thesis by FUNCT_2:def 1,RELSET_1:12;
 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 f',A',B' such that
A1:  [[A,B],f] = [[A',B'],f'] and
A2:  (B' = {} implies A' = {}) & f' is Function of A',B' by Th4;
     f = f' & A = A' & B = B' by A1,Lm1,ZFMISC_1:33;
   hence thesis by A2;
 end;

definition let V,A;
  func id$ A -> Element of Maps V equals
:Def6:  [[A,A],id A];
  coherence
 proof A = {} implies A = {};
  hence thesis by Th5;
 end;
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] = id$ A by Th8
 .= [[A,A],id A] by Def6;
  hence thesis by Lm1,ZFMISC_1:33;
 end;

definition let V,m1,m2;
  assume A1: cod m1 = dom m2;
   func m2*m1 -> Element of Maps V equals
:Def7:  [[dom m1,cod m2],m2`2*m1`2];
  coherence
 proof
A2:  (cod m1 <> {} or dom m1 = {}) & m1`2 is Function of dom m1,cod m1 &
      (cod m2 <> {} or dom m2 = {}) & 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,FUNCT_2:19;
  hence thesis by A1,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 Def7
    .= [[dom(m2*m1),cod(m2*m1)],(m2*m1)`2] by Th8;
  hence thesis by Lm1,ZFMISC_1:33;
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;
    (m2*m1)`2 = m2`2*m1`2 & dom(m2*m1) = dom m1 & cod(m2*m1) = cod m2 &
  (m3*m2)`2 = m3`2*m2`2 & dom(m3*m2) = dom m2 & cod(m3*m2) = cod m3
  by A1,A2,Th12;
  then (m3*(m2*m1))`2 = m3`2*(m2`2*m1`2) &
         dom(m3*(m2*m1)) = dom m1 & cod(m3*(m2*m1)) = cod m3 &
       ((m3*m2)*m1)`2 = (m3`2*m2`2)*m1`2 &
         dom((m3*m2)*m1) = dom m1 & cod((m3*m2)*m1) = cod m3 &
       m3`2*(m2`2*m1`2) = (m3`2*m2`2)*m1`2 by A1,A2,Th12,RELAT_1:55;
  hence thesis by Lm2;
 end;

theorem Th14:
   m*(id$ dom m) = m & (id$ cod m)*m = m
 proof set i1 = id$ dom m, i2 = id$ cod m;
A1:  (cod m <> {} or dom m = {}) & m`2 is Function of dom m,cod m by Th9;
    cod i1 = dom m by Th11;
  then dom m`2 = dom m &
   i1`2 = id dom m & dom i1 = dom m &
    (m*i1)`2 = m`2*i1`2 & dom(m*i1) = dom i1 & cod(m*i1) = cod m &
     m`2*(id dom m`2) = m`2 by A1,Th11,Th12,FUNCT_1:42,FUNCT_2:def 1;
  hence m*i1 = m by Lm2;
    dom i2 = cod m & rng m`2 c= cod m by A1,Th11,RELSET_1:12;
  then i2`2 = id cod m & cod i2 = cod m &
   (i2*m)`2 = i2`2*m`2 & dom(i2*m) = dom m & cod(i2*m) = cod i2 &
    (id cod m)*m`2 = m`2 by Th11,Th12,RELAT_1:79;
  hence thesis by Lm2;
 end;

definition let V,A,B;
 func Maps(A,B) -> set equals
:Def8:  { [[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) &
   Maps(A,B) = {[[A,B],f'] where f' is Element of Funcs V: [[A,B],f'] in
 Maps V}
    by Def8,Th1,Th5;
  hence thesis;
 end;

theorem Th16:
   m in Maps(A,B) implies m = [[A,B],m`2]
 proof
A1: Maps(A,B) = { [[A,B],f] where f is Element of Funcs V: [[A,B],f] in
 Maps V }
     by Def8;
  assume m in Maps(A,B);
  then A2: ex f being Element of Funcs(V) st m = [[A,B],f] &
 [[A,B],f] in Maps(V) by A1;
    m = [[dom m,cod m],m`2] by Th8;
  hence thesis by A2,ZFMISC_1:33;
 end;

theorem Th17:
   Maps(A,B) c= Maps V
 proof let z be set;
A1:  Maps(A,B) = {[[A,B],f] where f is Element of Funcs V: [[A,B],f] in Maps V}
      by Def8;
  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)
    by A1;
  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 let f be Function such that
A1:  [[A,B],f] in Maps(A,B);
    Maps(A,B) c= Maps V by Th17;
  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;
       z in Maps(A,B) & Maps(A,B) in M by A1,Th15;
     hence thesis by TARSKI:def 4;
    end;
   assume z in union M;
   then consider C being set such that
A2:  z in C and
A3:  C in M by TARSKI:def 4;
   consider A,B such that
A4:  C = Maps(A,B) by A3;
      Maps(A,B) = { [[A,B],f] where f is Element of Funcs V: [[A,B],f] in
 Maps V }
     by Def8;
   then ex f being Element of Funcs(V) st z = [[A,B],f] & [[A,B],f] in Maps(V)
     by A2,A4;
   hence z in Maps(V);
  end;
  hence thesis by TARSKI:2;
 end;

theorem Th19:
   m in Maps(A,B) iff dom m = A & cod m = B
 proof
  thus m in Maps(A,B) implies dom m = A & cod m = B
   proof assume m in Maps(A,B);
    then m = [[A,B],m`2] & m = [[dom m,cod m],m`2] by Th8,Th16;
    hence thesis by Lm1;
   end;
    (cod m <> {} or dom m = {}) & m`2 is Function of dom m,cod m by Th9;
  then [[dom m,cod m],m`2] in Maps(dom m,cod m) by 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 m = [[A,B],m`2] by Th16;
   then (B = {} implies A = {}) & m`2 is Function of A,B by A1,Lm4;
   hence thesis by FUNCT_2:11;
 end;

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

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

begin  :: Category Ens

definition let V;
  func fDom V -> Function of Maps V,V means
:Def10: 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 LambdaD;
    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:113;
 end;

  func fCod V -> Function of Maps V,V means
:Def11: 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 LambdaD;
    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:113;
 end;

  func fComp V -> PartFunc of [:Maps V,Maps V:],Maps V means
:Def12:
   (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,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;
A6:   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 P[x,y,z1] & P[x,y,z2];
      then z1 = m2*m1 & z2 = m2*m1;
      hence thesis;
     end;
   consider h being PartFunc of [:Maps(V),Maps(V):],Maps(V) such that
A7:  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
A8:   for x,y being set st [x,y] in dom h holds P[x,y,h.[x,y]]
    from PartFuncEx2(A5,A6);
   take h;
   thus
A9:   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 A7;
       hence thesis;
      end;
     assume dom m2 = cod m1;
     then P[m2,m1,m2*m1];
     hence thesis by A7;
    end;
   let m2,m1;
   assume dom m2 = cod m1;
   then [m2,m1] in dom h by A9;
   hence thesis by A8;
  end;
 uniqueness
  proof let h1,h2 be PartFunc of [:Maps V,Maps V:],Maps V such that
A10:  for m2,m1 holds [m2,m1] in dom h1 iff dom m2 = cod m1 and
A11:  for m2,m1 st dom m2 = cod m1 holds h1.[m2,m1] = m2*m1 and
A12:  for m2,m1 holds [m2,m1] in dom h2 iff dom m2 = cod m1 and
A13:  for m2,m1 st dom m2 = cod m1 holds h2.[m2,m1] = m2*m1;
      now
     thus
A14:     dom h1 c= [:Maps V,Maps V:] by RELSET_1:12;
     thus
A15:     dom h2 c= [:Maps V,Maps V:] by RELSET_1:12;
     let x,y be set;
     thus [x,y] in dom h1 implies [x,y] in dom h2
      proof assume
A16:      [x,y] in dom h1;
       then reconsider m2 = x, m1 = y as Element of Maps V by A14,ZFMISC_1:106;
         dom m2 = cod m1 by A10,A16;
       hence thesis by A12;
      end;
     assume
A17:    [x,y] in dom h2;
     then reconsider m2 = x, m1 = y as Element of Maps V by A15,ZFMISC_1:106;
       dom m2 = cod m1 by A12,A17;
     hence [x,y] in dom h1 by A10;
    end;
then A18:   dom h1 = dom h2 by ZFMISC_1:110;
      now let m be Element of [:Maps V,Maps V:];
     assume
A19:    m in dom h1;
     consider m2,m1 such that
A20:    m = [m2,m1] by DOMAIN_1:9;
       dom m2 = cod m1 by A10,A19,A20;
     then h1.[m2,m1] = m2*m1 & h2.[m2,m1] = m2*m1 by A11,A13;
     hence h1.m = h2.m by A20;
    end;
   hence thesis by A18,PARTFUN1:34;
  end;

  func fId V -> Function of V,Maps V means
:Def13:  for A holds it.A = id$ A;
  existence
  proof
    deffunc F(Element of V) = id$ $1;
    ex F being Function of V, Maps V st for A holds F.A = F(A) from LambdaD;
    hence thesis;
  end;
 uniqueness
  proof let h1,h2 be Function of V,Maps V such that
A21: for A holds h1.A = id$ A and
A22: for A holds h2.A = id$ A;
     now let A; thus h1.A = id$ A by A21 .= h2.A by A22; end;
   hence thesis by FUNCT_2:113;
  end;
end;

definition let V;
 func Ens(V) -> CatStr equals
:Def14:  CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #);
  coherence;
end;

theorem Th21:
   CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) is Category
 proof
  set M = Maps V, d = fDom V, c = fCod V, p = fComp V, i = fId V;
    now
   thus for f,g being Element of M holds [g,f] in dom(p) iff d.g=c.f
    proof let f,g be Element of M;
        d.g = dom g & c.f = cod f by Def10,Def11;
      hence thesis by Def12;
    end;
   thus 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 such that
A1:   d.g=c.f;
       d.g = dom g & c.f = cod f by Def10,Def11;
     then dom(g*f) = dom f & cod(g*f) = cod g & p.[g,f] = g*f &
      d.f = dom f & c.g = cod g by A1,Def10,Def11,Def12,Th12;
     hence thesis by Def10,Def11;
    end;
   thus for f,g,h being Element of M
     st d.h = c.g & d.g = c.f holds p.[h,p.[g,f]] = p.[p.[h,g],f]
    proof let f,g,h be Element of M such that
A2:    d.h = c.g and
A3:    d.g = c.f;
A4:    dom h = d.h & cod g = c.g & dom g = d.g & cod f = c.f by Def10,Def11;
then A5:    cod(g*f) = dom h & dom(h*g) = dom g by A2,A3,Th12;
     thus p.[h,p.[g,f]]
        = p.[h,g*f] by A3,A4,Def12
       .= h*(g*f) by A5,Def12
       .= (h*g)*f by A2,A3,A4,Th13
       .= p.[h*g,f] by A3,A4,A5,Def12
       .= p.[p.[h,g],f] by A2,A4,Def12;
    end;
   let b be Element of V;
A6:   i.b = id$ b & dom id$ b = b & cod id$ b = b by Def13,Th11;
   hence d.(i.b) = b & c.(i.b) = b by Def10,Def11;
   thus for f being Element of M st c.f=b holds p.[i.b,f] = f
    proof let f be Element of M such that
A7:     c.f = b;
A8:    cod f = c.f by Def11;
     then (id$ b)*f = f by A7,Th14;
     hence thesis by A6,A7,A8,Def12;
    end;
   let g be Element of M such that
A9:    d.g=b;
A10:    dom g = d.g by Def10;
   then g*(id$ b) = g by A9,Th14;
   hence p.[g,i.b] = g by A6,A9,A10,Def12;
  end;
  hence thesis by CAT_1:def 8;
 end;

definition let V;
 cluster Ens(V) -> strict Category-like;
  coherence
 proof Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
  hence thesis by Th21;
 end;
end;

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

theorem Th22:
   A is Object of Ens(V)
 proof Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
  hence thesis;
 end;

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

theorem Th23:
   a is Element of V
 proof Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
  hence thesis;
 end;

definition let V,a;
 func @a -> Element of V equals
:Def16:  a;
  coherence by Th23;
end;

Lm6: @@A = A & @@a = a
 proof
  thus @@A = @A by Def16 .= A by Def15;
  thus @@a = @a by Def15 .= a by Def16;
 end;

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

theorem Th24:
   m is Morphism of Ens(V)
 proof Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
  hence thesis;
 end;

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

theorem Th25:
   f is Element of Maps(V)
 proof Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
  hence thesis;
 end;

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

Lm7: @@m = m & @@f = f
 proof
  thus @@m = @m by Def18 .= m by Def17;
  thus @@f = @f by Def17 .= f by Def18;
 end;

theorem Th26:
   dom f = dom(@f) & cod f = cod(@f)
 proof
A1:  Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
  hence dom(@f) = (the Dom of Ens(V)).@f by Def10
             .= (the Dom of Ens(V)).f by Def18
             .= dom f by CAT_1:def 2;
  thus cod(@f) = (the Cod of Ens(V)).@f by A1,Def11
             .= (the Cod of Ens(V)).f by Def18
             .= cod f by CAT_1:def 3;
 end;

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);
       dom(f) = a & cod(f) = b by A1,CAT_1:18;
     then dom(@f) = a & cod(@f) = b by Th26;
     then dom(@f) = @a & cod(@f) = @b by Def16;
     then @f in Maps(@a,@b) by Th19;
     hence thesis by Def18;
    end;
   assume
A2:   x in Maps(@a,@b);
     Maps(@a,@b) c= Maps V by Th17;
   then reconsider m = x as Element of Maps V by A2;
     dom(m) = @a & cod(m) = @b by A2,Th19;
   then dom(m) = a & cod(m) = b by Def16;
   then dom(@@m) = a & cod(@@m) = b by Lm7;
   then dom(@m) = a & cod(@m) = b by Th26;
   then @m in Hom(a,b) by CAT_1:18;
   hence x in Hom(a,b) by Def17;
  end;
  hence thesis by TARSKI:2;
 end;

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

theorem Th28:
   dom g = cod f implies g*f = (@g)*(@f)
 proof assume
A1:  dom g = cod f;
A2:  Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
    dom(@g) = cod f by A1,Th26;
then A3:  dom(@g) = cod(@f) by Th26;
  thus g*f = (the Comp of Ens(V)).[g,f] by A1,CAT_1:41
          .= (the Comp of Ens(V)).[@g,f] by Def18
          .= (fComp V).[@g,@f] by A2,Def18
          .= (@g)*(@f) by A3,Def12;
 end;

theorem Th29:
   id a = id$(@a)
 proof
A1:  Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
  thus id a = (the Id of Ens(V)).a by CAT_1:def 5
           .= (fId V).(@a) by A1,Def16
           .= id$(@a) by Def13;
 end;

theorem
     a = {} implies a is initial
 proof assume a = {};
then A1:  @a = {} by Def16;
  let b;
  set m = [[@a,@b],{}];
    {} is Function of @a,@b by A1,FUNCT_2:55,RELAT_1:60;
then A2:  m in Maps(@a,@b) by A1,Th15;
    Maps(@a,@b) <> {} by A1,Th15;
  hence
A3:  Hom(a,b)<>{} by Th27;
    m in Hom(a,b) by A2,Th27;
  then reconsider f = m as Morphism of a,b by CAT_1:def 7;
  take f;
  let g be Morphism of a,b;
    g in Hom(a,b) by A3,CAT_1:def 7;
then A4:  g in Maps(@a,@b) by Th27;
    Maps(@a,@b) c= Maps V by Th17;
  then reconsider m, m' = g as Element of Maps(V) by A2,A4;
A5:  m' = [[@a,@b],m'`2] by A4,Th16;
    m = [[dom m,cod m],m`2] by Th8;
  then m`2 = {} & m'`2 is Function of @a,@b by A4,A5,Lm4,ZFMISC_1:33;
  hence thesis by A1,A5,PARTFUN1:57;
 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) <> {} & b = {} by Def15,CAT_1:def 16;
  then Funcs(@a,@b) <> {} & @b = {} by Def16,Lm8;
  then @a = {} by FUNCT_2:14;
  hence thesis by Def16;
 end;

theorem
     for W being Universe, a being Object of Ens(W) st a is initial
    holds a = {}
 proof let W be Universe, a be Object of Ens(W);
    {} in W by CLASSES2:62; hence thesis by Th31;
 end;

theorem
     (ex x being set st a = {x}) implies a is terminal
 proof given x being set such that
A1:  a = {x};
A2:  @a = {x} by A1,Def16;
  let b;
  consider h being Function of @b,@a;
  set m = [[@b,@a],h];
A3:  m in Maps(@b,@a) by A2,Th15;
  then m in Hom(b,a) by Th27;
  then reconsider f = m as Morphism of b,a by CAT_1:def 7;
  thus
A4:  Hom(b,a)<>{} by A3,Th27;
  take f;
  let g be Morphism of b,a;
    g in Hom(b,a) by A4,CAT_1:def 7;
then A5:  g in Maps(@b,@a) by Th27;
    Maps(@b,@a) c= Maps V by Th17;
  then reconsider m, m' = g as Element of Maps(V) by A3,A5;
A6:  m' = [[@b,@a],m'`2] by A5,Th16;
    m = [[dom m,cod m],m`2] by Th8;
  then m`2 = h & m'`2 is Function of @b,@a by A5,A6,Lm4,ZFMISC_1:33;
  hence thesis by A2,A6,FUNCT_2:66;
 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;
A3:
  now assume
A4: @a = {};
     now
     consider C being set such that
A5:    C in V and
A6:    C <> {} by A1,ZFMISC_1:41;
     reconsider C as Element of V by A5;
     set b = @C;
       Hom(b,a) <> {} & b <> {} by A2,A6,Def15,CAT_1:def 15;
     then Funcs(@b,@a) <> {} & @b <> {} by Def16,Lm8;
     hence contradiction by A4,FUNCT_2:14;
   end;
   hence contradiction;
  end;
  consider x being Element of @a;
    now assume a <> {x};
   then @a <> {x} by Def16;
   then consider y being set such that
A7:   y in @a and
A8:   y <> x by A3,ZFMISC_1:41;
    deffunc F(set) = x;
    deffunc G(set) = y;
A9: for z being set st z in @a holds F(z) in @a;
    consider fx being Function of @a,@a such that
A10:   for z being set st z in @a holds fx.z = F(z) from Lambda1(A9);
A11:    for z being set st z in @a holds G(z) in @a by A7;
    consider fy being Function of @a,@a such that
A12:   for z being set st z in @a holds fy.z = G(z) from Lambda1(A11);
     @a = {} implies @a = {};
then A13:    ([[@a,@a],fx]) in Maps(@a,@a) & ([[@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 A13;
     m1 in Hom(a,a) & m2 in Hom(a,a) by A13,Th27;
   then (@m1) in Hom(a,a) & (@m2) in Hom(a,a) by Def17;
   then reconsider f = @m1,g = @m2 as Morphism of a,a by CAT_1:def 7;
   consider h being Morphism of a,a such that
A14:   for h' being Morphism of a,a holds h = h' by A2,CAT_1:def 15;
     now thus f = h by A14 .= g by A14;
    thus f = [[@a,@a],fx] & g = [[@a,@a],fy] by Def17;
      fx.y = x & fy.y = y by A7,A10,A12;
    hence fx <> fy by A8;
   end;
   hence contradiction by ZFMISC_1:33;
  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 assume
A1:    W = {{}};
     {} in W by CLASSES2:62;
   then {{}} in W by CLASSES2:63;
   hence contradiction by A1;
  end;
  hence thesis by Th34;
 end;

theorem
     f is monic iff (@f)`2 is one-to-one
 proof set m = @f;
  thus f is monic implies (@f)`2 is one-to-one
   proof assume
A1:  f is monic;
    set A = dom (@f)`2;
    let x1,x2  be set such that
A2:   x1 in A & x2 in A and
A3:   (@f)`2.x1 = (@f)`2.x2;
A4:    A = dom(@f) by Lm3;
    then reconsider A as Element of V;
    reconsider fx1 = A --> x1, fx2 = A --> x2 as Function of A,A
      by A2,FUNCOP_1:57;
    reconsider m1 = [[A,A],fx1],m2 = [[A,A],fx2] as Element of Maps(V) by A2,
Th5;
    set f1 = @m1, f2 = @m2;
A5:   m1 = [[dom m1,cod m1],m1`2] & m2 = [[dom m2,cod m2],m2`2] by Th8;
    then dom m1 = A & dom m2 = A & cod m1 = A & cod m2 = A by Lm1;
then A6:   dom(@f1) = A & dom(@f2) = A & cod(@f1) = A & cod(@f2) = A
     by Lm7;
then A7:    dom f1 = A & dom f2 = A & cod f1 = A & cod f2 = A & dom f = A
     by A4,Th26;
    set h1 = (@f)`2*(@f1)`2, h2 = (@f)`2*(@f2)`2;
    set ff1 = (@f)*(@f1), ff2 = (@f)*(@f2);
       now
A8:   (ff1)`2 = h1 & dom(ff1) = dom(@f1) & cod(ff1) = cod(@f) &
       (ff2)`2 = h2 & dom(ff2) = dom(@f2) & cod(ff2) = cod(@f) by A4,A6,Th12;
      hence ff1=[[dom(@f1),cod(@f)],h1] & ff2=[[dom(@f2),cod(@f)],h2] by Th8;
        now
       thus
A9:      dom(h1) = A & dom(h2) = A by A6,A8,Lm3;
       let x be set;
       assume
A10:      x in A;
         fx1 = m1`2 & fx2 = m2`2 by A5,ZFMISC_1:33;
       then fx1 = (@f1)`2 & fx2 =(@f2)`2 by Lm7;
       then (@f1)`2.x = x1 & (@f2)`2.x = x2 by A10,FUNCOP_1:13;
       then h1.x = (@f)`2.x1 & h2.x = (@f)`2.x2 by A9,A10,FUNCT_1:22;
       hence h1.x = h2.x by A3;
      end;
      hence h1 = h2 by FUNCT_1:9;
     end;
    then ff1 = ff2 & f*(f1) = ff1 & f*(f2) = ff2 by A6,A7,Th28;
    then f1 = f2 & @m1 = m1 & @m2 = m2 by A1,A7,Def17,CAT_1:def 10;
    then fx1 = fx2 by ZFMISC_1:33;
    hence x1 = fx2.x1 by A2,FUNCOP_1:13 .= x2 by A2,FUNCOP_1:13;
   end;
  assume
A11:  m`2 is one-to-one;
  let f1,f2 such that
A12:  dom f1 = dom f2 and
A13:  cod f1 = dom f & cod f2 = dom f and
A14:  f*f1 = f*f2;
   set m1 = @f1, m2 = @f2;
A15:  dom m1 = dom f1 & dom m2 = dom f2 & cod m1 = cod f1 & cod m2 = cod f2 &
      dom m = dom f by Th26;
   then m*m1 = f*f1 & m*m2 = f*f2 &
    m*m1 = [[dom m1,cod m],m`2*m1`2] & m*m2 = [[dom m2,cod m],m`2*m2`2]
     by A13,Def7,Th28;
   then dom m1`2 = dom f1 & dom m2`2 = dom f2 & dom m`2 = dom f &
     rng m1`2 c= cod f1 & rng m2`2 c= cod f2 & (m`2)*(m1`2) = (m`2)*(m2`2)
      by A14,A15,Lm3,ZFMISC_1:33;
   then m1`2 = m2`2 & m1=[[dom m1,cod m1],m1`2] & m2=[[dom m2,cod m2],m2`2]
     by A11,A12,A13,Th8,FUNCT_1:49;
   hence f1 = m2 by A12,A13,A15,Def18 .= f2 by Def18;
 end;

theorem Th37:
   f is epi & (ex A st ex x1,x2 being set st x1 in A & x2 in A & x1 <> x2)
    implies @f is_a_surjection
 proof
  assume
A1:  f is epi;
  given B being Element of V, x1,x2 being set such that
A2:  x1 in B & x2 in B and
A3:  x1 <> x2;
A4:  rng (@f)`2 c= cod(@f) by Lm3;
    cod(@f) c= rng (@f)`2
   proof let x be set;
    set A = cod(@f);
    assume that
A5:   x in A and
A6:   not x in rng (@f)`2;
    reconsider g1 = A --> x1 as Function of A,B by A2,FUNCOP_1:57;
    set h = {x} --> x2, g2 = g1 +* h;
A7:  x in {x} by TARSKI:def 1;
A8:   dom g1 = A & dom h = {x} by FUNCOP_1:19;
then A9:   dom g2 = A \/ {x} by FUNCT_4:def 1 .= A by A5,ZFMISC_1:46;
      rng g1 = {x1} & rng h = {x2} by A5,FUNCOP_1:14;
    then rng g2 c= {x1} \/ {x2} by FUNCT_4:18;
    then rng g2 c= {x1,x2} & {x1,x2} c= B by A2,ENUMSET1:41,ZFMISC_1:38;
    then rng g2 c= B by XBOOLE_1:1;
    then reconsider g2 as Function of A,B by A2,A9,FUNCT_2:def 1,RELSET_1:11;
    reconsider m1 = [[A,B],g1], m2 = [[A,B],g2]
 as Element of Maps(V) by A2,Th5;
    set f1 = @m1, f2 = @m2;
A10:   m1 = f1 & m2 = f2 by Def17;
A11:   m1 = [[dom m1,cod m1],m1`2] & m2 = [[dom m2,cod m2],m2`2] by Th8;
    then dom m1 = A & dom m2 = A & cod m1 = B & cod m2 = B by Lm1;
then A12:    dom(@f1) = A & dom(@f2) = A & cod(@f1) = B & cod(@f2) = B
     by Lm7;
then A13:    dom f1 = A & dom f2 = A & cod f1 = B & cod f2 = B & cod f = A
     by Th26;
A14:  g1 = m1`2 & g2 = m2`2 by A11,ZFMISC_1:33;
    set h1 = (@f1)`2*(@f)`2, h2 = (@f2)`2*(@f)`2;
    set f1f = (@f1)*(@f), f2f = (@f2)*(@f);
       now
A15:   (f1f)`2 = h1 & dom(f1f) = dom(@f) & cod(f1f) = cod(@f1) &
       (f2f)`2 = h2 & dom(f2f) = dom(@f) & cod(f2f) = cod(@f2) by A12,Th12;
      hence f1f=[[dom(@f),cod(@f1)],h1] & f2f=[[dom(@f),cod(@f2)],h2] by Th8;
        now
       thus
A16:      dom(h1) = dom(@f) & dom(h2) = dom(@f) by A15,Lm3;
       let z be set;
       set y = (@f)`2.z;
       assume
A17:      z in dom(@f);
       then z in dom (@f)`2 by Lm3;
       then y in rng (@f)`2 by FUNCT_1:def 5;
       then g1 = (@f1)`2 & g2 =(@f2)`2 & y in A & not y in {x}
        by A4,A6,A14,Lm7,TARSKI:def 1;
       then h1.z = g1.y & h2.z = g2.y & not y in {x} & g1.y = x1
         by A16,A17,FUNCOP_1:13,FUNCT_1:22;
       hence h1.z = h2.z by A8,FUNCT_4:12;
      end;
      hence h1 = h2 by FUNCT_1:9;
     end;
    then f1f = f2f & f1*f = f1f & f2*f = f2f & h.x = x2
      by A7,A12,A13,Th28,FUNCOP_1:13;
    then f1 = f2 & g1.x = x1 & g2.x = x2
      by A1,A5,A7,A8,A13,CAT_1:def 11,FUNCOP_1:13,FUNCT_4:14;
    hence contradiction by A3,A10,ZFMISC_1:33;
   end;
  hence rng (@f)`2 = cod(@f) by A4,XBOOLE_0:def 10;
 end;

theorem
     @f is_a_surjection implies f is epi
 proof set m = @f;
  assume
A1:  rng m`2 = cod m;
  let f1,f2 such that
A2:  dom f1 = cod f & dom f2 = cod f & cod f1 = cod f2 and
A3:  f1*f=f2*f;
   set m1 = @f1, m2 = @f2;
A4:  dom m1 = dom f1 & dom m2 = dom f2 & cod m1 = cod f1 & cod m2 = cod f2 &
      cod m = cod f by Th26;
   then m1*m = f1*f & m2*m = f2*f &
    m1*m = [[dom m,cod m1],m1`2*m`2] & m2*m = [[dom m,cod m2],m2`2*m`2]
      by A2,Def7,Th28;
   then (m1`2)*(m`2) = (m2`2)*(m`2) & dom m1`2 = dom f1 & dom m2`2 = dom f2
     by A3,A4,Lm3,ZFMISC_1:33;
   then m1`2 = m2`2 & m1=[[dom m1,cod m1],m1`2] & m2=[[dom m2,cod m2],m2`2]
    by A1,A2,A4,Th8,FUNCT_1:156;
   hence f1 = m2 by A2,A4,Def18 .= f2 by Def18;
 end;

theorem
     for W being Universe, f being Morphism of Ens(W) st f is epi
    holds @f is_a_surjection
 proof let W be Universe, f be Morphism of Ens(W);
A1:  {} in W by CLASSES2:62;
  then {{}} in W by CLASSES2:63;
  then {{},{{}}} in W & {} in {{},{{}}} & {{}} in {{},{{}}} & {{}} <> {}
    by A1,CLASSES2:64,TARSKI:def 2;
  hence thesis by Th37;
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;
A1:  Ens(W) = CatStr(# W,Maps W,fDom W,fCod W,fComp W,fId W #) &
     Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #) by Def14;
A2:  for a,b being Object of Ens(W), a',b' being Object of Ens(V)
      st a = a' & b = b' holds Hom(a,b) = Hom(a',b')
  proof let a,b be Object of Ens(W), a',b' be Object of Ens(V);
   assume a = a' & b = b';
   then @a = a & @a' = a & @b = b & @b' = b &
     Hom(a,b) = Maps(@a,@b) & Hom(a',b') = Maps(@a',@b') by Def16,Th27;
   hence Hom(a,b) = Hom(a',b') by Lm5;
  end;
 thus Ens(W) is Subcategory of Ens(V)
  proof
   thus the Objects of Ens(W) c= the Objects of Ens(V) by A1;
   thus for a,b being Object of Ens(W), a',b' being Object of Ens(V)
      st a = a' & b = b' holds Hom(a,b) c= Hom(a',b') by A2;
   set w = the Comp of Ens(W), v = the Comp of Ens(V);
     now
A3:   dom w c= [:Maps W,Maps W:] & dom v c= [:Maps V,Maps V:]
       by A1,RELSET_1:12;
A4:    Maps W c= Maps V by Th7;
    thus
A5:   dom w c= dom v
     proof let x be set; assume
A6:    x in dom w;
      then consider m2,m1 being Element of Maps W such that
A7:    x = [m2,m1] by A3,DOMAIN_1:9;
      reconsider m1' = m1, m2' = m2 as Element of Maps V by A4,TARSKI:def 3;
        m1 = [[dom m1,cod m1],m1`2] & m2 = [[dom m2,cod m2],m2`2] &
       m1' = [[dom m1',cod m1'],m1'`2] & m2' = [[dom m2',cod m2'],m2'`2]
       by Th8;
      then dom m2' = dom m2 & cod m1' = cod m1 & dom m2 = cod m1
       by A1,A6,A7,Def12,Lm1;
      hence x in dom v by A1,A7,Def12;
     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:9;
    reconsider m1' = m1, m2' = m2 as Element of Maps V by A4,TARSKI:def 3;
    A10:   dom m2' = cod m1' & dom m2 = cod m1 by A1,A5,A8,A9,Def12;
      m1 = [[dom m1,cod m1],m1`2] & m2 = [[dom m2,cod m2],m2`2] &
     m1' = [[dom m1',cod m1'],m1'`2] & m2' = [[dom m2',cod m2'],m2'`2] by Th8;
    then m1`2 = m1'`2 & m2`2 = m2'`2 & dom m1 = dom m1' & cod m2 = cod m2'
      by Lm1;
    then m2*m1=[[dom m1,cod m2],m2`2*m1`2] & m2'*m1'=[[dom m1,cod m2],
      m2`2*m1`2]
      by A10,Def7;
    hence w.x = m2'*m1' by A1,A9,A10,Def12 .= v.x by A1,A9,A10,Def12;
   end;
   hence the Comp of Ens(W) <= the Comp of Ens(V) by GRFUNC_1:8;
   let a be Object of Ens(W), a' be Object of Ens(V);
   assume a = a';
   then @a = a & @a' = a by Def16;
   then id$(@a) = [[@a,@a],id(@a)] & id$(@a') = [[@a,@a],id(@a)] by Def6;
   hence id a = id$(@a') by Th29 .= id a' by Th29;
  end;
  thus thesis by A2;
 end;


begin :: Representable Functors

reserve C for Category, a,b,a',b',c for Object of C,
        f,g,h,f',g' for Morphism of C;

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

definition let C;
 cluster Hom(C) -> non empty;
 coherence
  proof consider a;
     Hom(a,a) in { Hom(a',b'): not contradiction };
   hence thesis by Def19;
  end;
end;

theorem Th41:
   Hom(a,b) in Hom(C)
 proof Hom(C) = { Hom(a',b'): not contradiction } by Def19; hence thesis; end
;

:: 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:19; hence thesis by CAT_1:52; end;

definition let C,a,f;
 func hom(a,f) -> Function of Hom(a,dom f),Hom(a,cod f) means
:Def20: for g st g in Hom(a,dom f) holds it.g = f*g;
  existence
 proof set X = Hom(a,dom f), Y = Hom(a,cod f);
  defpred P[set,set] means for g st g = $1 holds $2 = f*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; assume
A2:   x in X;
    then reconsider g = x as Morphism of a,dom f by CAT_1:def 7;
    take f*g;
      X <> {} & Hom(dom f,cod f) <> {} & f is Morphism of dom f,cod f
     by A2,CAT_1:18,22;
    hence thesis by CAT_1:51;
   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 NonUniqBoundFuncEx(A1);
    Hom(dom f,cod f) <> {} by CAT_1:19;
  then Y = {} implies X = {} by CAT_1:52;
  then reconsider h as Function of X,Y by A3,FUNCT_2:def 1,RELSET_1:11;
  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
      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:18;
  end;
  hence thesis;
 end;

 func hom(f,a) -> Function of Hom(cod f,a),Hom(dom f,a) means
:Def21: for g st g in Hom(cod f,a) holds it.g = g*f;
  existence
 proof set X = Hom(cod f,a), Y = Hom(dom f,a);
  defpred P[set,set] means for g st g = $1 holds $2 = g*f;
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 7;
    take g*f;
      X <> {} & Hom(dom f,cod f) <> {} & f is Morphism of dom f,cod f
     by A9,CAT_1:19,22;
    hence thesis by CAT_1:51;
   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 NonUniqBoundFuncEx(A8);
    Hom(dom f,cod f) <> {} by CAT_1:19;
  then Y = {} implies X = {} by CAT_1:52;
  then reconsider h as Function of X,Y by A10,FUNCT_2:def 1,RELSET_1:11;
  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
      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:18;
  end;
  hence thesis;
 end;
end;

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

theorem Th44:
   hom(id c,a) = id Hom(c,a)
 proof
   set A = Hom(c,a);
A1:  dom id c = c & cod id c = c by CAT_1:44;
     now
      A = {} implies A = {};
    hence dom hom(id c,a) = A by A1,FUNCT_2:def 1;
    let x be set;
    assume
A2:   x in A;
    then reconsider g = x as Morphism of C;
A3:   dom g = c by A2,CAT_1:18;
    thus hom(id(c),a).x = g * id(c) by A1,A2,Def21
                       .= x by A3,CAT_1:47;
   end;
  hence thesis by FUNCT_1:34;
 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 & cod(g*f) = cod g by CAT_1:42;
     now set h = hom(a,g*f), h2 = hom(a,g), h1 = hom(a,f);
       Hom(dom f,cod f) <> {} by CAT_1:19;
then A3:    Hom(a,cod f) = {} implies Hom(a,dom f) = {} by CAT_1:52;
       Hom(dom g,cod g) <> {} by CAT_1:19;
then A4:    Hom(a,cod g) = {} implies Hom(a,dom g) = {} by CAT_1:52;
     hence dom h = Hom(a,dom f) by A1,A2,A3,FUNCT_2:def 1;
       h2*h1 is Function of Hom(a,dom f),Hom(a,cod g) by A1,A3,FUNCT_2:19;
     hence
A5:    dom(h2*h1) = Hom(a,dom f) by A1,A3,A4,FUNCT_2:def 1;
     let x be set;
     assume
A6:    x in Hom(a,dom f);
     then reconsider f' = x as Morphism of C;
A7:    h1.x in Hom(a,dom g) by A1,A3,A6,FUNCT_2:7;
     then reconsider g' = h1.x as Morphism of C;
A8:    cod f' = dom f by A6,CAT_1:18;
     thus h.x = g*f*f' by A2,A6,Def20
             .= g*(f*f') by A1,A8,CAT_1:43
             .= g*g' by A6,Def20
             .= h2.g' by A7,Def20
             .= (h2*h1).x by A5,A6,FUNCT_1:22;
    end;
  hence thesis by FUNCT_1:9;
 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:  dom(g*f) = dom f & cod(g*f) = cod g by CAT_1:42;
     now set h = hom(g*f,a), h2 = hom(g,a), h1 = hom(f,a);
       Hom(dom f,cod f) <> {} by CAT_1:19;
then A3:    Hom(dom f,a) = {} implies Hom(cod f,a) = {} by CAT_1:52;
       Hom(dom g,cod g) <> {} by CAT_1:19;
then A4:    Hom(dom g,a) = {} implies Hom(cod g,a) = {} by CAT_1:52;
     hence dom h = Hom(cod g,a) by A1,A2,A3,FUNCT_2:def 1;
       h1*h2 is Function of Hom(cod g,a),Hom(dom f,a) by A1,A4,FUNCT_2:19;
     hence
A5:    dom(h1*h2) = Hom(cod g,a) by A1,A3,A4,FUNCT_2:def 1;
     let x be set;
     assume
A6:    x in Hom(cod g,a);
     then reconsider f' = x as Morphism of C;
A7:   h2.x in Hom(cod f,a) by A1,A4,A6,FUNCT_2:7;
     then reconsider g' = h2.x as Morphism of C;
A8:    dom f' = cod g by A6,CAT_1:18;
     thus h.x = f'*(g*f) by A2,A6,Def21
             .= f'*g*f by A1,A8,CAT_1:43
             .= g'*f by A6,Def21
             .= h1.g' by A7,Def21
             .= (h1*h2).x by A5,A6,FUNCT_1:22;
    end;
  hence thesis by FUNCT_1:9;
 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:19;
  then (Hom(a,cod f) = {} implies Hom(a,dom f) = {}) &
    Hom(a,dom f) in Hom(C) & Hom(a,cod f) in Hom(C) by Th41,CAT_1:52;
  hence thesis by 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:19;
  then (Hom(dom f,a) = {} implies Hom(cod f,a) = {}) &
    Hom(dom f,a) in Hom(C) & Hom(cod f,a) in Hom(C) by Th41,CAT_1:52;
  hence thesis by Th5;
 end;

definition let C,a;
 func hom?-(a) -> Function of the Morphisms of C, Maps(Hom(C)) means
:Def22: for f holds it.f = [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)];
  existence
 proof set X = the Morphisms of C, Y = Maps(Hom(C));
  defpred P[set,set] means
    for f st f = $1 holds $2 = [[Hom(a,dom f),Hom(a,cod f)],hom(a,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 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 NonUniqBoundFuncEx(A1);
  reconsider h as Function of X,Y by A2,FUNCT_2:def 1,RELSET_1:11;
  take h; thus thesis by A3;
 end;
  uniqueness
 proof let h1,h2 be Function of the Morphisms 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:113;
 end;

 func hom-?(a) -> Function of the Morphisms of C, Maps(Hom(C)) means
:Def23: for f holds it.f = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)];
 existence
 proof set X = the Morphisms of C, Y = Maps(Hom(C));
  defpred P[set,set] means
    for f st f = $1 holds $2 = [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)];
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 NonUniqBoundFuncEx(A6);
  reconsider h as Function of X,Y by A7,FUNCT_2:def 1,RELSET_1:11;
  take h; thus thesis by A8;
 end;
 uniqueness
 proof let h1,h2 be Function of the Morphisms 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:113;
 end;
end;

Lm9: for T being Function of the Morphisms of C, Maps(Hom(C)) st Hom(C) c= V
   holds T is Function of the Morphisms of C, the Morphisms of Ens V
 proof let T be Function of the Morphisms of C, Maps(Hom(C));
  assume Hom(C) c= V;
  then Hom(C) is non empty Subset of V &
    Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #)
     by Def14;
  then Maps(Hom(C)) c= Maps(V) & the Morphisms of Ens V = Maps V &
     Maps(Hom(C)) <> {} by Th7;
  hence thesis by FUNCT_2:9;
 end;

Lm10:
  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
  assume
A1:  Hom(C) c= V;
  let d be Object of Ens(V) such that
A2:  d = Hom(a,c);
    Hom(a,c) in Hom(C) by Th41;
  then reconsider A = Hom(a,c) as Element of V by A1;
    dom id c = c & cod id c = c & hom(a,id c) = id A by Th43,CAT_1:44;
  hence (hom?-(a)).(id c)
      = [[A,A],id A] by Def22
     .= id$ A by Def6
     .= id$ @@A by Lm6
     .= id$ @d by A2,Def15
     .= id d by Th29;
 end;

Lm11:
  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
  assume
A1:  Hom(C) c= V;
  let d be Object of Ens(V) such that
A2:  d = Hom(c,a);
    Hom(c,a) in Hom(C) by Th41;
  then reconsider A = Hom(c,a) as Element of V by A1;
    dom id c = c & cod id c = c & hom(id(c),a) = id A by Th44,CAT_1:44;
  hence (hom-?(a)).(id c)
      = [[A,A],id A] by Def23
     .= id$ A by Def6
     .= id$ @@A by Lm6
     .= id$ @d by A2,Def15
     .= 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 Morphisms of C, the Morphisms of Ens V by Lm9;
    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) by Th41;
      then reconsider A = Hom(a,c) as Element of V by A1;
      take d = @A;
        d = A by Def15;
      hence thesis by A1,Lm10;
    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;
       Hom(a,b) in Hom(C) & Hom(a,c) in Hom(C) by Th41;
     then reconsider A = Hom(a,b), B = Hom(a,c) as Element of V by A1;
     set g = T.f;
A2:    [[Hom(a,b),Hom(a,c)],hom(a,f)]
       = g by Def22
      .= @g by Def18
      .= [[dom(@g), cod(@g)],(@g)`2] by Th8
      .= [[dom g, cod(@g)],(@g)`2] by Th26
      .= [[dom g, cod g],(@g)`2] by Th26;
A3:   A = @A by Def15;
     hence T.(id b)
         = id @A by A1,Lm10
        .= id dom (T.f) by A2,A3,Lm1;
A4:   B = @B by Def15;
     hence T.(id c)
         = id @B by A1,Lm10
        .= id cod (T.f) by A2,A4,Lm1;
    end;
   let f,g be Morphism of C such that
A5:   dom g = cod f;
       [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)]
    = T.f by Def22
   .= @(T.f) by Def18
   .= [[dom(@(T.f)),cod(@(T.f))],(@(T.f))`2] by Th8
   .= [[dom(T.f),cod(@(T.f))],(@(T.f))`2] by Th26
   .= [[dom(T.f),cod(T.f)],(@(T.f))`2] by Th26;
then A6:  (@(T.f))`2=hom(a,f) & dom(T.f)=Hom(a,dom f) & cod(T.f)=Hom(a,cod f)
     by Lm1,ZFMISC_1:33;
then A7:   dom(@(T.f))=Hom(a,dom f) & cod(@(T.f))=Hom(a,cod f)
       by Th26;
       [[Hom(a,dom g),Hom(a,cod g)],hom(a,g)]
    = T.g by Def22
   .= @(T.g) by Def18
   .= [[dom(@(T.g)),cod(@(T.g))],(@(T.g))`2] by Th8
   .= [[dom(T.g),cod(@(T.g))],(@(T.g))`2] by Th26
   .= [[dom(T.g),cod(T.g)],(@(T.g))`2] by Th26;
then A8:  (@(T.g))`2=hom(a,g) & dom(T.g)=Hom(a,dom g) & cod(T.g)=Hom(a,cod g)
    by Lm1,ZFMISC_1:33;
then A9:  dom(@(T.g))=Hom(a,dom g) & cod(@(T.g))=Hom(a,cod g) by Th26;
     dom(g*f) = dom f & cod(g*f) = cod g by A5,CAT_1:42;
   hence T.(g*f) = [[Hom(a,dom(f)),Hom(a,cod(g))],hom(a,g*f)] by Def22
                .= [[Hom(a,dom(f)),Hom(a,cod(g))],hom(a,g)*hom(a,f)] by A5,Th45
                .= (@(T.g))*(@(T.f)) by A5,A6,A7,A8,A9,Def7
                .= (T.g)*(T.f) by A5,A6,A8,Th28;
  end;
  hence thesis by CAT_1:96;
 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 Morphisms of C, the Morphisms of Ens V by Lm9;
    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) by Th41;
      then reconsider A = Hom(c,a) as Element of V by A1;
      take d = @A;
        d = A by Def15;
      hence thesis by A1,Lm11;
    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;
       Hom(b,a) in Hom(C) & Hom(c,a) in Hom(C) by Th41;
     then reconsider A = Hom(b,a), B = Hom(c,a) as Element of V by A1;
     set g = T.f;
A2:    [[Hom(b,a),Hom(c,a)],hom(f,a)]
       = g by Def23
      .= @g by Def18
      .= [[dom(@g), cod(@g)],(@g)`2] by Th8
      .= [[dom g, cod(@g)],(@g)`2] by Th26
      .= [[dom g, cod g],(@g)`2] by Th26;
A3:   B = @B by Def15;
     hence T.(id c)
         = id @B by A1,Lm11
        .= id cod (T.f) by A2,A3,Lm1;
A4:   A = @A by Def15;
     hence T.(id b)
         = id @A by A1,Lm11
        .= id dom (T.f) by A2,A4,Lm1;
    end;
   let f,g be Morphism of C such that
A5:   dom g = cod f;
       [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)]
    = T.f by Def23
   .= @(T.f) by Def18
   .= [[dom(@(T.f)),cod(@(T.f))],(@(T.f))`2] by Th8
   .= [[dom(T.f),cod(@(T.f))],(@(T.f))`2] by Th26
   .= [[dom(T.f),cod(T.f)],(@(T.f))`2] by Th26;
then A6:  (@(T.f))`2=hom(f,a) & dom(T.f)=Hom(cod f,a) & cod(T.f)=Hom(dom f,a)
     by Lm1,ZFMISC_1:33;
then A7:   dom(@(T.f))=Hom(cod f,a) & cod(@(T.f))=Hom(dom f,a)
       by Th26;
       [[Hom(cod g,a),Hom(dom g,a)],hom(g,a)]
    = T.g by Def23
   .= @(T.g) by Def18
   .= [[dom(@(T.g)),cod(@(T.g))],(@(T.g))`2] by Th8
   .= [[dom(T.g),cod(@(T.g))],(@(T.g))`2] by Th26
   .= [[dom(T.g),cod(T.g)],(@(T.g))`2] by Th26;
then A8:  (@(T.g))`2=hom(g,a) & dom(T.g)=Hom(cod g,a) & cod(T.g)=Hom(dom g,a)
    by Lm1,ZFMISC_1:33;
then A9:  dom(@(T.g))=Hom(cod g,a) & cod(@(T.g))=Hom(dom g,a)
      by Th26;
     dom(g*f) = dom f & cod(g*f) = cod g by A5,CAT_1:42;
   hence T.(g*f) = [[Hom(cod(g),a),Hom(dom(f),a)],hom(g*f,a)] by Def23
                .= [[Hom(cod(g),a),Hom(dom(f),a)],hom(f,a)*hom(g,a)] by A5,Th46
                .= (@(T.f))*(@(T.g)) by A5,A6,A7,A8,A9,Def7
                .= (T.f)*(T.g) by A5,A6,A8,Th28;
  end;
  hence thesis by OPPCAT_1:def 7;
 end;

:: hom-bifunctor

theorem Th51:
   Hom(dom f,cod f') = {} implies Hom(cod f,dom f') = {}
 proof assume that
A1:  Hom(dom f,cod f') = {} and
A2:  Hom(cod f,dom f') <> {};
     Hom(dom f,cod f) <> {} by CAT_1:19;
   then Hom(dom f,dom f') <> {} & Hom(dom f',cod f') <> {} by A2,CAT_1:19,52;
   hence contradiction by A1,CAT_1:52;
 end;

definition let C,f,g;
 func hom(f,g) -> Function of Hom(cod f,dom g),Hom(dom f,cod g) means
:Def24:  for h st h in Hom(cod f,dom g) holds it.h = g*h*f;
  existence
 proof set X = Hom(cod f,dom g), Y = Hom(dom f,cod g);
  defpred P[set,set] means for h st h = $1 holds $2 = g*h*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 h = x as Morphism of cod f,dom g by CAT_1:def 7;
    take g*h*f;
      X <> {} & Hom(dom g,cod g) <> {} & g is Morphism of dom g,cod g
      by A2,CAT_1:19,22;
    then g*h in Hom(cod f,cod g) by CAT_1:51;
    then Hom(dom f,cod f) <> {} & Hom(cod f,cod g) <> {} &
       g*h is Morphism of cod f,cod g & f is Morphism of dom f,cod f
        by CAT_1:19,22,def 7;
    hence thesis by CAT_1:51;
   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 NonUniqBoundFuncEx(A1);
    Y = {} implies X = {} by Th51;
  then reconsider h as Function of X,Y by A3,FUNCT_2:def 1,RELSET_1:11;
  take h; thus thesis by A4;
 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
A5:  for h st h in X holds h1.h = g*h*f and
A6:  for h st h in X holds h2.h = g*h*f;
      now let x be set;
     assume
A7:    x in X;
     then reconsider h = x as Morphism of C;
     thus h1.x = g*h*f by A5,A7 .= h2.x by A6,A7;
    end;
    hence thesis by FUNCT_2:18;
 end;
end;

theorem Th52:
   [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)] is Element of Maps(Hom(C))
 proof
     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 Th41,Th51;
  hence thesis by Th5;
 end;

theorem Th53:
   hom(id a,f) = hom(a,f) & hom(f,id a) = hom(f,a)
 proof
A1:   dom id a = a & cod id a = a by CAT_1:44;
     now
      Hom(dom f,cod f) <> {} by CAT_1:19;
    then Hom(a,cod f) = {} implies Hom(a,dom f) = {} by CAT_1:52;
    hence dom hom(id a,f) = Hom(a,dom f) & dom hom(a,f) = Hom(a,dom f)
     by A1,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 & cod g = dom f by A2,CAT_1:18;
    thus hom(id a,f).x = f*g*(id a) by A1,A2,Def24
                      .= f*(g*(id a)) by A1,A3,CAT_1:43
                      .= f*g by A3,CAT_1:47
                      .= hom(a,f).x by A2,Def20;
   end;
  hence hom(id a,f) = hom(a,f) by FUNCT_1:9;
     now
      Hom(dom f,cod f) <> {} by CAT_1:19;
    then Hom(dom f,a) = {} implies Hom(cod f,a) = {} by CAT_1:52;
    hence dom hom(f,id a) = Hom(cod f,a) & dom hom(f,a) = Hom(cod f,a)
     by A1,FUNCT_2:def 1;
    let x be set;
    assume
A4:   x in Hom(cod f,a);
    then reconsider g = x as Morphism of C;
A5:   dom g = cod f & cod g = a by A4,CAT_1:18;
    thus hom(f,id a).x = (id a)*g*f by A1,A4,Def24
                      .= g*f by A5,CAT_1:46
                      .= hom(f,a).x by A4,Def21;
   end;
  hence hom(f,id a) = hom(f,a) by FUNCT_1:9;
 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;
     now
      Hom(dom f,cod f) <> {} by CAT_1:19;
    hence Hom(dom f,dom g) = {} implies Hom(cod f,dom g) = {} by CAT_1:52;
      Hom(dom g,cod g) <> {} by CAT_1:19;
    hence Hom(dom f,cod g) = {} implies Hom(dom f,dom g) = {} by CAT_1:52;
   end;
   then hom(dom f,g)*hom(f,dom g)
      is Function of Hom(cod f,dom g),Hom(dom f,cod g) by FUNCT_2:19;
   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 & cod h = dom g by A3,CAT_1:18;
   then dom(h*f) = dom f & cod(h*f) = dom g by CAT_1:42;
then A5:  h*f in Hom(dom f,dom g) by CAT_1:18;
   thus hom(f,g).x = g*h*f by A3,Def24
                  .= g*(h*f) by A4,CAT_1:43
                  .= hom(dom f,g).(h*f) by A5,Def20
                  .= hom(dom f,g).((hom(f,dom g)).h) by A3,Def21
                  .= (hom(dom f,g)*hom(f,dom g)).x by A2,A3,FUNCT_1:22;
  end;
  hence thesis by FUNCT_1:9;
 end;

theorem Th56:
  cod g = dom f & dom g' = cod f' implies hom(f*g,g'*f') = hom(g,g')*hom(f,f')
 proof assume
A1:  cod g = dom f & dom g' = cod f';
then A2:  dom(g'*f') = dom f' & cod(g'*f') = cod g' &
      dom(f*g) = dom g & cod(f*g) = cod f by CAT_1:42;
      now set h = hom(f*g,g'*f'), h2 = hom(g,g'), h1 = hom(f,f');
A3:   Hom(dom g,cod g') = {} implies Hom(cod g,dom g') = {} by Th51;
A4:   Hom(dom f,cod f') = {} implies Hom(cod f,dom f') = {} by Th51;
      hence dom h = Hom(cod f,dom f') by A1,A2,A3,FUNCT_2:def 1;
        h2*h1 is Function of Hom(cod f,dom f'),Hom(dom g,cod g')
       by A1,A4,FUNCT_2:19;
      hence
A5:     dom(h2*h1) = Hom(cod f,dom f') by A1,A3,A4,FUNCT_2:def 1;
      let x be set;
      assume
A6:     x in Hom(cod f,dom f');
      then reconsider k = x as Morphism of C;
A7:    h1.x in Hom(cod g,dom g') by A1,A4,A6,FUNCT_2:7;
      then reconsider l = h1.x as Morphism of C;
A8:     cod k = dom f' by A6,CAT_1:18;
A9:     dom k = cod f by A6,CAT_1:18;
then A10:     cod(k*(f*g)) = cod k by A2,CAT_1:42;
A11:     dom(f'*k) = dom k & cod(f'*k) = cod f' by A8,CAT_1:42;
then A12:    dom (f'*k*f) = dom f & cod(f'*k*f) = cod f' by A9,CAT_1:42;
      thus h.x = (g'*f')*k*(f*g) by A2,A6,Def24
              .= (g'*f')*(k*(f*g)) by A2,A8,A9,CAT_1:43
              .= g'*(f'*(k*(f*g))) by A1,A8,A10,CAT_1:43
              .= g'*(f'*k*(f*g)) by A2,A8,A9,CAT_1:43
              .= g'*(f'*k*f*g) by A1,A9,A11,CAT_1:43
              .= g'*(f'*k*f)*g by A1,A12,CAT_1:43
              .= g'*l*g by A6,Def24
              .= h2.l by A7,Def24
              .= (h2*h1).x by A5,A6,FUNCT_1:22;
     end;
  hence thesis by FUNCT_1:9;
 end;

definition let C;
 func hom??(C) -> Function of the Morphisms of [:C,C:], Maps(Hom(C)) means
:Def25: for f,g holds it.[f,g] = [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)]
;
  existence
 proof set X = the Morphisms of [:C,C:], Y = Maps(Hom(C));
  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)];
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 CAT_2:37;
    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 f',g';
    assume x = [f',g'];
    then f' = f & g' = g by A2,ZFMISC_1:33;
    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 NonUniqBoundFuncEx(A1);
  reconsider h as Function of X,Y by A3,FUNCT_2:def 1,RELSET_1:11;
  take h; thus thesis by A4;
 end;
  uniqueness
 proof
  let h1,h2 be Function of the Morphisms 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 Morphisms of [:C,C:] = [:the Morphisms of C,the Morphisms of C:]
     by CAT_2:33;
    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 FUNCT_2:120;
 end;
end;

theorem Th57:
   hom?-(a) = (curry (hom??(C))).(id a) & hom-?(a) = (curry' (hom??(C))).(id a)
 proof
    [:the Morphisms of C,the Morphisms of C:] = the Morphisms of [:C, C:]
   by CAT_2:33;
  then reconsider T = hom??(C)
     as Function of [:the Morphisms of C,the Morphisms of C:],Maps(Hom(C));
     now let f;
    thus ((curry T).(id a)).f
       = T.[id a,f] by CAT_2:3
      .= [[Hom(cod id a,dom f),Hom(dom id a,cod f)],hom(id a,f)] by Def25
      .= [[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)] by CAT_1:44
      .= [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] by CAT_1:44
      .= (hom?-(a)).f by Def22;
   end;
  hence hom?-(a) = (curry (hom??(C))).(id a) by FUNCT_2:113;
     now let f;
    thus ((curry' T).(id a)).f
       = T.[f,id a] by CAT_2:4
      .= [[Hom(cod f,dom id a),Hom(dom f,cod id a)],hom(f,id a)] by Def25
      .= [[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)] by CAT_1:44
      .= [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] by CAT_1:44
      .= (hom-?(a)).f by Def23;
   end;
  hence hom-?(a) = (curry' (hom??(C))).(id a) by FUNCT_2:113;
 end;

Lm12:
  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
  assume
A1:  Hom(C) c= V;
  let d be Object of Ens(V) such that
A2:  d = Hom(a,b);
    Hom(a,b) in Hom(C) by Th41;
  then reconsider A = Hom(a,b) as Element of V by A1;
    dom id a = a & cod id a = a & dom id b = b & cod id b = b &
   hom(id a,id b) = id A by Th54,CAT_1:44;
  hence (hom??(C)).[id a,id b]
      = [[A,A],id A] by Def25
     .= id$ A by Def6
     .= id$ @@A by Lm6
     .= id$ @d by A2,Def15
     .= 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;
    C opp = CatStr (#the Objects of C, the Morphisms of C,
                   the Cod of C, the Dom of C,
                   ~(the Comp of C), the Id of C#) by OPPCAT_1:def 1;
  then Hom(C) is non empty Subset of V &
   the Morphisms of [:C opp,C:]=[:the Morphisms of C,the Morphisms of C:] &
    Ens(V) = CatStr(# V,Maps V,fDom V,fCod V,fComp V,fId V #)
     by A1,Def14,CAT_2:33;
  then the Morphisms of [:C opp,C:] = the Morphisms of [:C,C:] &
     Maps(Hom(C)) c= Maps(V) & the Morphisms of Ens V = Maps V &
     Maps(Hom(C)) <> {} by Th7,CAT_2:33;
  then reconsider T = hom??(C) as
    Function of the Morphisms of [:C opp,C:], the Morphisms of Ens V
     by FUNCT_2:9;
A2: for f being Morphism of C opp holds opp f = f
   proof let f be Morphism of C opp;
    thus opp f = f opp by OPPCAT_1:def 5 .= f by OPPCAT_1:def 4;
   end;
A3: for a being Object of C opp holds opp a = a
   proof let a be Object of C opp;
    thus opp a = a opp by OPPCAT_1:def 3 .= a by OPPCAT_1:def 2;
   end;
    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
A4:     c = [a,b] by CAT_2:35;
        Hom(opp a,b) in Hom(C) by Th41;
      then reconsider A = Hom(opp a,b) as Element of V by A1;
      take d = @A;
        now
        thus id c = [id a,id b] by A4,CAT_2:41
            .= [opp(id a), id b] by A2
            .= [id(opp a),id b] by OPPCAT_1:22;
        thus d = A by Def15;
      end;
      hence thesis by A1,Lm12;
    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
A5:    fg = [f,g] by CAT_2:37;
       Hom(cod opp f,dom g) in Hom(C) & Hom(dom opp f,cod g) in Hom(C) by Th41;
     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;
       opp f = f by A2;
then A6:    [[Hom(cod opp f,dom g),Hom(dom opp f,cod g)],hom(opp f,g)]
       = h by A5,Def25
      .= @h by Def18
      .= [[dom(@h), cod(@h)],(@h)`2] by Th8
      .= [[dom h, cod(@h)],(@h)`2] by Th26
      .= [[dom h, cod h],(@h)`2] by Th26;
A7:   A = @A by Def15;
     thus T.(id dom fg)
         = T.(id [dom f,dom g]) by A5,CAT_2:38
        .= T.[id dom f,id dom g] by CAT_2:41
        .= T.[opp (id dom f),id dom g] by A2
        .= T.[id opp(dom f),id dom g] by OPPCAT_1:22
        .= T.[id cod opp f,id dom g] by OPPCAT_1:12
        .= id @A by A1,A7,Lm12
        .= id dom (T.fg) by A6,A7,Lm1;
A8:   B = @B by Def15;
     thus T.(id cod fg)
         = T.(id [cod f,cod g]) by A5,CAT_2:38
        .= T.[id cod f,id cod g] by CAT_2:41
        .= T.[opp(id cod f),id cod g] by A2
        .= T.[id opp(cod f),id cod g] by OPPCAT_1:22
        .= T.[id dom opp f,id cod g] by OPPCAT_1:12
        .= id @B by A1,A8,Lm12
        .= id cod (T.fg) by A6,A8,Lm1;
    end;
   let ff,gg be Morphism of [:C opp,C:] such that
A9:   dom gg = cod ff;
    consider f being (Morphism of C opp), f' such that
A10:   ff = [f,f'] by CAT_2:37;
    consider g being (Morphism of C opp), g' such that
A11:   gg = [g,g'] by CAT_2:37;
      opp f = f by A2;
     then [[Hom(cod opp f,dom f'),Hom(dom opp f,cod f')],hom(opp f,f')]
    = T.ff by A10,Def25
   .= @(T.ff) by Def18
   .= [[dom(@(T.ff)),cod(@(T.ff))],(@(T.ff))`2] by Th8
   .= [[dom(T.ff),cod(@(T.ff))],(@(T.ff))`2] by Th26
   .= [[dom(T.ff),cod(T.ff)],(@(T.ff))`2] by Th26;
then A12:  (@(T.ff))`2=hom(opp f,f') &
       dom(T.ff)=Hom(cod opp f,dom f') & cod(T.ff)=Hom(dom opp f,cod f')
     by Lm1,ZFMISC_1:33;
then A13:   dom(@(T.ff))=Hom(cod opp f,dom f') & cod(@(T.ff))=Hom(dom opp f,cod
f')
       by Th26;
      opp g = g by A2;
     then [[Hom(cod opp g,dom g'),Hom(dom opp g,cod g')],hom(opp g,g')]
    = T.gg by A11,Def25
   .= @(T.gg) by Def18
   .= [[dom(@(T.gg)),cod(@(T.gg))],(@(T.gg))`2] by Th8
   .= [[dom(T.gg),cod(@(T.gg))],(@(T.gg))`2] by Th26
   .= [[dom(T.gg),cod(T.gg)],(@(T.gg))`2] by Th26;
then A14:  (@(T.gg))`2=hom(opp g,g') &
       dom(T.gg)=Hom(cod opp g,dom g') & cod(T.gg)=Hom(dom opp g,cod g')
    by Lm1,ZFMISC_1:33;
then A15:  dom(@(T.gg))=Hom(cod opp g,dom g') & cod(@(T.gg))=Hom(dom opp g,cod
g')
      by Th26;
A16:  dom gg = [dom g,dom g'] & cod ff = [cod f,cod f'] by A10,A11,CAT_2:38;
then A17:  dom g = cod f by A9,ZFMISC_1:33;
       now
      thus dom gg = [opp dom g,dom g'] by A3,A16
                 .= [cod opp g,dom g'] by OPPCAT_1:12;
      thus cod ff = [opp cod f,cod f'] by A3,A16
                 .= [dom opp f,cod f'] by OPPCAT_1:12;
     end;
then A18:  cod opp g = dom opp f & dom g' = cod f' by A9,ZFMISC_1:33;
then A19:   dom(g'*f') = dom f' & cod(g'*f') = cod g' &
       dom((opp f)*(opp g)) = dom opp g & cod((opp f)*(opp g)) = cod opp f
        by CAT_1:42;
   thus T.(gg*ff)
    = T.([g*f,g'*f']) by A9,A10,A11,CAT_2:40
   .= T.([opp (g*f),g'*f']) by A2
   .= T.([(opp f)*(opp g),g'*f']) by A17,OPPCAT_1:19
   .= [[Hom(cod((opp f)*(opp g)),dom(g'*f')),
        Hom(dom((opp f)*(opp g)),cod(g'*f'))],
       hom((opp f)*(opp g),g'*f')] by Def25
   .= [[Hom(cod opp f,dom f'),Hom(dom opp g,cod g')],
       hom(opp g,g')*hom(opp f,f')] by A18,A19,Th56
   .= (@(T.gg))*(@(T.ff)) by A12,A13,A14,A15,A18,Def7
   .= (T.gg)*(T.ff) by A12,A14,A18,Th28;
  end;
  hence thesis by CAT_1:96;
 end;

definition let V,C,a;
 assume A1: Hom(C) c= V;
 func hom?-(V,a) -> Functor of C,Ens(V) equals
:Def26:  hom?-(a);
  coherence by A1,Th49;
 func hom-?(V,a) -> Contravariant_Functor of C,Ens(V) equals
:Def27:  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
:Def28:  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 Def26
                      .= [[Hom(a,dom f),Hom(a,cod f)],hom(a,f)] by Def22;
 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) by Th41;
   then reconsider A = Hom(a,b) as Element of V by A1;
   set d = @A;
A2:  d = A by Def15;
     (hom?-(V,a)).(id b) = (hom?-(a)).(id b) by A1,Def26
                      .= id d by A1,A2,Lm10;
   hence thesis by A2,CAT_1:103;
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 Def27
                      .= [[Hom(cod f,a),Hom(dom f,a)],hom(f,a)] by Def23;
 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) by Th41;
   then reconsider A = Hom(b,a) as Element of V by A1;
   set d = @A;
A2:  d = A by Def15;
     (hom-?(V,a)).(id b) = (hom-?(a)).(id b) by A1,Def27
                      .= id d by A1,A2,Lm11;
   hence thesis by A2,OPPCAT_1:31;
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??(V,C)).[f,g] by OPPCAT_1:def 4
    .= (hom??(C)).[f,g] by A1,Def28
    .= [[Hom(cod f,dom g),Hom(dom f,cod g)],hom(f,g)] by Def25;
 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) by Th41;
   then reconsider A = Hom(a,b) as Element of V by A1;
   set d = @A;
A2:  d = A by Def15;
     (hom??(V,C)).(id[a opp,b]) = (hom??(V,C)).[id(a opp),id b] by CAT_2:41
                             .= (hom??(V,C)).[(id a) opp,id b] by OPPCAT_1:21
                             .= (hom??(V,C)).[id a,id b] by OPPCAT_1:def 4
                             .= (hom??(C)).[id a,id b] by A1,Def28
                             .= id d by A1,A2,Lm12;
   hence thesis by A2,CAT_1:103;
 end;

theorem
     Hom(C) c= V implies hom??(V,C)?-(a opp) = hom?-(V,a)
 proof assume
A1:  Hom(C) c= V;
   thus hom??(V,C)?-(a opp) = (curry hom??(V,C)).(id (a opp)) by CAT_2:def 8
                           .= (curry hom??(V,C)).((id a) opp) by OPPCAT_1:21
                           .= (curry hom??(V,C)).(id a) by OPPCAT_1:def 4
                           .= (curry hom??(C)).(id a) by A1,Def28
                           .= hom?-(a) by Th57
                           .= hom?-(V,a) by A1,Def26;
 end;

theorem
     Hom(C) c= V implies hom??(V,C)-?a = hom-?(V,a)
 proof assume
A1:  Hom(C) c= V;
  thus hom??(V,C)-?a = (curry' hom??(V,C)).(id a) by CAT_2:def 9
                    .= (curry' hom??(C)).(id a) by A1,Def28
                    .= hom-?(a) by Th57
                    .= hom-?(V,a) by A1,Def27;
 end;

Back to top