cat_4.miz



    begin

    reserve o,m for set;

    definition

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

      :: original: are_isomorphic

      redefine

      :: CAT_4:def1

      pred a,b are_isomorphic means ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} & ex f be Morphism of a, b, f9 be Morphism of b, a st (f * f9) = ( id b) & (f9 * f) = ( id a);

      compatibility by CAT_1: 48;

    end

    begin

    definition

      let C be Category;

      :: CAT_4:def2

      attr C is with_finite_product means for I be finite set, F be Function of I, the carrier of C holds ex a be Object of C, F9 be Projections_family of a, I st ( cods F9) = F & a is_a_product_wrt F9;

    end

    theorem :: CAT_4:1

    

     Th1: for C be Category holds C is with_finite_product iff (ex a be Object of C st a is terminal) & for a,b be Object of C holds ex c be Object of C, p1,p2 be 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 be Object of C st a is terminal) & for a,b be Object of C holds ex c be Object of C, p1,p2 be 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 be finite set, F be Function of I, the carrier of C holds ex a be Object of C, F9 be Projections_family of a, I st ( cods F9) = F & a is_a_product_wrt F9;

        then

        consider a be Object of C, F9 be Projections_family of a, {} such that ( cods F9) = F and

         A2: a is_a_product_wrt F9;

        thus ex a be 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 be Object of C, F9 be 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, FUNCT_2:def 13;

        then F9 = (( 0 ,1) --> (p1,p2)) by A6, FUNCT_4: 66;

        hence thesis by A4, CAT_3: 54;

      end;

      given a be Object of C such that

       A8: a is terminal;

      defpred Q[ Nat] means for I be finite set, F be Function of I, the carrier of C st ( card I) = $1 holds ex a be Object of C, F9 be Projections_family of a, I st ( cods F9) = F & a is_a_product_wrt F9;

      assume

       A9: for a,b be Object of C holds ex c be Object of C, p1,p2 be 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 be 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 be Object of C, G9 be Projections_family of a, (I \ {x}) such that

         A13: ( cods G9) = G and

         A14: a is_a_product_wrt G9 by A11;

        consider c be Object of C, p1,p2 be 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, CAT_3: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, CAT_3:def 2

          .= (( cods G99) /. y) by A38, CAT_3:def 2;

        end;

        then

        consider h9 be Morphism of C such that

         A40: h9 in ( Hom (d,a)) and

         A41: for k be Morphism of C st k in ( Hom (d,a)) holds (for y be 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 be Morphism of C such that

         A45: h in ( Hom (d,c)) and

         A46: for k be 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 be 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 be set st y in I holds ((F9 /. y) (*) k) = (F99 /. y);

          

           A51: for y be 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 be 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 be Nat holds Q[n] from NAT_1:sch 2( A66, A10);

      hence thesis by A65;

    end;

    definition

      struct ( CatStr) ProdCatStr (# the carrier, carrier' -> set,

the Source, Target -> Function of the carrier', the carrier,

the Comp -> PartFunc of [: the carrier', the carrier':], the carrier',

the TerminalObj -> Element of the carrier,

the CatProd -> Function of [: the carrier, the carrier:], the carrier,

the Proj1, Proj2 -> Function of [: the carrier, the carrier:], the carrier' #)

       attr strict strict;

    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;

      :: CAT_4:def3

      func [1] C -> Object of C equals the TerminalObj of C;

      correctness ;

      let a,b be Object of C;

      :: CAT_4:def4

      func a [x] b -> Object of C equals (the CatProd of C . (a,b));

      correctness ;

      :: CAT_4:def5

      func pr1 (a,b) -> Morphism of C equals (the Proj1 of C . (a,b));

      correctness ;

      :: CAT_4:def6

      func pr2 (a,b) -> Morphism of C equals (the Proj2 of C . (a,b));

      correctness ;

    end

    definition

      let o, m;

      :: CAT_4:def7

      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 :: CAT_4:2

     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 be 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 :: CAT_4:3

    

     Th3: for a,b be 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 :: CAT_4:4

    

     Th4: for f,g be 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 :: CAT_4:5

    

     Th5: for a,b be Object of ( c1Cat (o,m)), f be 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 :: CAT_4:6

    for a,b be Object of ( c1Cat (o,m)), f be 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 :: CAT_4:7

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

    theorem :: CAT_4:8

    

     Th8: for a be 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 :: CAT_4:9

    

     Th9: for c be Object of ( c1Cat (o,m)), p1,p2 be 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;

      :: CAT_4:def8

      attr IT is Cartesian means

      : Def8: the TerminalObj of IT is terminal & for a,b be 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 :: CAT_4:10

    

     Th10: for o,m be 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 :: CAT_4:11

    ( [1] C) is terminal by Def8;

    theorem :: CAT_4:12

    

     Th12: for f1,f2 be 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 be Morphism of a, ( [1] C) such that

       A1: for g be Morphism of a, ( [1] C) holds f = g;

      

      thus f1 = f by A1

      .= f2 by A1;

    end;

    theorem :: CAT_4:13

    

     Th13: ( Hom (a,( [1] C))) <> {}

    proof

      ( [1] C) is terminal by Def8;

      hence thesis;

    end;

    definition

      let C, a;

      :: CAT_4:def9

      func term (a) -> Morphism of a, ( [1] C) means not contradiction;

      existence ;

      uniqueness by Th12;

    end

    theorem :: CAT_4:14

    

     Th14: ( term a) = ( term (a,( [1] C)))

    proof

      ( [1] C) is terminal by Def8;

      hence thesis by CAT_3: 37;

    end;

    theorem :: CAT_4:15

    ( 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 :: CAT_4:16

    ( Hom (a,( [1] C))) = {( term a)}

    proof

      for f2 be Morphism of a, ( [1] C) holds ( term a) = f2 by Th12;

      hence thesis by Th13, CAT_1: 8;

    end;

    theorem :: CAT_4:17

    

     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 :: CAT_4:18

    

     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;

      :: original: pr1

      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;

      :: original: pr2

      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 :: CAT_4:19

    

     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 :: CAT_4:20

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

    theorem :: CAT_4:21

    C is with_finite_product

    proof

      

       A1: for a, b holds ex c be Object of C, p1,p2 be 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 :: CAT_4:22

    ( 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)) <> {} ;

      :: CAT_4:def10

      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 be Morphism of c, (a [x] b) such that

         A3: for h1 be 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 be Morphism of c, (a [x] b) such that

         A5: for h1 be 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 :: CAT_4:23

    

     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 :: CAT_4:24

    

     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 :: CAT_4:25

    

     Th25: for f be Morphism of c, a, g be Morphism of c, b, h be 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 :: CAT_4:26

    

     Th26: for f,k be Morphism of c, a, g,h be 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 :: CAT_4:27

    for f be Morphism of c, a, g be 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 :: CAT_4:28

    

     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;

      :: CAT_4:def11

      func lambda (a) -> Morphism of (( [1] C) [x] a), a equals ( pr2 (( [1] C),a));

      correctness ;

      :: CAT_4:def12

      func lambda' (a) -> Morphism of a, (( [1] C) [x] a) equals <:( term a), ( id a):>;

      correctness ;

      :: CAT_4:def13

      func rho (a) -> Morphism of (a [x] ( [1] C)), a equals ( pr1 (a,( [1] C)));

      correctness ;

      :: CAT_4:def14

      func rho' (a) -> Morphism of a, (a [x] ( [1] C)) equals <:( id a), ( term a):>;

      correctness ;

    end

    theorem :: CAT_4:29

    

     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 :: CAT_4:30

    (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;

      :: CAT_4:def15

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

      correctness ;

    end

    theorem :: CAT_4:31

    

     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 :: CAT_4:32

    

     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 :: CAT_4:33

    ((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;

      :: CAT_4:def16

      func Delta a -> Morphism of a, (a [x] a) equals <:( id a), ( id a):>;

      correctness ;

    end

    theorem :: CAT_4:34

    ( Hom (a,(a [x] a))) <> {}

    proof

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

      hence thesis by Th23;

    end;

    theorem :: CAT_4:35

    for f be 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;

      :: CAT_4:def17

      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 ;

      :: CAT_4:def18

      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 :: CAT_4:36

    

     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 :: CAT_4:37

    

     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 :: CAT_4:38

    (((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;

      :: CAT_4:def19

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

      correctness ;

    end

    theorem :: CAT_4:39

    ( 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 :: CAT_4:40

    (( 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 :: CAT_4:41

    

     Th41: for f be Morphism of a, b, h be Morphism of c, d, g be Morphism of e, a, k be 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 :: CAT_4:42

    for f be Morphism of c, a, g be 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 :: CAT_4:43

    for f be Morphism of a, b, h be Morphism of c, d, g be Morphism of e, a, k be 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

    definition

      let C be Category;

      :: CAT_4:def20

      attr C is with_finite_coproduct means for I be finite set, F be Function of I, the carrier of C holds ex a be Object of C, F9 be Injections_family of a, I st ( doms F9) = F & a is_a_coproduct_wrt F9;

    end

    theorem :: CAT_4:44

    

     Th44: for C be Category holds C is with_finite_coproduct iff (ex a be Object of C st a is initial) & for a,b be Object of C holds ex c be Object of C, i1,i2 be 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 be Object of C st a is initial) & for a,b be Object of C holds ex c be Object of C, i1,i2 be 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 be finite set, F be Function of I, the carrier of C holds ex a be Object of C, F9 be Injections_family of a, I st ( doms F9) = F & a is_a_coproduct_wrt F9;

        then

        consider a be Object of C, F9 be Injections_family of a, {} such that ( doms F9) = F and

         A3: a is_a_coproduct_wrt F9;

        thus ex a be 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 be Object of C, F9 be 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, FUNCT_2:def 13;

        then F9 = (( 0 ,1) --> (i1,i2)) by A7, FUNCT_4: 66;

        hence thesis by A5, CAT_3: 79;

      end;

      given a be Object of C such that

       A8: a is initial;

      defpred Q[ Nat] means for I be finite set, F be Function of I, the carrier of C st ( card I) = $1 holds ex a be Object of C, F9 be Injections_family of a, I st ( doms F9) = F & a is_a_coproduct_wrt F9;

      assume

       A9: for a,b be Object of C holds ex c be Object of C, i1,i2 be 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 be 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 be Object of C, G9 be 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 be Object of C, i1,i2 be 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, CAT_3: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, CAT_3:def 1

          .= (( doms G99) /. y) by A38, CAT_3:def 1;

        end;

        then

        consider h9 be Morphism of C such that

         A40: h9 in ( Hom (a,d)) and

         A41: for k be Morphism of C st k in ( Hom (a,d)) holds (for y be 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 be Morphism of C such that

         A45: h in ( Hom (c,d)) and

         A46: for k be 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 be 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 be set st y in I holds (k (*) (F9 /. y)) = (F99 /. y);

          

           A51: for y be 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 be 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 be Nat holds Q[n] from NAT_1:sch 2( A66, A10);

      hence thesis by A65;

    end;

    definition

      struct ( CatStr) CoprodCatStr (# the carrier, carrier' -> set,

the Source, Target -> Function of the carrier', the carrier,

the Comp -> PartFunc of [: the carrier', the carrier':], the carrier',

the Initial -> Element of the carrier,

the Coproduct -> Function of [: the carrier, the carrier:], the carrier,

the Incl1, Incl2 -> Function of [: the carrier, the carrier:], the carrier' #)

       attr strict strict;

    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;

      :: CAT_4:def21

      func EmptyMS C -> Object of C equals the Initial of C;

      correctness ;

      let a,b be Object of C;

      :: CAT_4:def22

      func a + b -> Object of C equals (the Coproduct of C . (a,b));

      correctness ;

      :: CAT_4:def23

      func in1 (a,b) -> Morphism of C equals (the Incl1 of C . (a,b));

      correctness ;

      :: CAT_4:def24

      func in2 (a,b) -> Morphism of C equals (the Incl2 of C . (a,b));

      correctness ;

    end

    definition

      let o, m;

      :: CAT_4:def25

      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

    ::$Canceled

    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 be 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 :: CAT_4:46

    

     Th45: for a,b be 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 :: CAT_4:47

    

     Th46: for f,g be 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 :: CAT_4:48

    

     Th47: for a,b be Object of ( c1Cat* (o,m)), f be 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 :: CAT_4:49

    for a,b be Object of ( c1Cat* (o,m)), f be 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 :: CAT_4:50

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

    theorem :: CAT_4:51

    

     Th50: for a be 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 :: CAT_4:52

    

     Th51: for c be Object of ( c1Cat* (o,m)), i1,i2 be 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;

      :: CAT_4:def26

      attr IT is Cocartesian means

      : Def26: the Initial of IT is initial & for a,b be 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 :: CAT_4:53

    

     Th52: for o,m be 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 :: CAT_4:54

    ( EmptyMS C) is initial by Def26;

    theorem :: CAT_4:55

    

     Th54: for f1,f2 be 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 be Morphism of ( EmptyMS C), a such that

       A1: for g be Morphism of ( EmptyMS C), a holds f = g;

      

      thus f1 = f by A1

      .= f2 by A1;

    end;

    definition

      let C, a;

      :: CAT_4:def27

      func init a -> Morphism of ( EmptyMS C), a means not contradiction;

      existence ;

      uniqueness by Th54;

    end

    theorem :: CAT_4:56

    

     Th55: ( Hom (( EmptyMS C),a)) <> {}

    proof

      ( EmptyMS C) is initial by Def26;

      hence thesis;

    end;

    theorem :: CAT_4:57

    

     Th56: ( init a) = ( init (( EmptyMS C),a))

    proof

      ( EmptyMS C) is initial by Def26;

      hence thesis by CAT_3: 40;

    end;

    theorem :: CAT_4:58

    ( 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 :: CAT_4:59

    ( Hom (( EmptyMS C),a)) = {( init a)}

    proof

      for f2 be Morphism of ( EmptyMS C), a holds ( init a) = f2 by Th54;

      hence thesis by Th55, CAT_1: 8;

    end;

    theorem :: CAT_4:60

    

     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 :: CAT_4:61

    

     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 :: CAT_4:62

    

     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 :: CAT_4:63

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

    theorem :: CAT_4:64

    C is with_finite_coproduct

    proof

      

       A1: for a, b holds ex c be Object of C, i1,i2 be 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;

      :: original: in1

      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;

      :: original: in2

      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 :: CAT_4:65

    ( 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;

      :: original: in1

      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;

      :: original: in2

      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)) <> {} ;

      :: CAT_4:def28

      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 be Morphism of (a + b), c such that

         A3: for k be 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 be Morphism of (a + b), c such that

         A5: for k be 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 :: CAT_4:66

    

     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 :: CAT_4:67

    

     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 :: CAT_4:68

    

     Th67: for f be Morphism of a, c, g be Morphism of b, c, h be 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 :: CAT_4:69

    

     Th68: for f,k be Morphism of a, c, g,h be 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 :: CAT_4:70

    for f be Morphism of a, c, g be 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 :: CAT_4:71

    (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 :: CAT_4:72

    ((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 :: CAT_4:73

    (((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;

      :: CAT_4:def29

      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;

      :: CAT_4:def30

      func f + g -> Morphism of (a + b), (c + d) equals [$(( in1 (c,d)) * f), (( in2 (c,d)) * g)$];

      correctness ;

    end

    theorem :: CAT_4:74

    ( 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 :: CAT_4:75

    (( 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 :: CAT_4:76

    

     Th75: for f be Morphism of a, c, h be Morphism of b, d, g be Morphism of c, e, k be 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 :: CAT_4:77

    for f be Morphism of a, c, g be 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 :: CAT_4:78

    for f be Morphism of a, c, h be Morphism of b, d, g be Morphism of c, e, k be 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;