:: Cartesian Categories
::  by Czes{\l}aw Byli\'nski
::
:: Received October 27, 1992
:: Copyright (c) 1992-2016 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 CAT_1, WELLORD1, XBOOLE_0, RELAT_1, FINSET_1, FUNCT_1, STRUCT_0,
      CAT_3, GRAPH_1, CARD_1, FUNCOP_1, PARTFUN1, NAT_1, ARYTM_3, SUBSET_1,
      TARSKI, ARYTM_1, FUNCT_4, FUNCT_6, ZFMISC_1, ALGSTR_1, MCART_1, DIRAF,
      PBOOLE, EQREL_1, CAT_4, MONOID_0, RELAT_2, BINOP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1,
      RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, ALGSTR_1, XCMPLX_0,
      ORDINAL1, CARD_1, FUNCT_4, STRUCT_0, GRAPH_1, CAT_1, CAT_3;
 constructors BINOP_1, REAL_1, NAT_1, ALGSTR_1, CAT_3, RELSET_1, XREAL_0,
      FUNCT_4;
 registrations XBOOLE_0, FUNCT_1, FINSET_1, XREAL_0, NAT_1, ORDINAL1, CARD_1,
      STRUCT_0, PARTFUN1, FUNCT_2, RELSET_1, CAT_1;
 requirements NUMERALS, SUBSET, BOOLE;
 definitions CAT_1, CAT_3;
 equalities CAT_1, FUNCOP_1, GRAPH_1;
 expansions CAT_1, CAT_3;
 theorems TARSKI, ZFMISC_1, FUNCT_2, FUNCOP_1, FUNCT_4, CARD_1, CARD_2, CAT_1,
      CAT_3, FUNCT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1;
 schemes NAT_1;

begin

reserve o,m for set;

definition
  let C be Category, a,b be Object of C;

  redefine pred a,b are_isomorphic means
  Hom(a,b)<>{} & Hom(b,a)<>{} & ex f
  being Morphism of a,b, f9 being Morphism of b,a st f*f9 = id b & f9*f = id a;
  compatibility by CAT_1:48;
end;

begin :: Cartesian Categories

definition
  let C be Category;
  attr C is with_finite_product means
  for I being finite set, F being Function
of I,the carrier of C ex a being Object of C, F9 being Projections_family of a,
  I st cods F9 = F & a is_a_product_wrt F9;
end;

theorem Th1:
  for C being Category holds C is with_finite_product iff (ex a
  being Object of C st a is terminal) & for a,b being Object of C ex c being
Object of C, p1,p2 being Morphism of C st dom p1 = c & dom p2 = c & cod p1 = a
  & cod p2 = b & c is_a_product_wrt p1,p2
proof
  let C be Category;
  thus C is with_finite_product implies (ex a being Object of C st a is
  terminal) & for a,b being Object of C ex c being Object of C, p1,p2 being
  Morphism of C st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c
  is_a_product_wrt p1,p2
  proof
    reconsider F = {} as Function of {},the carrier of C by RELSET_1:12;
    assume
A1: for I being finite set, F being Function of I,the carrier of C ex
    a being Object of C, F9 being Projections_family of a,I st cods F9 = F & a
    is_a_product_wrt F9;
    then consider
    a being Object of C, F9 being Projections_family of a,{} such
    that
    cods F9 = F and
A2: a is_a_product_wrt F9;
    thus ex a being Object of C st a is terminal by A2,CAT_3:50;
    let a,b be Object of C;
    set F = (0,1)-->(a,b);
    consider c being Object of C, F9 being Projections_family of c,{0,1} such
    that
A3: cods F9 = F and
A4: c is_a_product_wrt F9 by A1;
    take c, p1 = F9/.0, p2 = F9/.1;
A5: 1 in {0,1} by TARSKI:def 2;
    then
A6: p2 = F9.1 by FUNCT_2:def 13;
A7: 0 in {0,1} by TARSKI:def 2;
    hence dom p1 = c & dom p2 = c by A5,CAT_3:41;
    F/.0 = a & F/.1 = b by CAT_3:3;
    hence cod p1 = a & cod p2 = b by A3,A7,A5,CAT_3:def 2;
    dom F9 = {0,1} & p1 = F9.0 by A7,FUNCT_2:def 1,def 13;
    then F9 = (0,1)-->(p1,p2) by A6,FUNCT_4:66;
    hence thesis by A4,CAT_3:54;
  end;
  given a being Object of C such that
A8: a is terminal;
  defpred Q[Nat] means for I being finite set, F being Function of I,the
carrier of C st card I = $1 ex a being Object of C, F9 being Projections_family
  of a,I st cods F9 = F & a is_a_product_wrt F9;
  assume
A9: for a,b being Object of C ex c being Object of C, p1,p2 being
  Morphism of C st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c
  is_a_product_wrt p1,p2;
A10: for n being Nat st Q[n] holds Q[n+1]
  proof
    let n be Nat such that
A11: Q[n];
    let I be finite set, F be Function of I,the carrier of C such that
A12: card I = n+1;
    set x = the Element of I;
    reconsider Ix = I \ {x} as finite set;
    reconsider sx = {x} as finite set;
    reconsider G = F|(I\{x}) as Function of I\{x},the carrier of C by
FUNCT_2:32;
    card(Ix) = card(I) - card(sx) by A12,CARD_1:27,CARD_2:44,ZFMISC_1:31
      .= card(I) - 1 by CARD_1:30
      .= n by A12,XCMPLX_1:26;
    then consider
    a being Object of C, G9 being Projections_family of a,I\{x} such
    that
A13: cods G9 = G and
A14: a is_a_product_wrt G9 by A11;
    consider c being Object of C, p1,p2 being Morphism of C such that
A15: dom p1 = c and
A16: dom p2 = c and
A17: cod p1 = a and
A18: cod p2 = F/.x and
A19: c is_a_product_wrt p1,p2 by A9;
    set F9 = (G9*p1) +* (x .-->p2);
A20: dom({x} -->p2) = {x} by FUNCT_2:def 1;
    rng F9 c= rng(G9*p1) \/ rng(x .-->p2) by FUNCT_4:17;
    then
A21: rng F9 c= the carrier' of C by XBOOLE_1:1;
    dom(G9*p1) = I\{x} by FUNCT_2:def 1;
    then
A22: dom(G9*p1) \/ dom(x .-->p2) = I \/ {x} by A20,XBOOLE_1:39
      .= I by A12,CARD_1:27,ZFMISC_1:40;
    then dom F9 = I by FUNCT_4:def 1;
    then reconsider F9 as Function of I, the carrier' of C by A21,FUNCT_2:def 1
,RELSET_1:4;
A23: doms G9 = (I\{x})-->a by CAT_3:def 13;
    now
      let y be object;
      assume
A24:  y in I;
      now
        per cases;
        suppose
          y = x;
          then
A25:      y in {x} by TARSKI:def 1;
          F9/.y = F9.y by A24,FUNCT_2:def 13
            .= (x .-->p2).y by A20,A25,FUNCT_4:13
            .= p2 by A25,FUNCOP_1:7;
          hence (I --> c).y = dom(F9/.y) by A16,A24,FUNCOP_1:7
            .= (doms F9)/.y by A24,CAT_3:def 1;
        end;
        suppose
A26:      y <> x;
          then
A27:      not y in {x} by TARSKI:def 1;
A28:      y in I\{x} by A24,A26,ZFMISC_1:56;
          F9/.y = F9.y by A24,FUNCT_2:def 13
            .= (G9*p1).y by A20,A22,A24,A27,FUNCT_4:def 1
            .= (G9*p1)/.y by A28,FUNCT_2:def 13;
          hence (doms F9)/.y = dom((G9*p1)/.y) by A24,CAT_3:def 1
            .= (doms(G9*p1))/.y by A28,CAT_3:def 1
            .= ((I\{x})-->c)/.y by A15,A17,A23,CAT_3:16
            .= c by A24,A26,CAT_3:2,ZFMISC_1:56
            .= (I --> c).y by A24,FUNCOP_1:7;
        end;
      end;
      hence (doms F9).y = (I --> c).y by A24,FUNCT_2:def 13;
    end;
    then reconsider F9 as Projections_family of c,I
        by CAT_3:def 13,FUNCT_2:12;
    take c,F9;
A29:  now
      let y be set;
      assume
A30:  y in I;
   now
        per cases;
        suppose
A31:      y = x;
          then
A32:      y in {x} by TARSKI:def 1;
          F9/.y = F9.y by A30,FUNCT_2:def 13
            .= (x .-->p2).y by A20,A32,FUNCT_4:13
            .= p2 by A32,FUNCOP_1:7;
          hence (cods F9)/.y = F/.y by A18,A30,A31,CAT_3:def 2;
        end;
        suppose
A33:      y <> x;
          then
A34:      not y in {x} by TARSKI:def 1;
A35:      y in I\{x} by A30,A33,ZFMISC_1:56;
          F9/.y = F9.y by A30,FUNCT_2:def 13
            .= (G9*p1).y by A20,A22,A30,A34,FUNCT_4:def 1
            .= (G9*p1)/.y by A35,FUNCT_2:def 13;
          hence (cods F9)/.y = cod((G9*p1)/.y) by A30,CAT_3:def 2
            .= (cods(G9*p1))/.y by A35,CAT_3:def 2
            .= G/.y by A13,A17,A23,CAT_3:16
            .= G.y by A35,FUNCT_2:def 13
            .= F.y by A30,A33,FUNCT_1:49,ZFMISC_1:56
            .= F/.y by A30,FUNCT_2:def 13;
        end;
      end;
      hence (cods F9)/.y = F/.y;
    end;
    hence
 cods F9 = F by CAT_3:1;
    thus F9 is Projections_family of c,I;
    let d be Object of C;
    let F99 be Projections_family of d,I such that
A36: cods F9 = cods F99;
    reconsider G99 = F99|(I\{x}) as Function of I\{x},the carrier' of C by
FUNCT_2:32;
 now
      let y be set;
      assume
A37:  y in I\{x};
      then G99/.y = G99.y by FUNCT_2:def 13
        .= F99.y by A37,FUNCT_1:49
        .= F99/.y by A37,FUNCT_2:def 13;
      hence doms(G99)/.y = dom(F99/.y) by A37,CAT_3:def 1
        .= d by A37,CAT_3:41
        .= ((I\{x})-->d)/.y by A37,CAT_3:2;
    end;
    then reconsider G99 as Projections_family of d,I\{x}
               by CAT_3:1,def 13;
    now
      let y be set;
      assume
A38:  y in I\{x};
      then
A39:  G/.y = G.y by FUNCT_2:def 13
        .= F.y by A38,FUNCT_1:49
        .= F/.y by A38,FUNCT_2:def 13;
      F99/.y = F99.y by A38,FUNCT_2:def 13
        .= G99.y by A38,FUNCT_1:49
        .= G99/.y by A38,FUNCT_2:def 13;
      hence (cods G9)/.y = cod(G99/.y)
            by A13,A36,A38,A39,A29,CAT_3:1,def 2
        .= (cods G99)/.y by A38,CAT_3:def 2;
    end;
    then consider h9 being Morphism of C such that
A40: h9 in Hom(d,a) and
A41: for k being Morphism of C st k in Hom(d,a) holds (for y being set
    st y in I\{x} holds (G9/.y)(*)k = G99/.y) iff h9 = k by A14,CAT_3:1;
A42: x in {x} by TARSKI:def 1;
    set g = F99/.x;
A43: dom g = d by A12,CARD_1:27,CAT_3:41;
A44: F9/.x = F9.x by A12,CARD_1:27,FUNCT_2:def 13
      .= (x .-->p2).x by A20,A42,FUNCT_4:13
      .= p2 by A42,FUNCOP_1:7;
    then cod p2 = (cods F9)/.x by A12,CARD_1:27,CAT_3:def 2
      .= cod g by A12,A36,CARD_1:27,CAT_3:def 2;
    then g in Hom(d,cod p2) by A43;
    then consider h being Morphism of C such that
A45: h in Hom(d,c) and
A46: for k being Morphism of C st k in Hom(d,c) holds p1(*)k = h9 & p2(*)k
    = g iff h = k by A17,A19,A40;
    take h;
    thus h in Hom(d,c) by A45;
    let k be Morphism of C such that
A47: k in Hom(d,c);
    thus (for y being set st y in I holds (F9/.y)(*)k = F99/.y) implies h = k
    proof
A48:  cod k = c by A47,CAT_1:1;
      then
A49:  cod(p1(*)k) = a by A15,A17,CAT_1:17;
      assume
A50:  for y being set st y in I holds (F9/.y)(*)k = F99/.y;
A51:  for y being set st y in I\{x} holds (G9/.y)(*)(p1(*)k) = G99/.y
      proof
        let y be set;
        assume
A52:    y in I\{x};
        then
A53:    not y in {x} by XBOOLE_0:def 5;
A54:    F9/.y = F9.y by A52,FUNCT_2:def 13
          .= (G9*p1).y by A20,A22,A52,A53,FUNCT_4:def 1
          .= (G9*p1)/.y by A52,FUNCT_2:def 13;
        dom(G9/.y) = a by A52,CAT_3:41;
        hence (G9/.y)(*)(p1(*)k) = ((G9/.y)(*)p1)(*)k by A15,A17,A48,CAT_1:18
          .= ((G9*p1)/.y)(*)k by A52,CAT_3:def 5
          .= F99/.y by A50,A52,A54
          .= F99.y by A52,FUNCT_2:def 13
          .= G99.y by A52,FUNCT_1:49
          .= G99/.y by A52,FUNCT_2:def 13;
      end;
      dom k = d by A47,CAT_1:1;
      then dom(p1(*)k) = d by A15,A48,CAT_1:17;
      then p1(*)k in Hom(d,a) by A49;
      then
A55:  p1(*)k = h9 by A41,A51;
      p2(*)k = g by A12,A44,A50,CARD_1:27;
      hence thesis by A46,A47,A55;
    end;
    assume
A56: h = k;
    let y be set such that
A57: y in I;
    now
      per cases;
      suppose
A58:    y = x;
        then
A59:    y in {x} by TARSKI:def 1;
        F9/.y = F9.y by A57,FUNCT_2:def 13
          .= (x .-->p2).y by A20,A59,FUNCT_4:13
          .= p2 by A59,FUNCOP_1:7;
        hence thesis by A46,A47,A56,A58;
      end;
      suppose
A60:    y <> x;
        then
A61:    not y in {x} by TARSKI:def 1;
A62:    cod k = c by A47,CAT_1:1;
A63:    y in I\{x} by A57,A60,ZFMISC_1:56;
A64:    dom(G9/.y) = a by A57,A60,CAT_3:41,ZFMISC_1:56;
        F9/.y = F9.y by A57,FUNCT_2:def 13
          .= (G9*p1).y by A20,A22,A57,A61,FUNCT_4:def 1
          .= (G9*p1)/.y by A63,FUNCT_2:def 13
          .= (G9/.y)(*)p1 by A63,CAT_3:def 5;
        hence (F9/.y)(*)k = (G9/.y)(*)(p1(*)k) by A15,A17,A62,A64,CAT_1:18
          .= (G9/.y)(*)h9 by A46,A47,A56
          .= G99/.y by A40,A41,A63
          .= G99.y by A63,FUNCT_2:def 13
          .= F99.y by A57,A60,FUNCT_1:49,ZFMISC_1:56
          .= F99/.y by A57,FUNCT_2:def 13;
      end;
    end;
    hence thesis;
  end;
  let I be finite set, F be Function of I,the carrier of C;
A65: card I = card I;
A66: Q[ 0 ]
  proof
    let I be finite set, F be Function of I,the carrier of C;
    assume card I = 0;
    then
A67: I = {};
    {} is Function of {}, the carrier' of C by RELSET_1:12;
    then reconsider F9 = {} as Projections_family of a,I by A67,CAT_3:42;
    take a,F9;
    for x being set st x in I holds (cods F9)/.x = F/.x;
    hence cods F9 = F by CAT_3:1;
    thus thesis by A8,A67,CAT_3:50;
  end;
  for n being Nat holds Q[n] from NAT_1:sch 2(A66,A10);
  hence thesis by A65;
end;

definition
  struct (CatStr)ProdCatStr (# carrier,carrier' -> set, Source,Target ->
Function of the carrier', the carrier, Comp -> PartFunc of [:the carrier', the
    carrier' :],the carrier',
TerminalObj -> Element of the carrier, CatProd -> Function of [:the carrier,the
carrier:],the carrier, Proj1,Proj2 -> Function of [:the carrier,the carrier:],
    the carrier' #);
end;

registration
  cluster non void non empty for ProdCatStr;
  existence
  proof
    set o = the set;
    take ProdCatStr(# {o},{o},o:->o,o:->o,(o,o):->o,Extract(o),(o,o):->
      o,(o,o):->o,(o,o):->o #);
    thus thesis;
  end;
end;

definition
  let C be non void non empty ProdCatStr;
  func [1]C -> Object of C equals
  the TerminalObj of C;
  correctness;
  let a,b be Object of C;
  func a[x]b -> Object of C equals
  (the CatProd of C).(a,b);
  correctness;
  func pr1(a,b) -> Morphism of C equals
  (the Proj1 of C).(a,b);
  correctness;
  func pr2(a,b) -> Morphism of C equals
  (the Proj2 of C).(a,b);
  correctness;
end;

definition
  let o,m;
  func c1Cat(o,m) -> strict ProdCatStr equals
  ProdCatStr(# {o},{m},m:->o,m:->o,(m,m):->m,
  Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #);
  correctness;
end;

registration let o,m be set;
 cluster c1Cat(o,m) -> non empty trivial non void trivial';
 coherence;
end;

theorem
  the CatStr of c1Cat(o,m) = 1Cat(o,m);

Lm1: c1Cat(o,m) is Category-like
proof
  set C = c1Cat(o,m);
  set CP = the Comp of C, CD = the Source of C, CC = the Target of C;
  thus
 for f,g being Morphism of C holds [g,f] in dom CP iff dom g = cod f
  proof
    let f,g be Morphism of C;
A1: dom CP = {[m,m]} by FUNCOP_1:13;
    f = m & g = m by TARSKI:def 1;
    hence thesis by A1,TARSKI:def 1;
  end;
end;

registration
  cluster strict Category-like reflexive transitive
   associative with_identities
   non void non empty for non void non empty ProdCatStr;
  existence
  proof
    c1Cat(0,1) is Category-like transitive reflexive associative
     with_identities by Lm1;
    hence thesis;
  end;
end;

registration
  let o,m be set;
  cluster c1Cat(o,m) -> Category-like reflexive transitive
   associative with_identities non empty non void;
  coherence by Lm1;
end;

theorem Th3:
  for a,b being Object of c1Cat(o,m) holds a = b
proof
  let a,b be Object of c1Cat(o,m);
  a = o by TARSKI:def 1;
  hence thesis by TARSKI:def 1;
end;

theorem Th4:
  for f,g being Morphism of c1Cat(o,m) holds f = g
proof
  let f,g be Morphism of c1Cat(o,m);
  f = m by TARSKI:def 1;
  hence thesis by TARSKI:def 1;
end;

theorem Th5:
  for a,b being Object of c1Cat(o,m), f being Morphism of c1Cat(o,m
  ) holds f in Hom(a,b)
proof
  let a,b be Object of c1Cat(o,m), f be Morphism of c1Cat(o,m);
  cod f = o by TARSKI:def 1;
  then
A1: cod f = b by TARSKI:def 1;
  dom f = o by TARSKI:def 1;
  then dom f = a by TARSKI:def 1;
  hence thesis by A1;
end;

theorem
  for a,b being Object of c1Cat(o,m), f being Morphism of c1Cat(o,m)
  holds f is Morphism of a,b
proof
  let a,b be Object of c1Cat(o,m), f be Morphism of c1Cat(o,m);
  f in Hom(a,b) by Th5;
  hence thesis by CAT_1:def 5;
end;

theorem
  for a,b being Object of c1Cat(o,m) holds Hom(a,b) <> {} by Th5;

theorem Th8:
  for a being Object of c1Cat(o,m) holds a is terminal
proof
  let a be Object of c1Cat(o,m);
  let b be Object of c1Cat(o,m);
  set f = the Morphism of b,a;
  thus Hom(b,a)<>{} by Th5;
  take f;
  thus thesis by Th4;
end;

theorem Th9:
  for c being Object of c1Cat(o,m), p1,p2 being Morphism of c1Cat(
  o,m) holds c is_a_product_wrt p1,p2
proof
  let c be Object of c1Cat(o,m), p1,p2 be Morphism of c1Cat(o,m);
  thus dom p1 = c & dom p2 = c by Th3;
  let d be Object of c1Cat(o,m),f,g be Morphism of c1Cat(o,m) such that
  f in Hom(d,cod p1) and
  g in Hom(d,cod p2);
  take h = p1;
  thus h in Hom(d,c) by Th5;
  thus thesis by Th4;
end;

definition
  let IT be Category-like reflexive transitive
    associative with_identities
    non void non empty ProdCatStr;
  attr IT is Cartesian means
  :Def8:
  the TerminalObj of IT is terminal & for a,
b being Object of IT holds cod((the Proj1 of IT).(a,b)) = a & cod((the Proj2 of
IT).(a,b)) = b & (the CatProd of IT).(a,b) is_a_product_wrt (the Proj1 of IT).(
  a,b),(the Proj2 of IT).(a,b);
end;

theorem Th10:
  for o,m being set holds c1Cat(o,m) is Cartesian
by Th8,Th3,Th9;

registration
  cluster strict Cartesian
  for Category-like reflexive transitive associative with_identities
   non void non empty ProdCatStr;
  existence
  proof
    c1Cat(0,1) is Cartesian by Th10;
    hence thesis;
  end;
end;

definition
  mode Cartesian_category is Cartesian
   Category-like non void non empty
     reflexive transitive associative with_identities
   non void non empty
    ProdCatStr;
end;

reserve C for Cartesian_category;
reserve a,b,c,d,e,s for Object of C;

theorem
  [1]C is terminal by Def8;

theorem Th12:
  for f1,f2 being Morphism of a,[1]C holds f1 = f2
proof
  let f1,f2 be Morphism of a,[1]C;
  [1]C is terminal by Def8;
  then consider f being Morphism of a,[1]C such that
A1: for g being Morphism of a,[1]C holds f = g;
  thus f1 = f by A1
    .= f2 by A1;
end;

theorem Th13:
  Hom(a,[1]C) <> {}
proof
  [1]C is terminal by Def8;
  hence thesis;
end;

definition
  let C,a;
  func term(a) -> Morphism of a,[1]C means
  not contradiction;
  existence;
  uniqueness by Th12;
end;

theorem Th14:
  term a = term(a,[1]C)
proof
  [1]C is terminal by Def8;
  hence thesis by CAT_3:37;
end;

theorem
  dom(term a) = a & cod(term a) = [1]C
proof
  [1]C is terminal & term a = term(a,[1]C) by Def8,Th14;
  hence thesis by CAT_3:35;
end;

theorem
  Hom(a,[1]C) = {term a}
proof
  for f2 being Morphism of a,[1]C holds term a = f2 by Th12;
  hence thesis by Th13,CAT_1:8;
end;

theorem Th17:
  dom pr1(a,b) = a[x]b & cod pr1(a,b) = a
proof
  set p1 = (the Proj1 of C).(a,b), p2 = (the Proj2 of C).(a,b);
  a[x]b is_a_product_wrt p1,p2 by Def8;
  hence thesis by Def8;
end;

theorem Th18:
  dom pr2(a,b) = a[x]b & cod pr2(a,b) = b
proof
  set p1 = (the Proj1 of C).(a,b), p2 = (the Proj2 of C).(a,b);
  a[x]b is_a_product_wrt p1,p2 by Def8;
  hence thesis by Def8;
end;

definition
  let C,a,b;
  redefine func pr1(a,b) -> Morphism of a[x]b,a;
  coherence
  proof
    dom pr1(a,b) = a[x]b & cod pr1(a,b) = a by Th17;
    hence thesis by CAT_1:4;
  end;
  redefine func pr2(a,b) -> Morphism of a[x]b,b;
  coherence
  proof
    dom pr2(a,b) = a[x]b & cod pr2(a,b) = b by Th18;
    hence thesis by CAT_1:4;
  end;
end;

theorem Th19:
  Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {}
proof
  set c = (the CatProd of C).(a,b), p1 = (the Proj1 of C).(a,b), p2 = (the
  Proj2 of C).(a,b);
  c is_a_product_wrt p1,p2 by Def8;
  then
A1: dom p1 = c & dom p2 = c;
  cod(p1) = a & cod(p2) = b by Def8;
  hence thesis by A1,CAT_1:1;
end;

theorem
  a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Def8;

theorem
  C is with_finite_product
proof
A1: for a,b ex c being Object of C, p1,p2 being Morphism of C st dom p1 = c
  & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2
  proof
    let a,b;
    take a[x]b, pr1(a,b), pr2(a,b);
    thus thesis by Def8,Th17,Th18;
  end;
  [1]C is terminal by Def8;
  hence thesis by A1,Th1;
end;

theorem
  Hom(a,b) <> {} & Hom(b,a) <> {}
  implies pr1(a,b) is retraction & pr2(a,b) is retraction
proof
A1: Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19;
  a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) & cod pr1(a,b) = a by Def8;
  hence thesis by A1,CAT_3:57;
end;

definition
  let C,a,b,c;
  let f be Morphism of c,a, g be Morphism of c,b;
  assume
A1: Hom(c,a) <> {} & Hom(c,b) <> {};
  func <:f,g:> -> Morphism of c,a[x]b means
  :Def10:
  pr1(a,b)*it = f & pr2(a,b) *it = g;
  existence
  proof
A2: a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Def8;
    Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19;
    then consider h being Morphism of c,a[x]b such that
A3: for h1 being Morphism of c,a[x]b holds pr1(a,b)*h1 = f & pr2(a,b)*
    h1 = g iff h = h1 by A1,A2,CAT_3:55;
    take h;
    thus thesis by A3;
  end;
  uniqueness
  proof
A4: a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Def8;
    Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19;
    then consider h being Morphism of c,a[x]b such that
A5: for h1 being Morphism of c,a[x]b holds pr1(a,b)*h1 = f & pr2(a,b)*
    h1 = g iff h = h1 by A1,A4,CAT_3:55;
    let h1,h2 be Morphism of c,a[x]b such that
A6: pr1(a,b)*h1 = f & pr2(a,b)*h1 = g and
A7: pr1(a,b)*h2 = f & pr2(a,b)*h2 = g;
    h1 = h by A6,A5;
    hence thesis by A7,A5;
  end;
end;

theorem Th23:
  Hom(c,a) <> {} & Hom(c,b) <> {} implies Hom(c,a[x]b) <> {}
proof
A1: a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Def8;
  Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19;
  hence thesis by A1,CAT_3:55;
end;

theorem Th24:
  <:pr1(a,b),pr2(a,b):> = id(a[x]b)
proof
A1: Hom(a[x]b,b) <> {} by Th19;
  then
A2: pr2(a,b)*(id(a[x]b)) = pr2(a,b) by CAT_1:29;
A3: Hom(a[x]b,a) <> {} by Th19;
  then pr1(a,b)*(id(a[x]b)) = pr1(a,b) by CAT_1:29;
  hence thesis by A3,A1,A2,Def10;
end;

theorem Th25:
  for f being Morphism of c,a, g being Morphism of c,b, h being
Morphism of d,c st Hom(c,a)<>{} & Hom(c,b)<>{} & Hom(d,c)<>{} holds <:f*h,g*h:>
  = <:f,g:>*h
proof
  let f be Morphism of c,a, g be Morphism of c,b, h be Morphism of d,c;
  assume that
A1: Hom(c,a)<>{} & Hom(c,b)<>{} and
A2: Hom(d,c)<>{};
A3: Hom(c,a[x]b) <> {} by A1,Th23;
A4: Hom(a[x]b,b) <> {} by Th19;
  (pr2(a,b)*<:f,g:>)*h = g*h by A1,Def10;
  then
A5: pr2(a,b)*(<:f,g:>*h) = g*h by A2,A4,A3,CAT_1:25;
A6: Hom(a[x]b,a) <> {} by Th19;
A7: Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,CAT_1:24;
  (pr1(a,b)*<:f,g:>)*h = f*h by A1,Def10;
  then pr1(a,b)*(<:f,g:>*h) = f*h by A2,A6,A3,CAT_1:25;
  hence thesis by A5,A7,Def10;
end;

theorem Th26:
  for f,k being Morphism of c,a, g,h being Morphism of c,b st Hom(
  c,a) <> {} & Hom(c,b) <> {} & <:f,g:> = <:k,h:> holds f = k & g = h
proof
  let f,k be Morphism of c,a, g,h be Morphism of c,b;
  assume
A1: Hom(c,a) <> {} & Hom(c,b) <> {};
  then pr1(a,b)*<:f,g:> = f & pr2(a,b)*<:f,g:> = g by Def10;
  hence thesis by A1,Def10;
end;

theorem
  for f being Morphism of c,a, g being Morphism of c,b st Hom(c,a) <> {}
  & Hom(c,b) <> {} & (f is monic or g is monic) holds <:f,g:> is monic
proof
  let f be Morphism of c,a, g be Morphism of c,b;
  assume that
A1: Hom(c,a) <> {} and
A2: Hom(c,b) <> {} and
A3: f is monic or g is monic;
A4: now
    assume
A5: g is monic;
    let d be Object of C, f1,f2 be Morphism of d,c such that
A6: Hom(d,c)<>{} and
A7: <:f,g:>*f1 = <:f,g:>*f2;
A8: Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A6,CAT_1:24;
    <:f*f1,g*f1:> = <:f,g:>*f1 & <:f*f2,g*f2:> = <:f,g:>*f2 by A1,A2,A6,Th25;
    then g*f1 = g*f2 by A7,A8,Th26;
    hence f1 = f2 by A5,A6;
  end;
A9: now
    assume
A10: f is monic;
    let d;
    let f1,f2 be Morphism of d,c such that
A11: Hom(d,c)<>{} and
A12: <:f,g:>*f1 = <:f,g:>*f2;
A13: Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A11,CAT_1:24;
    <:f*f1,g*f1:> = <:f,g:>*f1 & <:f*f2,g*f2:> = <:f,g:>*f2 by A1,A2,A11,Th25;
    then f*f1 = f*f2 by A12,A13,Th26;
    hence f1 = f2 by A10,A11;
  end;
  Hom(c,a[x]b) <> {} by A1,A2,Th23;
  hence thesis by A3,A9,A4;
end;

theorem Th28:
  Hom(a,a[x][1]C) <> {} & Hom(a,[1]C[x]a) <> {}
proof
  Hom(a,[1]C) <> {} & Hom(a,a) <> {} by Th13;
  hence thesis by Th23;
end;

definition
  let C,a;
  func lambda(a) -> Morphism of [1]C[x]a,a equals
  pr2([1]C,a);
  correctness;
  func lambda'(a) -> Morphism of a,[1]C[x]a equals
  <:term a,id a:>;
  correctness;
  func rho(a) -> Morphism of a[x][1]C,a equals
  pr1(a,[1]C);
  correctness;
  func rho'(a) -> Morphism of a,a[x][1]C equals
  <:id a,term a:>;
  correctness;
end;

theorem Th29:
  lambda(a)*lambda'(a) = id a & lambda'(a)*lambda(a) = id([1]C[x]a
  ) & rho(a)*rho'(a) = id a & rho'(a)*rho(a) = id(a[x][1]C)
proof
A1: (term a)*pr2([1]C,a) = pr1([1]C,a) by Th12;
A2: Hom(a,[1]C) <> {} & Hom(a,a) <> {} by Th13;
  hence id a = lambda(a)*lambda'(a) by Def10;
A3: Hom([1]C[x]a,a) <> {} by Th19;
  then (id a)*pr2([1]C,a) = pr2([1]C,a) by CAT_1:28;
  then <:term a,id a:>*pr2([1]C,a) = <:pr1([1]C,a),pr2([1]C,a):> by A2,A3,A1
,Th25;
  hence id([1]C[x]a) = lambda'(a)*lambda(a) by Th24;
  thus id a = rho(a)*rho'(a) by A2,Def10;
A4: (term a)*pr1(a,[1]C) = pr2(a,[1]C) by Th12;
A5: Hom(a[x][1]C,a) <> {} by Th19;
  then (id a)*pr1(a,[1]C) = pr1(a,[1]C) by CAT_1:28;
  then <:id a,term a:>*pr1(a,[1]C) = <:pr1(a,[1]C),pr2(a,[1]C):> by A2,A5,A4
,Th25;
  hence thesis by Th24;
end;

theorem
  a, a[x][1]C are_isomorphic & a,[1]C[x]a are_isomorphic
proof
  thus a,a[x][1]C are_isomorphic
  proof
    thus Hom(a,a[x][1]C) <> {} & Hom(a[x][1]C,a) <> {} by Th19,Th28;
    take rho'(a), rho(a);
    thus thesis by Th29;
  end;
  thus Hom(a,[1]C[x]a) <> {} & Hom([1]C[x]a,a) <> {} by Th19,Th28;
  take lambda'(a), lambda(a);
  thus thesis by Th29;
end;

definition
  let C,a,b;
  func Switch(a,b) -> Morphism of a[x]b,b[x]a equals
  <:pr2(a,b),pr1(a,b):>;
  correctness;
end;

theorem Th31:
  Hom(a[x]b,b[x]a)<>{}
proof
  Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19;
  hence thesis by Th23;
end;

theorem Th32:
  Switch(a,b)*Switch(b,a) = id(b[x]a)
proof
A1: Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th19;
A2: Hom(b[x]a,b) <> {} & Hom(b[x]a,a) <> {} by Th19;
  then Hom(b[x]a,a[x]b)<>{} by Th23;
  hence Switch(a,b)*Switch(b,a) = <:pr2(a,b)*<:pr2(b,a),pr1(b,a):>,pr1(a,b)*<:
  pr2(b,a),pr1(b,a):>:> by A1,Th25
    .= <:pr1(b,a),pr1(a,b)*<:pr2(b,a),pr1(b,a):>:> by A2,Def10
    .= <:pr1(b,a),pr2(b,a):> by A2,Def10
    .= id(b[x]a) by Th24;
end;

theorem
  a[x]b,b[x]a are_isomorphic
proof
  thus Hom(a[x]b,b[x]a)<>{} & Hom(b[x]a,a[x]b)<>{} by Th31;
  take Switch(a,b), Switch(b,a);
  thus thesis by Th32;
end;

definition
  let C,a;
  func Delta a -> Morphism of a,a[x]a equals
  <:id a,id a:>;
  correctness;
end;

theorem
  Hom(a,a[x]a) <> {}
proof
  Hom(a,a) <> {};
  hence thesis by Th23;
end;

theorem
  for f being Morphism of a,b st Hom(a,b) <> {} holds <:f,f:> = Delta(b) *f
proof
  let f be Morphism of a,b such that
A1: Hom(a,b) <> {};
  Hom(b,b) <> {} & (id b)*f = f by A1,CAT_1:28;
  hence thesis by A1,Th25;
end;

definition
  let C,a,b,c;
  func Alpha(a,b,c) -> Morphism of (a[x]b)[x]c,a[x](b[x]c) equals
  <:pr1(a,b)*
  pr1(a[x]b,c),<:pr2(a,b)*pr1(a[x]b,c),pr2(a[x]b,c):>:>;
  correctness;
  func Alpha'(a,b,c) -> Morphism of a[x](b[x]c),(a[x]b)[x]c equals
  <:<:pr1(a,b
  [x]c),pr1(b,c)*pr2(a,b[x]c):>,pr2(b,c)*pr2(a,b[x]c):>;
  correctness;
end;

theorem Th36:
  Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} & Hom(a[x](b[x]c),(a[x]b)[x]c ) <> {}
proof
A1: Hom((a[x]b)[x]c,a[x]b) <> {} by Th19;
  Hom(a[x]b,b) <> {} by Th19;
  then
A2: Hom((a[x]b)[x]c,b) <> {} by A1,CAT_1:24;
  Hom(a[x]b,a) <> {} by Th19;
  then
A3: Hom((a[x]b)[x]c,a) <> {} by A1,CAT_1:24;
  Hom((a[x]b)[x]c,c) <> {} by Th19;
  then Hom((a[x]b)[x]c,b[x]c) <> {} by A2,Th23;
  hence Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} by A3,Th23;
A4: Hom(a[x](b[x]c),b[x]c) <> {} by Th19;
  Hom(b[x]c,c) <> {} by Th19;
  then
A5: Hom(a[x](b[x]c),c) <> {} by A4,CAT_1:24;
  Hom(b[x]c,b) <> {} by Th19;
  then
A6: Hom(a[x](b[x]c),b) <> {} by A4,CAT_1:24;
  Hom(a[x](b[x]c),a) <> {} by Th19;
  then Hom(a[x](b[x]c),a[x]b) <> {} by A6,Th23;
  hence thesis by A5,Th23;
end;

theorem Th37:
  Alpha(a,b,c)*Alpha'(a,b,c) = id(a[x](b[x]c)) & Alpha'(a,b,c)*
  Alpha(a,b,c) = id((a[x]b)[x]c)
proof
  set k = <:pr2(a,b)*pr1(a[x]b,c),pr2(a[x]b,c):>;
  set l = <:pr1(a,b[x]c),pr1(b,c)*pr2(a,b[x]c):>;
  set f = <:pr1(a,b)*pr1(a[x]b,c),k:>;
  set g = <:l,pr2(b,c)*pr2(a,b[x]c):>;
A1: Hom((a[x]b)[x]c,a[x]b) <> {} by Th19;
A2: Hom(a[x]b,b) <> {} by Th19;
  then
A3: Hom((a[x]b)[x]c,b) <> {} by A1,CAT_1:24;
A4: Hom((a[x]b)[x]c,c) <> {} by Th19;
  then
A5: Hom((a[x]b)[x]c,b[x]c) <> {} by A3,Th23;
A6: Hom(a[x]b,a) <> {} by Th19;
  then
A7: Hom((a[x]b)[x]c,a) <> {} by A1,CAT_1:24;
A8: Hom(a[x](b[x]c),b[x]c) <> {} by Th19;
A9: Hom(b[x]c,c) <> {} by Th19;
  then
A10: Hom(a[x](b[x]c),c) <> {} by A8,CAT_1:24;
A11: Hom(b[x]c,b) <> {} by Th19;
  then
A12: Hom(a[x](b[x]c),b) <> {} by A8,CAT_1:24;
A13: Hom(a[x](b[x]c),a) <> {} by Th19;
  then
A14: Hom(a[x](b[x]c),a[x]b) <> {} by A12,Th23;
A15: Hom(a[x](b[x]c),(a[x]b)[x]c) <> {} by Th36;
  then pr2(a,b)*pr1(a[x]b,c)*g = pr2(a,b)*(pr1(a[x]b,c)*g) by A1,A2,CAT_1:25
    .= pr2(a,b)*l by A10,A14,Def10
    .= pr1(b,c)*pr2(a,b[x]c) by A12,A13,Def10;
  then
A16: k*g = <:pr1(b,c)*pr2(a,b[x]c),pr2(a[x]b,c)*g:> by A3,A4,A15,Th25
    .= <:pr1(b,c)*pr2(a,b[x]c),pr2(b,c)*pr2(a,b[x]c):> by A10,A14,Def10
    .= <:pr1(b,c),pr2(b,c):>*pr2(a,b[x]c) by A11,A8,A9,Th25
    .= id(b[x]c)*pr2(a,b[x]c) by Th24
    .= pr2(a,b[x]c) by A8,CAT_1:28;
A17: Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} by Th36;
  then pr1(b,c)*pr2(a,b[x]c)*f = pr1(b,c)*(pr2(a,b[x]c)*f) by A11,A8,CAT_1:25
    .= pr1(b,c)*k by A7,A5,Def10
    .= pr2(a,b)*pr1(a[x]b,c) by A3,A4,Def10;
  then
A18: l*f = <:pr1(a,b[x]c)*f,pr2(a,b)*pr1(a[x]b,c):> by A17,A12,A13,Th25
    .= <:pr1(a,b)*pr1(a[x]b,c),pr2(a,b)*pr1(a[x]b,c):> by A7,A5,Def10
    .= <:pr1(a,b),pr2(a,b):>*pr1(a[x]b,c) by A6,A1,A2,Th25
    .= id(a[x]b)*pr1(a[x]b,c) by Th24
    .= pr1(a[x]b,c) by A1,CAT_1:28;
  pr1(a,b)*pr1(a[x]b,c)*g = pr1(a,b)*(pr1(a[x]b,c)*g) by A6,A1,A15,CAT_1:25
    .= pr1(a,b)*l by A10,A14,Def10
    .= pr1(a,b[x]c) by A12,A13,Def10;
  hence
  Alpha(a,b,c)*Alpha'(a,b,c) = <:pr1(a,b[x]c),pr2(a,b[x]c):> by A7,A5,A15,A16
,Th25
    .= id(a[x](b[x]c)) by Th24;
  pr2(b,c)*pr2(a,b[x]c)*f = pr2(b,c)*(pr2(a,b[x]c)*f) by A17,A8,A9,CAT_1:25
    .= pr2(b,c)*k by A7,A5,Def10
    .= pr2(a[x]b,c) by A3,A4,Def10;
  hence Alpha'(a,b,c)*Alpha(a,b,c) = <:pr1(a[x]b,c),pr2(a[x]b,c):> by A17,A10
,A14,A18,Th25
    .= id((a[x]b)[x]c) by Th24;
end;

theorem
  (a[x]b)[x]c,a[x](b[x]c) are_isomorphic
proof
  thus Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} & Hom(a[x](b[x]c),(a[x]b)[x]c) <> {}
  by Th36;
  take Alpha(a,b,c), Alpha'(a,b,c);
  thus thesis by Th37;
end;

definition
  let C,a,b,c,d;
  let f be Morphism of a,b, g be Morphism of c,d;
  func f[x]g -> Morphism of a[x]c,b[x]d equals
  <:f*pr1(a,c),g*pr2(a,c):>;
  correctness;
end;

theorem
  Hom(a,c) <> {} & Hom(b,d) <> {} implies Hom(a[x]b,c[x]d) <> {}
proof
  assume that
A1: Hom(a,c) <> {} and
A2: Hom(b,d) <> {};
  Hom(a[x]b,b) <> {} by Th19;
  then
A3: Hom(a[x]b,d) <> {} by A2,CAT_1:24;
  Hom(a[x]b,a) <> {} by Th19;
  then Hom(a[x]b,c) <> {} by A1,CAT_1:24;
  hence thesis by A3,Th23;
end;

theorem
  (id a)[x](id b) = id(a[x]b)
proof
  Hom(a[x]b,b) <> {} by Th19;
  then
A1: (id b)*pr2(a,b) = pr2(a,b) by CAT_1:28;
  Hom(a[x]b,a) <> {} by Th19;
  then (id a)*pr1(a,b) = pr1(a,b) by CAT_1:28;
  hence thesis by A1,Th24;
end;

theorem Th41:
  for f being Morphism of a,b, h being Morphism of c,d, g being
  Morphism of e,a, k being Morphism of e,c st Hom(a,b) <> {} & Hom(c,d) <> {} &
  Hom(e,a) <> {} & Hom(e,c) <> {} holds (f[x]h)*<:g,k:> = <:f*g,h*k:>
proof
  let f be Morphism of a,b, h be Morphism of c,d;
  let g be Morphism of e,a, k be Morphism of e,c;
  assume that
A1: Hom(a,b) <> {} and
A2: Hom(c,d) <> {} and
A3: Hom(e,a) <> {} & Hom(e,c) <> {};
A4: Hom(e,a[x]c) <> {} by A3,Th23;
A5: Hom(a[x]c,c) <> {} by Th19;
  then
A6: Hom(a[x]c,d) <> {} by A2,CAT_1:24;
A7: Hom(a[x]c,a) <> {} by Th19;
  then
A8: Hom(a[x]c,b) <> {} by A1,CAT_1:24;
  pr2(a,c)*<:g,k:> = k by A3,Def10;
  then
A9: h*k = (h*pr2(a,c))*<:g,k:> by A2,A4,A5,CAT_1:25;
  pr1(a,c)*<:g,k:> = g by A3,Def10;
  then f*g = (f*pr1(a,c))*<:g,k:> by A1,A4,A7,CAT_1:25;
  hence thesis by A4,A8,A6,A9,Th25;
end;

theorem
  for f being Morphism of c,a, g being Morphism of c,b st Hom(c,a) <> {}
  & Hom(c,b) <> {} holds <:f,g:> = (f[x]g)*Delta(c)
proof
  let f be Morphism of c,a, g be Morphism of c,b such that
A1: Hom(c,a) <> {} and
A2: Hom(c,b) <> {};
  Hom(c,c) <> {};
  hence (f[x]g)*Delta(c) = <:f*(id c),g*(id c):> by A1,A2,Th41
    .= <:f,g*(id c):> by A1,CAT_1:29
    .= <:f,g:> by A2,CAT_1:29;
end;

theorem
  for f being Morphism of a,b, h being Morphism of c,d, g being Morphism
  of e,a, k being Morphism of s,c st Hom(a,b) <> {} & Hom(c,d) <> {} & Hom(e,a)
  <> {} & Hom(s,c) <> {} holds (f[x]h)*(g[x]k) = (f*g)[x](h*k)
proof
  let f be Morphism of a,b, h be Morphism of c,d;
  let g be Morphism of e,a, k be Morphism of s,c;
  assume that
A1: Hom(a,b) <> {} and
A2: Hom(c,d) <> {} and
A3: Hom(e,a) <> {} and
A4: Hom(s,c) <> {};
A5: Hom(e[x]s,s) <> {} by Th19;
  then
A6: Hom(e[x]s,c) <> {} by A4,CAT_1:24;
A7: Hom(e[x]s,e) <> {} by Th19;
  then f*(g*pr1(e,s)) = (f*g)*pr1(e,s) by A1,A3,CAT_1:25;
  then
A8: (f*g)[x](h*k) = <:f*(g*pr1(e,s)),h*(k*pr2(e,s)):> by A2,A4,A5,CAT_1:25;
  Hom(e[x]s,a) <> {} by A3,A7,CAT_1:24;
  hence thesis by A1,A2,A6,A8,Th41;
end;

begin :: Categories with Finite Coproducts

definition
  let C be Category;
  attr C is with_finite_coproduct means
  for I being finite set, F being
  Function of I,the carrier of C ex a being Object of C, F9 being
  Injections_family of a,I st doms F9 = F & a is_a_coproduct_wrt F9;
end;

theorem Th44:
  for C being Category holds C is with_finite_coproduct iff (ex a
  being Object of C st a is initial) & for a,b being Object of C ex c being
Object of C, i1,i2 being Morphism of C st dom i1 = a & dom i2 = b & cod i1 = c
  & cod i2 = c & c is_a_coproduct_wrt i1,i2
proof
  let C be Category;
  thus C is with_finite_coproduct implies (ex a being Object of C st a is
  initial) & for a,b being Object of C ex c being Object of C, i1,i2 being
  Morphism of C st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c
  is_a_coproduct_wrt i1,i2
  proof
    reconsider F = {} as Function of {},the carrier of C by RELSET_1:12;
A1: 0 in {0,1} by TARSKI:def 2;
    assume
A2: for I being finite set, F being Function of I,the carrier of C ex
    a being Object of C, F9 being Injections_family of a,I st doms F9 = F & a
    is_a_coproduct_wrt F9;
    then consider
    a being Object of C, F9 being Injections_family of a,{} such that
    doms F9 = F and
A3: a is_a_coproduct_wrt F9;
    thus ex a being Object of C st a is initial by A3,CAT_3:75;
    let a,b be Object of C;
    set F = (0,1)-->(a,b);
    consider c being Object of C, F9 being Injections_family of c,{0,1} such
    that
A4: doms F9 = F and
A5: c is_a_coproduct_wrt F9 by A2;
    take c, i1 = F9/.0, i2 = F9/.1;
A6: 1 in {0,1} by TARSKI:def 2;
    then
A7: i2 = F9.1 by FUNCT_2:def 13;
    F/.0 = a & F/.1 = b by CAT_3:3;
    hence dom i1 = a & dom i2 = b by A4,A1,A6,CAT_3:def 1;
    thus cod i1 = c & cod i2 = c by A1,A6,CAT_3:62;
    dom F9 = {0,1} & i1 = F9.0 by A1,FUNCT_2:def 1,def 13;
    then F9 = (0,1)-->(i1,i2) by A7,FUNCT_4:66;
    hence thesis by A5,CAT_3:79;
  end;
  given a being Object of C such that
A8: a is initial;
  defpred Q[Nat] means for I being finite set, F being Function of I,the
carrier of C st card I = $1 ex a being Object of C, F9 being Injections_family
  of a,I st doms F9 = F & a is_a_coproduct_wrt F9;
  assume
A9: for a,b being Object of C ex c being Object of C, i1,i2 being
  Morphism of C st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c
  is_a_coproduct_wrt i1,i2;
A10: for n being Nat st Q[n] holds Q[n+1]
  proof
    let n be Nat such that
A11: Q[n];
    let I be finite set, F be Function of I,the carrier of C such that
A12: card I = n+1;
    set x = the Element of I;
    reconsider Ix = I \ {x} as finite set;
    reconsider sx = {x} as finite set;
    reconsider G = F|(I\{x}) as Function of I\{x},the carrier of C by
FUNCT_2:32;
    card(Ix) = card(I) - card(sx) by A12,CARD_1:27,CARD_2:44,ZFMISC_1:31
      .= card(I) - 1 by CARD_1:30
      .= n by A12,XCMPLX_1:26;
    then consider
    a being Object of C, G9 being Injections_family of a,I\{x} such
    that
A13: doms G9 = G and
A14: a is_a_coproduct_wrt G9 by A11;
    set b = F/.x;
    consider c being Object of C, i1,i2 being Morphism of C such that
A15: dom i1 = a and
A16: dom i2 = b and
A17: cod i1 = c and
A18: cod i2 = c and
A19: c is_a_coproduct_wrt i1,i2 by A9;
    set F9 = (i1*G9) +* (x .-->i2);
A20: dom({x} -->i2) = {x} by FUNCT_2:def 1;
    rng F9 c= rng(i1*G9) \/ rng(x .-->i2) by FUNCT_4:17;
    then
A21: rng F9 c= the carrier' of C by XBOOLE_1:1;
    dom(i1*G9) = I\{x} by FUNCT_2:def 1;
    then
A22: dom(i1*G9) \/ dom(x .-->i2) = I \/ {x} by A20,XBOOLE_1:39
      .= I by A12,CARD_1:27,ZFMISC_1:40;
    then dom F9 = I by FUNCT_4:def 1;
    then reconsider F9 as Function of I, the carrier' of C by A21,FUNCT_2:def 1
,RELSET_1:4;
A23: cods G9 = (I\{x})-->a by CAT_3:def 16;
    now
      let y be object;
      assume
A24:  y in I;
      now
        per cases;
        suppose
          y = x;
          then
A25:      y in {x} by TARSKI:def 1;
          F9/.y = F9.y by A24,FUNCT_2:def 13
            .= (x .-->i2).y by A20,A25,FUNCT_4:13
            .= i2 by A25,FUNCOP_1:7;
          hence (I --> c).y = cod(F9/.y) by A18,A24,FUNCOP_1:7
            .= (cods F9)/.y by A24,CAT_3:def 2;
        end;
        suppose
A26:      y <> x;
          then
A27:      not y in {x} by TARSKI:def 1;
A28:      y in I\{x} by A24,A26,ZFMISC_1:56;
          F9/.y = F9.y by A24,FUNCT_2:def 13
            .= (i1*G9).y by A20,A22,A24,A27,FUNCT_4:def 1
            .= (i1*G9)/.y by A28,FUNCT_2:def 13;
          hence (cods F9)/.y = cod((i1*G9)/.y) by A24,CAT_3:def 2
            .= (cods(i1*G9))/.y by A28,CAT_3:def 2
            .= ((I\{x})-->c)/.y by A15,A17,A23,CAT_3:17
            .= c by A24,A26,CAT_3:2,ZFMISC_1:56
            .= (I --> c).y by A24,FUNCOP_1:7;
        end;
      end;
      hence (cods F9).y = (I --> c).y by A24,FUNCT_2:def 13;
    end;
    then reconsider F9 as Injections_family of c,I
               by CAT_3:def 16,FUNCT_2:12;
    take c,F9;
A29:  now
      let y be set;
      assume
A30:  y in I;
      now
        per cases;
        suppose
A31:      y = x;
          then
A32:      y in {x} by TARSKI:def 1;
          F9/.y = F9.y by A30,FUNCT_2:def 13
            .= (x .-->i2).y by A20,A32,FUNCT_4:13
            .= i2 by A32,FUNCOP_1:7;
          hence (doms F9)/.y = F/.y by A16,A30,A31,CAT_3:def 1;
        end;
        suppose
A33:      y <> x;
          then
A34:      not y in {x} by TARSKI:def 1;
A35:      y in I\{x} by A30,A33,ZFMISC_1:56;
          F9/.y = F9.y by A30,FUNCT_2:def 13
            .= (i1*G9).y by A20,A22,A30,A34,FUNCT_4:def 1
            .= (i1*G9)/.y by A35,FUNCT_2:def 13;
          hence (doms F9)/.y = dom((i1*G9)/.y) by A30,CAT_3:def 1
            .= (doms(i1*G9))/.y by A35,CAT_3:def 1
            .= G/.y by A13,A15,A23,CAT_3:17
            .= G.y by A35,FUNCT_2:def 13
            .= F.y by A30,A33,FUNCT_1:49,ZFMISC_1:56
            .= F/.y by A30,FUNCT_2:def 13;
        end;
      end;
      hence (doms F9)/.y = F/.y;
    end;
    hence
 doms F9 = F by CAT_3:1;
    thus F9 is Injections_family of c,I;
    let d be Object of C;
    let F99 be Injections_family of d,I such that
A36: doms F9 = doms F99;
    reconsider G99 = F99|(I\{x}) as Function of I\{x},the carrier' of C by
FUNCT_2:32;
    now
      let y be set;
      assume
A37:  y in I\{x};
      then G99/.y = G99.y by FUNCT_2:def 13
        .= F99.y by A37,FUNCT_1:49
        .= F99/.y by A37,FUNCT_2:def 13;
      hence cods(G99)/.y = cod(F99/.y) by A37,CAT_3:def 2
        .= d by A37,CAT_3:62
        .= ((I\{x})-->d)/.y by A37,CAT_3:2;
    end;
    then reconsider G99 as Injections_family of d,I\{x}
               by CAT_3:1,def 16;
    now
      let y be set;
      assume
A38:  y in I\{x};
      then
A39:  G/.y = G.y by FUNCT_2:def 13
        .= F.y by A38,FUNCT_1:49
        .= F/.y by A38,FUNCT_2:def 13;
      F99/.y = F99.y by A38,FUNCT_2:def 13
        .= G99.y by A38,FUNCT_1:49
        .= G99/.y by A38,FUNCT_2:def 13;
      hence (doms G9)/.y = dom(G99/.y) by A13,A29,A36,A38,A39,CAT_3:1,def 1
        .= (doms G99)/.y by A38,CAT_3:def 1;
    end;
    then consider h9 being Morphism of C such that
A40: h9 in Hom(a,d) and
A41: for k being Morphism of C st k in Hom(a,d) holds (for y being set
    st y in I\{x} holds k(*)(G9/.y) = G99/.y) iff h9 = k by A14,CAT_3:1;
A42: x in {x} by TARSKI:def 1;
    set g = F99/.x;
A43: cod g = d by A12,CARD_1:27,CAT_3:62;
A44: F9/.x = F9.x by A12,CARD_1:27,FUNCT_2:def 13
      .= (x .-->i2).x by A20,A42,FUNCT_4:13
      .= i2 by A42,FUNCOP_1:7;
    then dom i2 = (doms F9)/.x by A12,CARD_1:27,CAT_3:def 1
      .= dom g by A12,A36,CARD_1:27,CAT_3:def 1;
    then g in Hom(dom i2,d) by A43;
    then consider h being Morphism of C such that
A45: h in Hom(c,d) and
A46: for k being Morphism of C st k in Hom(c,d) holds k(*)i1 = h9 & k(*)i2
    = g iff h = k by A15,A19,A40;
    take h;
    thus h in Hom(c,d) by A45;
    let k be Morphism of C such that
A47: k in Hom(c,d);
    thus (for y being set st y in I holds k(*)(F9/.y) = F99/.y) implies h = k
    proof
A48:  dom k = c by A47,CAT_1:1;
      then
A49:  dom(k(*)i1) = a by A15,A17,CAT_1:17;
      assume
A50:  for y being set st y in I holds k(*)(F9/.y) = F99/.y;
A51:  for y being set st y in I\{x} holds k(*)i1(*)(G9/.y) = G99/.y
      proof
        let y be set;
        assume
A52:    y in I\{x};
        then
A53:    not y in {x} by XBOOLE_0:def 5;
A54:    F9/.y = F9.y by A52,FUNCT_2:def 13
          .= (i1*G9).y by A20,A22,A52,A53,FUNCT_4:def 1
          .= (i1*G9)/.y by A52,FUNCT_2:def 13;
        cod(G9/.y) = a by A52,CAT_3:62;
        hence k(*)i1(*)(G9/.y) = k(*)(i1(*)(G9/.y)) by A15,A17,A48,CAT_1:18
          .= k(*)((i1*G9)/.y) by A52,CAT_3:def 6
          .= F99/.y by A50,A52,A54
          .= F99.y by A52,FUNCT_2:def 13
          .= G99.y by A52,FUNCT_1:49
          .= G99/.y by A52,FUNCT_2:def 13;
      end;
      cod k = d by A47,CAT_1:1;
      then cod(k(*)i1) = d by A17,A48,CAT_1:17;
      then k(*)i1 in Hom(a,d) by A49;
      then
A55:  k(*)i1 = h9 by A41,A51;
      k(*)i2 = g by A12,A44,A50,CARD_1:27;
      hence thesis by A46,A47,A55;
    end;
    assume
A56: h = k;
    let y be set such that
A57: y in I;
    now
      per cases;
      suppose
A58:    y = x;
        then
A59:    y in {x} by TARSKI:def 1;
        F9/.y = F9.y by A57,FUNCT_2:def 13
          .= (x .-->i2).y by A20,A59,FUNCT_4:13
          .= i2 by A59,FUNCOP_1:7;
        hence thesis by A46,A47,A56,A58;
      end;
      suppose
A60:    y <> x;
        then
A61:    not y in {x} by TARSKI:def 1;
A62:    dom k = c by A47,CAT_1:1;
A63:    y in I\{x} by A57,A60,ZFMISC_1:56;
A64:    cod(G9/.y) = a by A57,A60,CAT_3:62,ZFMISC_1:56;
        F9/.y = F9.y by A57,FUNCT_2:def 13
          .= (i1*G9).y by A20,A22,A57,A61,FUNCT_4:def 1
          .= (i1*G9)/.y by A63,FUNCT_2:def 13
          .= i1(*)(G9/.y) by A63,CAT_3:def 6;
        hence k(*)(F9/.y) = k(*)i1(*)(G9/.y) by A15,A17,A62,A64,CAT_1:18
          .= h9(*)(G9/.y) by A46,A47,A56
          .= G99/.y by A40,A41,A63
          .= G99.y by A63,FUNCT_2:def 13
          .= F99.y by A57,A60,FUNCT_1:49,ZFMISC_1:56
          .= F99/.y by A57,FUNCT_2:def 13;
      end;
    end;
    hence thesis;
  end;
  let I be finite set, F be Function of I,the carrier of C;
A65: card I = card I;
A66: Q[ 0 ]
  proof
    let I be finite set, F be Function of I,the carrier of C;
    assume card I = 0;
    then
A67: I = {};
    {} is Function of {}, the carrier' of C by RELSET_1:12;
    then reconsider F9 = {} as Injections_family of a,I by A67,CAT_3:63;
    take a,F9;
    for x being set st x in I holds (doms F9)/.x = F/.x;
    hence doms F9 = F by CAT_3:1;
    thus thesis by A8,A67,CAT_3:75;
  end;
  for n being Nat holds Q[n] from NAT_1:sch 2(A66,A10);
  hence thesis by A65;
end;

definition
  struct (CatStr)CoprodCatStr (# carrier,carrier' -> set, Source,Target ->
Function of the carrier', the carrier, Comp -> PartFunc of [:the carrier', the
carrier' :],the carrier',
  Initial
-> Element of the carrier, Coproduct -> Function of [:the carrier,the carrier:]
    ,the carrier, Incl1,Incl2 -> Function of [:the carrier,the carrier:],the
    carrier' #);
end;

registration
  cluster non void non empty for CoprodCatStr;
  existence
  proof
    set o = the set;
    take CoprodCatStr(# {o},{o},o:->o,o:->o,(o,o):->o,Extract(o),(o,o)
      :->o,(o,o):->o,(o,o):->o #);
    thus thesis;
  end;
end;

definition
  let C be non void non empty CoprodCatStr;
  func EmptyMS C -> Object of C equals
  the Initial of C;
  correctness;
  let a,b be Object of C;
  func a+b -> Object of C equals
  (the Coproduct of C).(a,b);
  correctness;
  func in1(a,b) -> Morphism of C equals
  (the Incl1 of C).(a,b);
  correctness;
  func in2(a,b) -> Morphism of C equals
  (the Incl2 of C).(a,b);
  correctness;
end;

definition
  let o,m;
  func c1Cat*(o,m) -> strict CoprodCatStr equals
  CoprodCatStr(# {o},{m},m:->o,m:->o,(m,m):->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #);
  correctness;
end;

::$CT

registration
  let o,m;
  cluster c1Cat*(o,m) -> non void non empty trivial trivial';
  coherence;
end;

Lm2: c1Cat*(o,m) is Category-like
proof
  set C = c1Cat*(o,m);
  set CP = the Comp of C, CD = the Source of C, CC = the Target of C;
  thus
 for f,g being Morphism of C holds [g,f] in dom CP iff dom g=cod f
  proof
    let f,g be Morphism of C;
A1: dom CP = {[m,m]} by FUNCOP_1:13;
A2:  f = m & g = m by TARSKI:def 1;
    thus [g,f] in dom CP implies dom g=cod f
       by ZFMISC_1:def 10;
    thus thesis by A1,A2,TARSKI:def 1;
  end;
 end;

registration
  cluster strict Category-like
    reflexive transitive associative with_identities
   for  non void non empty CoprodCatStr;
  existence
  proof
    c1Cat*(0,1) is
    reflexive transitive associative with_identities
   Category-like by Lm2;
    hence thesis;
  end;
end;

registration
  let o,m be set;
  cluster c1Cat*(o,m) -> Category-like
    reflexive transitive associative with_identities
   non void non empty;
  coherence by Lm2;
end;

theorem Th45:
  for a,b being Object of c1Cat*(o,m) holds a = b
proof
  let a,b be Object of c1Cat*(o,m);
  a = o by TARSKI:def 1;
  hence thesis by TARSKI:def 1;
end;

theorem Th46:
  for f,g being Morphism of c1Cat*(o,m) holds f = g
proof
  let f,g be Morphism of c1Cat*(o,m);
  f = m by TARSKI:def 1;
  hence thesis by TARSKI:def 1;
end;

theorem Th47:
  for a,b being Object of c1Cat*(o,m), f being Morphism of c1Cat*(
  o,m) holds f in Hom(a,b)
proof
  let a,b be Object of c1Cat*(o,m), f be Morphism of c1Cat*(o,m);
  cod f = o by TARSKI:def 1;
  then
A1: cod f = b by TARSKI:def 1;
  dom f = o by TARSKI:def 1;
  then dom f = a by TARSKI:def 1;
  hence thesis by A1;
end;

theorem
  for a,b being Object of c1Cat*(o,m), f being Morphism of c1Cat*(o,m)
  holds f is Morphism of a,b
proof
  let a,b be Object of c1Cat*(o,m), f be Morphism of c1Cat*(o,m);
  f in Hom(a,b) by Th47;
  hence thesis by CAT_1:def 5;
end;

theorem
  for a,b being Object of c1Cat*(o,m) holds Hom(a,b) <> {} by Th47;

theorem Th50:
  for a being Object of c1Cat*(o,m) holds a is initial
proof
  let a be Object of c1Cat*(o,m);
  let b be Object of c1Cat*(o,m);
  set f = the Morphism of a,b;
  thus Hom(a,b)<>{} by Th47;
  take f;
  thus thesis by Th46;
end;

theorem Th51:
  for c being Object of c1Cat*(o,m), i1,i2 being Morphism of
  c1Cat*(o,m) holds c is_a_coproduct_wrt i1,i2
proof
  let c be Object of c1Cat*(o,m), i1,i2 be Morphism of c1Cat*(o,m);
  thus cod i1 = c & cod i2 = c by Th45;
  let d be Object of c1Cat*(o,m), f,g be Morphism of c1Cat*(o,m) such that
  f in Hom(dom i1,d) and
  g in Hom(dom i2,d);
  take h = i1;
  thus h in Hom(c,d) by Th47;
  thus thesis by Th46;
end;

definition
  let IT be Category-like
   reflexive transitive associative with_identities
    non void non empty CoprodCatStr;
  attr IT is Cocartesian means
  :Def26:
  the Initial of IT is initial & for a,b
  being Object of IT holds dom((the Incl1 of IT).(a,b)) = a & dom((the Incl2 of
  IT).(a,b)) = b & (the Coproduct of IT).(a,b) is_a_coproduct_wrt (the Incl1 of
  IT).(a,b),(the Incl2 of IT).(a,b);
end;

theorem Th52:
  for o,m being set holds c1Cat*(o,m) is Cocartesian
by Th50,Th45,Th51;

registration
  cluster strict Cocartesian for
    reflexive transitive associative with_identities
Category-like non void non empty CoprodCatStr;
  existence
  proof
    c1Cat*(0,1) is Cocartesian by Th52;
    hence thesis;
  end;
end;

definition
  mode Cocartesian_category is Cocartesian
    reflexive transitive associative with_identities
Category-like non void non empty
    CoprodCatStr;
end;

reserve C for Cocartesian_category;
reserve a,b,c,d,e,s for Object of C;

theorem
  EmptyMS C is initial by Def26;

theorem Th54:
  for f1,f2 being Morphism of EmptyMS C,a holds f1 = f2
proof
  let f1,f2 be Morphism of EmptyMS C,a;
  EmptyMS C is initial by Def26;
  then consider f being Morphism of EmptyMS C,a such that
A1: for g being Morphism of EmptyMS C, a holds f = g;
  thus f1 = f by A1
    .= f2 by A1;
end;

definition
  let C,a;
  func init a -> Morphism of EmptyMS C, a means
  not contradiction;
  existence;
  uniqueness by Th54;
end;

theorem Th55:
  Hom(EmptyMS C,a) <> {}
proof
  EmptyMS C is initial by Def26;
  hence thesis;
end;

theorem Th56:
  init a = init(EmptyMS C,a)
proof
  EmptyMS C is initial by Def26;
  hence thesis by CAT_3:40;
end;

theorem
  dom(init a) = EmptyMS C & cod(init a) = a
proof
  EmptyMS C is initial & init a = init(EmptyMS C,a) by Def26,Th56;
  hence thesis by CAT_3:38;
end;

theorem
  Hom(EmptyMS C,a) = {init a}
proof
  for f2 being Morphism of EmptyMS C,a holds init a = f2 by Th54;
  hence thesis by Th55,CAT_1:8;
end;

theorem Th59:
  dom in1(a,b) = a & cod in1(a,b) = a+b
proof
  set i1 = (the Incl1 of C).(a,b), i2 = (the Incl2 of C).(a,b);
  a+b is_a_coproduct_wrt i1,i2 by Def26;
  hence thesis by Def26;
end;

theorem Th60:
  dom in2(a,b) = b & cod in2(a,b) = a+b
proof
  set i1 = (the Incl1 of C).(a,b), i2 = (the Incl2 of C).(a,b);
  a+b is_a_coproduct_wrt i1,i2 by Def26;
  hence thesis by Def26;
end;

theorem Th61:
  Hom(a,a+b) <> {} & Hom(b,a+b) <> {}
proof
  set c = (the Coproduct of C).(a,b);
  set i1 = (the Incl1 of C).(a,b), i2 = (the Incl2 of C).(a,b);
  c is_a_coproduct_wrt i1,i2 by Def26;
  then
A1: cod i1 = c & cod i2 = c;
  dom(i1) = a & dom(i2) = b by Def26;
  hence thesis by A1,CAT_1:1;
end;

theorem
  a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Def26;

theorem
  C is with_finite_coproduct
proof
A1: for a,b ex c being Object of C, i1,i2 being Morphism of C st dom i1 = a
  & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2
  proof
    let a,b;
    take a+b, in1(a,b), in2(a,b);
    thus thesis by Def26,Th59,Th60;
  end;
  EmptyMS C is initial by Def26;
  hence thesis by A1,Th44;
end;

definition
  let C,a,b;
  redefine func in1(a,b) -> Morphism of a,a+b;
  coherence
  proof
    dom in1(a,b) = a & cod in1(a,b) = a+b by Th59;
    hence thesis by CAT_1:4;
  end;
  redefine func in2(a,b) -> Morphism of b,a+b;
  coherence
  proof
    dom in2(a,b) = b & cod in2(a,b) = a+b by Th60;
    hence thesis by CAT_1:4;
  end;
end;

theorem
  Hom(a,b) <> {} & Hom(b,a) <> {} implies in1(a,b) is coretraction & in2
  (a,b) is coretraction
proof
A1:  Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th61;
  a+b is_a_coproduct_wrt in1(a,b),in2(a,b) & dom in1(a,b) = a by Def26;
  hence thesis by A1,CAT_3:82;
end;

definition
  let C,a,b;
  redefine func in1(a,b) -> Morphism of a,a+b;
  coherence
  proof
    cod in1(a,b) = a+b & dom in1(a,b) = a by Th59;
    hence thesis;
  end;
  redefine func in2(a,b) -> Morphism of b,a+b;
  coherence
  proof
    cod in2(a,b) = a+b & dom in2(a,b) = b by Th60;
    hence thesis;
  end;
end;

definition
  let C,a,b,c;
  let f be Morphism of a,c, g be Morphism of b,c;
  assume
A1: Hom(a,c) <> {} & Hom(b,c) <> {};
  func [$f,g$] -> Morphism of a+b,c means
  :Def28:
  it*in1(a,b) = f & it*in2(a,b ) = g;
  existence
  proof
A2: a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Def26;
    Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th61;
    then consider h being Morphism of a+b,c such that
A3: for k being Morphism of a+b,c holds k*in1(a,b) = f & k*in2(a,b) =
    g iff h = k by A1,A2,CAT_3:81;
    take h;
    thus thesis by A3;
  end;
  uniqueness
  proof
A4: Hom(b,a+b) <> {} by Th61;
    a+b is_a_coproduct_wrt in1(a,b),in2(a,b) & Hom(a,a+b) <> {} by Def26,Th61;
    then consider h being Morphism of a+b,c such that
A5: for k being Morphism of a+b,c holds k*in1(a,b) = f & k*in2(a,b) =
    g iff h = k by A1,A4,CAT_3:81;
    let h1,h2 be Morphism of a+b,c such that
A6: h1*in1(a,b) = f & h1*in2(a,b) = g and
A7: h2*in1(a,b) = f & h2*in2(a,b) = g;
    h1 = h by A6,A5;
    hence thesis by A7,A5;
  end;
end;

theorem Th65:
  Hom(a,c) <> {} & Hom(b,c) <> {} implies Hom(a+b,c) <> {}
proof
A1: a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Def26;
  Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th61;
  hence thesis by A1,CAT_3:81;
end;

theorem Th66:
  [$in1(a,b),in2(a,b)$] = id(a+b)
proof
A1: Hom(b,a+b) <> {} by Th61;
  then
A2: (id(a+b))*in2(a,b) = in2(a,b) by CAT_1:28;
A3: Hom(a,a+b) <> {} by Th61;
  then (id(a+b))*in1(a,b) = in1(a,b) by CAT_1:28;
  hence thesis by A3,A1,A2,Def28;
end;

theorem Th67:
  for f being Morphism of a,c, g being Morphism of b,c, h being
Morphism of c,d st Hom(a,c)<>{} & Hom(b,c)<>{} & Hom(c,d)<>{} holds [$h*f,h*g$]
  = h*[$f,g$]
proof
  let f be Morphism of a,c, g be Morphism of b,c, h be Morphism of c,d;
  assume that
A1: Hom(a,c)<>{} & Hom(b,c)<>{} and
A2: Hom(c,d)<>{};
A3: Hom(a+b,c) <> {} by A1,Th65;
A4: Hom(b,a+b) <> {} by Th61;
  h*([$f,g$]*in2(a,b)) = h*g by A1,Def28;
  then
A5: h*[$f,g$]*in2(a,b) = h*g by A2,A4,A3,CAT_1:25;
A6: Hom(a,a+b) <> {} by Th61;
A7: Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,CAT_1:24;
  h*([$f,g$]*in1(a,b)) = h*f by A1,Def28;
  then h*[$f,g$]*in1(a,b) = h*f by A2,A6,A3,CAT_1:25;
  hence thesis by A5,A7,Def28;
end;

theorem Th68:
  for f,k being Morphism of a,c, g,h being Morphism of b,c st Hom(
  a,c) <> {} & Hom(b,c) <> {} & [$f,g$] = [$k,h$] holds f = k & g = h
proof
  let f,k be Morphism of a,c, g,h be Morphism of b,c;
  assume
A1: Hom(a,c) <> {} & Hom(b,c) <> {};
  then [$f,g$]*in1(a,b) = f & [$f,g$]*in2(a,b) = g by Def28;
  hence thesis by A1,Def28;
end;

theorem
  for f being Morphism of a,c, g being Morphism of b,c st Hom(a,c) <> {}
  & Hom(b,c) <> {} & (f is epi or g is epi) holds [$f,g$] is epi
proof
  let f be Morphism of a,c, g be Morphism of b,c;
  assume that
A1: Hom(a,c) <> {} and
A2: Hom(b,c) <> {} and
A3: f is epi or g is epi;
A4: now
    assume
A5: g is epi;
    let d be Object of C, f1,f2 be Morphism of c,d such that
A6: Hom(c,d)<>{} and
A7: f1*[$f,g$] = f2*[$f,g$];
A8: Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A6,CAT_1:24;
    [$f1*f,f1*g$] = f1*[$f,g$] & [$f2*f,f2*g$] = f2*[$f,g$] by A1,A2,A6,Th67;
    then f1*g = f2*g by A7,A8,Th68;
    hence f1 = f2 by A5,A6;
  end;
A9: now
    assume
A10: f is epi;
    let d;
    let f1,f2 be Morphism of c,d such that
A11: Hom(c,d)<>{} and
A12: f1*[$f,g$] = f2*[$f,g$];
A13: Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A11,CAT_1:24;
    [$f1*f,f1*g$] = f1*[$f,g$] & [$f2*f,f2*g$] = f2*[$f,g$] by A1,A2,A11,Th67;
    then f1*f = f2*f by A12,A13,Th68;
    hence f1 = f2 by A10,A11;
  end;
  Hom(a+b,c) <> {} by A1,A2,Th65;
  hence thesis by A3,A9,A4;
end;

theorem
  a, a+EmptyMS C are_isomorphic & a,EmptyMS C+a are_isomorphic
proof
A1: in2(EmptyMS C,a)*init a = in1(EmptyMS C,a) by Th54;
A2: Hom(EmptyMS C,a) <> {} & Hom(a,a) <> {} by Th55;
  thus a,a+EmptyMS C are_isomorphic
  proof
    thus
A3: Hom(a,a+EmptyMS C) <> {} by Th61;
    thus Hom(a+EmptyMS C,a) <> {} by A2,Th65;
    take g = in1(a,EmptyMS C), f = [$id a,init a$];
A4: in1(a,EmptyMS C)*init a = in2(a,EmptyMS C) by Th54;
    in1(a,EmptyMS C)*id(a) = in1(a,EmptyMS C) by A3,CAT_1:29;
    then g*f = [$in1(a,EmptyMS C),in2(a,EmptyMS C)$] by A2,A3,A4,Th67;
    hence thesis by A2,Def28,Th66;
  end;
  thus
A5: Hom(a,EmptyMS C+a) <> {} by Th61;
  thus Hom(EmptyMS C+a,a) <> {} by A2,Th65;
  take g = in2(EmptyMS C,a), f = [$init a,id a$];
  in2(EmptyMS C,a)*id(a) = in2(EmptyMS C,a) by A5,CAT_1:29;
  then g*f = [$in1(EmptyMS C,a),in2(EmptyMS C,a)$] by A2,A5,A1,Th67;
  hence thesis by A2,Def28,Th66;
end;

theorem
  a+b,b+a are_isomorphic
proof
A1: Hom(a,b+a) <> {} & Hom(b,b+a) <> {} by Th61;
  hence
A2: Hom(a+b,b+a)<>{} by Th65;
A3: Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th61;
  hence
A4: Hom(b+a,a+b)<>{} by Th65;
  take f9 = [$in2(b,a),in1(b,a)$], f = [$in2(a,b),in1(a,b)$];
  thus f9*f = [$f9*in2(a,b),f9*in1(a,b)$] by A2,A3,Th67
    .= [$in1(b,a),f9*in1(a,b)$] by A1,Def28
    .= [$in1(b,a),in2(b,a)$] by A1,Def28
    .= id(b+a) by Th66;
  thus f*f9 = [$f*in2(b,a),f*in1(b,a)$] by A1,A4,Th67
    .= [$in1(a,b),f*in1(b,a)$] by A3,Def28
    .= [$in1(a,b),in2(a,b)$] by A3,Def28
    .= id(a+b) by Th66;
end;

theorem
  (a+b)+c,a+(b+c) are_isomorphic
proof
  set k = [$in1(a+b,c)*in2(a,b),in2(a+b,c)$];
  set l = [$in1(a,b+c),in2(a,b+c)*in1(b,c)$];
A1: Hom(b+c,a+(b+c)) <> {} by Th61;
A2: Hom(b,b+c) <> {} by Th61;
  then
A3: Hom(b,a+(b+c)) <> {} by A1,CAT_1:24;
A4: Hom(a,a+(b+c)) <> {} by Th61;
  then
A5: Hom(a+b,a+(b+c)) <> {} by A3,Th65;
A6: Hom(c,b+c) <> {} by Th61;
  then
A7: Hom(c,a+(b+c)) <> {} by A1,CAT_1:24;
  hence
A8: Hom((a+b)+c,a+(b+c)) <> {} by A5,Th65;
A9: Hom(a+b,(a+b)+c) <> {} by Th61;
A10: Hom(b,a+b) <> {} by Th61;
  then
A11: Hom(b,(a+b)+c) <> {} by A9,CAT_1:24;
A12: Hom(c,(a+b)+c) <> {} by Th61;
  then
A13: Hom(b+c,(a+b)+c) <> {} by A11,Th65;
A14: Hom(a,a+b) <> {} by Th61;
  then
A15: Hom(a,(a+b)+c) <> {} by A9,CAT_1:24;
  hence
A16: Hom(a+(b+c),(a+b)+c) <> {} by A13,Th65;
  take g = [$l,in2(a,b+c)*in2(b,c)$];
  g*(in1(a+b,c)*in2(a,b)) = (g*in1(a+b,c))*in2(a,b) by A8,A9,A10,CAT_1:25
    .= l*in2(a,b) by A7,A5,Def28
    .= in2(a,b+c)*in1(b,c) by A3,A4,Def28;
  then
A17: g*k = [$in2(a,b+c)*in1(b,c),g*in2(a+b,c)$] by A8,A11,A12,Th67
    .= [$in2(a,b+c)*in1(b,c),in2(a,b+c)*in2(b,c)$] by A7,A5,Def28
    .= in2(a,b+c)*[$in1(b,c),in2(b,c)$] by A2,A1,A6,Th67
    .= in2(a,b+c)*id(b+c) by Th66
    .= in2(a,b+c) by A1,CAT_1:29;
  take f = [$in1(a+b,c)*in1(a,b),k$];
  f*(in2(a,b+c)*in1(b,c)) = (f*in2(a,b+c))*in1(b,c) by A2,A1,A16,CAT_1:25
    .= k*in1(b,c) by A15,A13,Def28
    .= in1(a+b,c)*in2(a,b) by A11,A12,Def28;
  then
A18: f*l = [$f*in1(a,b+c),in1(a+b,c)*in2(a,b)$] by A3,A4,A16,Th67
    .= [$in1(a+b,c)*in1(a,b),in1(a+b,c)*in2(a,b)$] by A15,A13,Def28
    .= in1(a+b,c)*[$in1(a,b),in2(a,b)$] by A14,A9,A10,Th67
    .= in1(a+b,c)*id(a+b) by Th66
    .= in1(a+b,c) by A9,CAT_1:29;
  g*(in1(a+b,c)*in1(a,b)) = g*in1(a+b,c)*in1(a,b) by A8,A14,A9,CAT_1:25
    .= l*in1(a,b) by A7,A5,Def28
    .= in1(a,b+c) by A3,A4,Def28;
  hence g*f = [$in1(a,b+c),in2(a,b+c)$] by A8,A15,A13,A17,Th67
    .= id(a+(b+c)) by Th66;
  f*(in2(a,b+c)*in2(b,c)) = (f*in2(a,b+c))*in2(b,c) by A1,A6,A16,CAT_1:25
    .= k*in2(b,c) by A15,A13,Def28
    .= in2(a+b,c) by A11,A12,Def28;
  hence f*g = [$in1(a+b,c),in2(a+b,c)$] by A7,A5,A16,A18,Th67
    .= id((a+b)+c) by Th66;
end;

definition
  let C,a;
  func nabla a -> Morphism of a+a,a equals
  [$id a,id a$];
  correctness;
end;

definition
  let C,a,b,c,d;
  let f be Morphism of a,c, g be Morphism of b,d;
  func f+g -> Morphism of a+b,c+d equals
  [$in1(c,d)*f,in2(c,d)*g$];
  correctness;
end;

theorem
  Hom(a,c) <> {} & Hom(b,d) <> {} implies Hom(a+b,c+d) <> {}
proof
  assume that
A1: Hom(a,c) <> {} and
A2: Hom(b,d) <> {};
  Hom(d,c+d) <> {} by Th61;
  then
A3: Hom(b,c+d) <> {} by A2,CAT_1:24;
  Hom(c,c+d) <> {} by Th61;
  then Hom(a,c+d) <> {} by A1,CAT_1:24;
  hence thesis by A3,Th65;
end;

theorem
  (id a)+(id b) = id(a+b)
proof
  Hom(b,a+b) <> {} by Th61;
  then
A1: in2(a,b)*(id b) = in2(a,b) by CAT_1:29;
  Hom(a,a+b) <> {} by Th61;
  then in1(a,b)*(id a) = in1(a,b) by CAT_1:29;
  hence thesis by A1,Th66;
end;

theorem Th75:
  for f being Morphism of a,c, h being Morphism of b,d, g being
  Morphism of c,e, k being Morphism of d,e st Hom(a,c) <> {} & Hom(b,d) <> {} &
  Hom(c,e) <> {} & Hom(d,e) <> {} holds [$g,k$]*(f+h) = [$g*f,k*h$]
proof
  let f be Morphism of a,c, h be Morphism of b,d;
  let g be Morphism of c,e, k be Morphism of d,e;
  assume that
A1: Hom(a,c) <> {} and
A2: Hom(b,d) <> {} and
A3: Hom(c,e) <> {} & Hom(d,e) <> {};
A4: Hom(c+d,e) <> {} by A3,Th65;
A5: Hom(d,c+d) <> {} by Th61;
  then
A6: Hom(b,c+d) <> {} by A2,CAT_1:24;
A7: Hom(c,c+d) <> {} by Th61;
  then
A8: Hom(a,c+d) <> {} by A1,CAT_1:24;
  [$g,k$]*in2(c,d) = k by A3,Def28;
  then
A9: k*h = [$g,k$]*(in2(c,d)*h) by A2,A4,A5,CAT_1:25;
  [$g,k$]*in1(c,d) = g by A3,Def28;
  then g*f = [$g,k$]*(in1(c,d)*f) by A1,A4,A7,CAT_1:25;
  hence thesis by A4,A8,A6,A9,Th67;
end;

theorem
  for f being Morphism of a,c, g being Morphism of b,c st Hom(a,c) <> {}
  & Hom(b,c) <> {} holds nabla(c)*(f+g) = [$f,g$]
proof
  let f be Morphism of a,c, g be Morphism of b,c such that
A1: Hom(a,c) <> {} and
A2: Hom(b,c) <> {};
  Hom(c,c) <> {};
  hence nabla(c)*(f+g) = [$(id c)*f,(id c)*g$] by A1,A2,Th75
    .= [$f,(id c)*g$] by A1,CAT_1:28
    .= [$f,g$] by A2,CAT_1:28;
end;

theorem
  for f being Morphism of a,c, h being Morphism of b,d, g being Morphism
  of c,e, k being Morphism of d,s st Hom(a,c) <> {} & Hom(b,d) <> {} & Hom(c,e)
  <> {} & Hom(d,s) <> {} holds (g+k)*(f+h) = (g*f)+(k*h)
proof
  let f be Morphism of a,c, h be Morphism of b,d;
  let g be Morphism of c,e, k be Morphism of d,s;
  assume that
A1: Hom(a,c) <> {} and
A2: Hom(b,d) <> {} and
A3: Hom(c,e) <> {} and
A4: Hom(d,s) <> {};
A5: Hom(s,e+s) <> {} by Th61;
  then
A6: Hom(d,e+s) <> {} by A4,CAT_1:24;
A7: Hom(e,e+s) <> {} by Th61;
  then in1(e,s)*g*f = in1(e,s)*(g*f) by A1,A3,CAT_1:25;
  then
A8: (g*f)+(k*h) = [$in1(e,s)*g*f,in2(e,s)*k*h$] by A2,A4,A5,CAT_1:25;
  Hom(c,e+s) <> {} by A3,A7,CAT_1:24;
  hence thesis by A1,A2,A6,A8,Th75;
end;