cat_3.miz



    begin

    reserve I for set,

x,x1,x2,y,z for set,

A for non empty set;

    reserve C,D for Category;

    reserve a,b,c,d for Object of C;

    reserve f,g,h,i,j,k,p1,p2,q1,q2,i1,i2,j1,j2 for Morphism of C;

    scheme :: CAT_3:sch1

    LambdaIdx { I() -> set , A() -> non empty set , F( object) -> Element of A() } :

ex F be Function of I(), A() st for x st x in I() holds (F /. x) = F(x);

      

       A1: for x be object st x in I() holds F(x) in A();

      consider IT be Function of I(), A() such that

       A2: for x be object st x in I() holds (IT . x) = F(x) from FUNCT_2:sch 2( A1);

      take IT;

      let x;

      assume

       A3: x in I();

      

      hence F(x) = (IT . x) by A2

      .= (IT /. x) by A3, FUNCT_2:def 13;

    end;

    theorem :: CAT_3:1

    

     Th1: for F1,F2 be Function of I, A st for x st x in I holds (F1 /. x) = (F2 /. x) holds F1 = F2

    proof

      let F1,F2 be Function of I, A such that

       A1: for x st x in I holds (F1 /. x) = (F2 /. x);

      now

        let x be object;

        assume

         A2: x in I;

        

        hence (F1 . x) = (F1 /. x) by FUNCT_2:def 13

        .= (F2 /. x) by A1, A2

        .= (F2 . x) by A2, FUNCT_2:def 13;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    scheme :: CAT_3:sch2

    FuncIdxcorrectness { I() -> set , A() -> non empty set , F( set) -> Element of A() } :

(ex F be Function of I(), A() st for x st x in I() holds (F /. x) = F(x)) & for F1,F2 be Function of I(), A() st (for x st x in I() holds (F1 /. x) = F(x)) & (for x st x in I() holds (F2 /. x) = F(x)) holds F1 = F2;

      thus ex F be Function of I(), A() st for x st x in I() holds (F /. x) = F(x) from LambdaIdx;

      let F1,F2 be Function of I(), A() such that

       A1: for x st x in I() holds (F1 /. x) = F(x) and

       A2: for x st x in I() holds (F2 /. x) = F(x);

      now

        let x;

        assume

         A3: x in I();

        

        hence (F1 /. x) = F(x) by A1

        .= (F2 /. x) by A2, A3;

      end;

      hence thesis by Th1;

    end;

    definition

      let A, x;

      let a be Element of A;

      :: original: .-->

      redefine

      func x .--> a -> Function of {x}, A ;

      coherence by FUNCOP_1: 46;

    end

    theorem :: CAT_3:2

    

     Th2: for a be Element of A st x in I holds ((I --> a) /. x) = a

    proof

      let a be Element of A;

      assume

       A1: x in I;

      

      hence a = ((I --> a) . x) by FUNCOP_1: 7

      .= ((I --> a) /. x) by A1, FUNCT_2:def 13;

    end;

    theorem :: CAT_3:3

    

     Th3: x1 <> x2 implies for y1,y2 be Element of A holds (((x1,x2) --> (y1,y2)) /. x1) = y1 & (((x1,x2) --> (y1,y2)) /. x2) = y2

    proof

      assume

       A1: x1 <> x2;

      let y1,y2 be Element of A;

      set h = ((x1,x2) --> (y1,y2));

      

       A2: (h . x2) = y2 & x1 in {x1, x2} by FUNCT_4: 63, TARSKI:def 2;

      

       A3: x2 in {x1, x2} by TARSKI:def 2;

      (h . x1) = y1 by A1, FUNCT_4: 63;

      hence thesis by A2, A3, FUNCT_2:def 13;

    end;

    begin

    definition

      let C, I;

      let F be Function of I, the carrier' of C;

      :: CAT_3:def1

      func doms F -> Function of I, the carrier of C means

      : Def1: for x st x in I holds (it /. x) = ( dom (F /. x));

      correctness

      proof

        deffunc F( set) = ( dom (F /. $1));

        set A = the carrier of C;

        thus (ex F be Function of I, A st for x st x in I holds (F /. x) = F(x)) & for F1,F2 be Function of I, A st (for x st x in I holds (F1 /. x) = F(x)) & (for x st x in I holds (F2 /. x) = F(x)) holds F1 = F2 from FuncIdxcorrectness;

      end;

      :: CAT_3:def2

      func cods F -> Function of I, the carrier of C means

      : Def2: for x st x in I holds (it /. x) = ( cod (F /. x));

      correctness

      proof

        deffunc F( set) = ( cod (F /. $1));

        set A = the carrier of C;

        thus (ex F be Function of I, A st for x st x in I holds (F /. x) = F(x)) & for F1,F2 be Function of I, A st (for x st x in I holds (F1 /. x) = F(x)) & (for x st x in I holds (F2 /. x) = F(x)) holds F1 = F2 from FuncIdxcorrectness;

      end;

    end

    theorem :: CAT_3:4

    

     Th4: ( doms (I --> f)) = (I --> ( dom f))

    proof

      set F = (I --> f), F9 = (I --> ( dom f));

      now

        let x;

        assume

         A1: x in I;

        then (F /. x) = f & (F9 /. x) = ( dom f) by Th2;

        hence (( doms F) /. x) = (F9 /. x) by A1, Def1;

      end;

      hence thesis by Th1;

    end;

    theorem :: CAT_3:5

    

     Th5: ( cods (I --> f)) = (I --> ( cod f))

    proof

      set F = (I --> f), F9 = (I --> ( cod f));

      now

        let x;

        assume

         A1: x in I;

        then (F /. x) = f & (F9 /. x) = ( cod f) by Th2;

        hence (( cods F) /. x) = (F9 /. x) by A1, Def2;

      end;

      hence thesis by Th1;

    end;

    theorem :: CAT_3:6

    

     Th6: ( doms ((x1,x2) --> (p1,p2))) = ((x1,x2) --> (( dom p1),( dom p2)))

    proof

      set F = ((x1,x2) --> (p1,p2)), f = (x1 .--> p1), g = (x2 .--> p2), F9 = ((x1,x2) --> (( dom p1),( dom p2))), f9 = (x1 .--> ( dom p1)), g9 = (x2 .--> ( dom p2));

      

       A1: ( dom g) = {x2} by FUNCOP_1: 13;

      

       A2: ( dom g9) = {x2} & F9 = (f9 +* g9) by FUNCOP_1: 13, FUNCT_4:def 4;

      

       A3: F = (f +* g) by FUNCT_4:def 4;

      

       A4: ( dom f) = {x1} by FUNCOP_1: 13;

      now

        let x;

        assume

         A5: x in {x1, x2};

        then

         A6: x in ( dom F) by FUNCT_4: 62;

        now

          per cases by A3, A6, FUNCT_4: 12;

            case

             A7: x in ( dom f) & not x in ( dom g);

            then (F . x) = (f . x) by A3, FUNCT_4: 11;

            then

             A8: (F . x) = p1 by A4, A7, FUNCOP_1: 7;

            (F9 . x) = (f9 . x) by A1, A2, A7, FUNCT_4: 11;

            then (F9 . x) = ( dom p1) by A4, A7, FUNCOP_1: 7;

            hence (F /. x) = p1 & (F9 /. x) = ( dom p1) by A5, A8, FUNCT_2:def 13;

          end;

            case

             A9: x in ( dom g);

            then (F . x) = (g . x) by A3, FUNCT_4: 13;

            then

             A10: (F . x) = p2 by A1, A9, FUNCOP_1: 7;

            (F9 . x) = (g9 . x) by A1, A2, A9, FUNCT_4: 13;

            then (F9 . x) = ( dom p2) by A1, A9, FUNCOP_1: 7;

            hence (F /. x) = p2 & (F9 /. x) = ( dom p2) by A5, A10, FUNCT_2:def 13;

          end;

        end;

        hence (( doms F) /. x) = (F9 /. x) by A5, Def1;

      end;

      hence thesis by Th1;

    end;

    theorem :: CAT_3:7

    

     Th7: ( cods ((x1,x2) --> (p1,p2))) = ((x1,x2) --> (( cod p1),( cod p2)))

    proof

      set F = ((x1,x2) --> (p1,p2)), f = (x1 .--> p1), g = (x2 .--> p2), F9 = ((x1,x2) --> (( cod p1),( cod p2))), f9 = (x1 .--> ( cod p1)), g9 = (x2 .--> ( cod p2));

      

       A1: ( dom g) = {x2} by FUNCOP_1: 13;

      

       A2: ( dom g9) = {x2} & F9 = (f9 +* g9) by FUNCOP_1: 13, FUNCT_4:def 4;

      

       A3: F = (f +* g) by FUNCT_4:def 4;

      

       A4: ( dom f) = {x1} by FUNCOP_1: 13;

      now

        let x;

        assume

         A5: x in {x1, x2};

        then

         A6: x in ( dom F) by FUNCT_4: 62;

        now

          per cases by A3, A6, FUNCT_4: 12;

            case

             A7: x in ( dom f) & not x in ( dom g);

            then (F . x) = (f . x) by A3, FUNCT_4: 11;

            then

             A8: (F . x) = p1 by A4, A7, FUNCOP_1: 7;

            (F9 . x) = (f9 . x) by A1, A2, A7, FUNCT_4: 11;

            then (F9 . x) = ( cod p1) by A4, A7, FUNCOP_1: 7;

            hence (F /. x) = p1 & (F9 /. x) = ( cod p1) by A5, A8, FUNCT_2:def 13;

          end;

            case

             A9: x in ( dom g);

            then (F . x) = (g . x) by A3, FUNCT_4: 13;

            then

             A10: (F . x) = p2 by A1, A9, FUNCOP_1: 7;

            (F9 . x) = (g9 . x) by A1, A2, A9, FUNCT_4: 13;

            then (F9 . x) = ( cod p2) by A1, A9, FUNCOP_1: 7;

            hence (F /. x) = p2 & (F9 /. x) = ( cod p2) by A5, A10, FUNCT_2:def 13;

          end;

        end;

        hence (( cods F) /. x) = (F9 /. x) by A5, Def2;

      end;

      hence thesis by Th1;

    end;

    definition

      let C, I;

      let F be Function of I, the carrier' of C;

      :: CAT_3:def3

      func F opp -> Function of I, the carrier' of (C opp ) means

      : Def3: for x st x in I holds (it /. x) = ((F /. x) opp );

      correctness

      proof

        deffunc F( set) = ((F /. $1) opp );

        set A = the carrier' of (C opp );

        thus (ex F be Function of I, A st for x st x in I holds (F /. x) = F(x)) & for F1,F2 be Function of I, A st (for x st x in I holds (F1 /. x) = F(x)) & (for x st x in I holds (F2 /. x) = F(x)) holds F1 = F2 from FuncIdxcorrectness;

      end;

    end

    theorem :: CAT_3:8

    ((I --> f) opp ) = (I --> (f opp ))

    proof

      set F = (I --> f), F9 = (I --> (f opp ));

      now

        let x;

        assume

         A1: x in I;

        then (F /. x) = f & (F9 /. x) = (f opp ) by Th2;

        hence ((F opp ) /. x) = (F9 /. x) by A1, Def3;

      end;

      hence thesis by Th1;

    end;

    theorem :: CAT_3:9

    x1 <> x2 implies (((x1,x2) --> (p1,p2)) opp ) = ((x1,x2) --> ((p1 opp ),(p2 opp )))

    proof

      set F = ((x1,x2) --> (p1,p2)), F9 = ((x1,x2) --> ((p1 opp ),(p2 opp )));

      assume

       A1: x1 <> x2;

      now

        let x;

        assume

         A2: x in {x1, x2};

        then x = x1 or x = x2 by TARSKI:def 2;

        then (F /. x) = p1 & (F9 /. x) = (p1 opp ) or (F /. x) = p2 & (F9 /. x) = (p2 opp ) by A1, Th3;

        hence ((F opp ) /. x) = (F9 /. x) by A2, Def3;

      end;

      hence thesis by Th1;

    end;

    theorem :: CAT_3:10

    for F be Function of I, the carrier' of C holds ((F opp ) opp ) = F

    proof

      let F be Function of I, the carrier' of C;

      now

        thus the carrier' of C = the carrier' of ((C opp ) opp );

        let x;

        assume

         A1: x in I;

        

        hence (((F opp ) opp ) /. x) = (((F opp ) /. x) opp ) by Def3

        .= (((F /. x) opp ) opp ) by A1, Def3

        .= (F /. x);

      end;

      hence thesis by Th1;

    end;

    definition

      let C, I;

      let F be Function of I, the carrier' of (C opp );

      :: CAT_3:def4

      func opp F -> Function of I, the carrier' of C means

      : Def4: for x st x in I holds (it /. x) = ( opp (F /. x));

      correctness

      proof

        deffunc F( set) = ( opp (F /. $1));

        set A = the carrier' of C;

        thus (ex F be Function of I, A st for x st x in I holds (F /. x) = F(x)) & for F1,F2 be Function of I, A st (for x st x in I holds (F1 /. x) = F(x)) & (for x st x in I holds (F2 /. x) = F(x)) holds F1 = F2 from FuncIdxcorrectness;

      end;

    end

    theorem :: CAT_3:11

    for f be Morphism of (C opp ) holds ( opp (I --> f)) = (I --> ( opp f))

    proof

      let f be Morphism of (C opp );

      set F = (I --> f), F9 = (I --> ( opp f));

      now

        let x;

        assume

         A1: x in I;

        then (F /. x) = f & (F9 /. x) = ( opp f) by Th2;

        hence (( opp F) /. x) = (F9 /. x) by A1, Def4;

      end;

      hence thesis by Th1;

    end;

    theorem :: CAT_3:12

    x1 <> x2 implies for p1,p2 be Morphism of (C opp ) holds ( opp ((x1,x2) --> (p1,p2))) = ((x1,x2) --> (( opp p1),( opp p2)))

    proof

      assume

       A1: x1 <> x2;

      let p1,p2 be Morphism of (C opp );

      set F = ((x1,x2) --> (p1,p2)), F9 = ((x1,x2) --> (( opp p1),( opp p2)));

      now

        let x;

        assume

         A2: x in {x1, x2};

        then x = x1 or x = x2 by TARSKI:def 2;

        then (F /. x) = p1 & (F9 /. x) = ( opp p1) or (F /. x) = p2 & (F9 /. x) = ( opp p2) by A1, Th3;

        hence (( opp F) /. x) = (F9 /. x) by A2, Def4;

      end;

      hence thesis by Th1;

    end;

    theorem :: CAT_3:13

    for F be Function of I, the carrier' of C holds ( opp (F opp )) = F

    proof

      let F be Function of I, the carrier' of C;

      now

        let x;

        assume

         A1: x in I;

        

        hence (( opp (F opp )) /. x) = ( opp ((F opp ) /. x)) by Def4

        .= ( opp ((F /. x) opp )) by A1, Def3

        .= (F /. x);

      end;

      hence thesis by Th1;

    end;

    definition

      let C, I;

      let F be Function of I, the carrier' of C, f;

      :: CAT_3:def5

      func F * f -> Function of I, the carrier' of C means

      : Def5: for x st x in I holds (it /. x) = ((F /. x) (*) f);

      correctness

      proof

        deffunc F( set) = ((F /. $1) (*) f);

        set A = the carrier' of C;

        thus (ex F be Function of I, A st for x st x in I holds (F /. x) = F(x)) & for F1,F2 be Function of I, A st (for x st x in I holds (F1 /. x) = F(x)) & (for x st x in I holds (F2 /. x) = F(x)) holds F1 = F2 from FuncIdxcorrectness;

      end;

      :: CAT_3:def6

      func f * F -> Function of I, the carrier' of C means

      : Def6: for x st x in I holds (it /. x) = (f (*) (F /. x));

      correctness

      proof

        deffunc F( set) = (f (*) (F /. $1));

        set A = the carrier' of C;

        thus (ex F be Function of I, A st for x st x in I holds (F /. x) = F(x)) & for F1,F2 be Function of I, A st (for x st x in I holds (F1 /. x) = F(x)) & (for x st x in I holds (F2 /. x) = F(x)) holds F1 = F2 from FuncIdxcorrectness;

      end;

    end

    theorem :: CAT_3:14

    

     Th14: x1 <> x2 implies (((x1,x2) --> (p1,p2)) * f) = ((x1,x2) --> ((p1 (*) f),(p2 (*) f)))

    proof

      set F = ((x1,x2) --> (p1,p2)), F9 = ((x1,x2) --> ((p1 (*) f),(p2 (*) f)));

      assume

       A1: x1 <> x2;

      now

        let x;

        assume

         A2: x in {x1, x2};

        then x = x1 or x = x2 by TARSKI:def 2;

        then (F /. x) = p1 & (F9 /. x) = (p1 (*) f) or (F /. x) = p2 & (F9 /. x) = (p2 (*) f) by A1, Th3;

        hence ((F * f) /. x) = (F9 /. x) by A2, Def5;

      end;

      hence thesis by Th1;

    end;

    theorem :: CAT_3:15

    

     Th15: x1 <> x2 implies (f * ((x1,x2) --> (p1,p2))) = ((x1,x2) --> ((f (*) p1),(f (*) p2)))

    proof

      set F = ((x1,x2) --> (p1,p2)), F9 = ((x1,x2) --> ((f (*) p1),(f (*) p2)));

      assume

       A1: x1 <> x2;

      now

        let x;

        assume

         A2: x in {x1, x2};

        then x = x1 or x = x2 by TARSKI:def 2;

        then (F /. x) = p1 & (F9 /. x) = (f (*) p1) or (F /. x) = p2 & (F9 /. x) = (f (*) p2) by A1, Th3;

        hence ((f * F) /. x) = (F9 /. x) by A2, Def6;

      end;

      hence thesis by Th1;

    end;

    theorem :: CAT_3:16

    

     Th16: for F be Function of I, the carrier' of C st ( doms F) = (I --> ( cod f)) holds ( doms (F * f)) = (I --> ( dom f)) & ( cods (F * f)) = ( cods F)

    proof

      let F be Function of I, the carrier' of C such that

       A1: ( doms F) = (I --> ( cod f));

      now

        let x;

        assume

         A2: x in I;

        

        then

         A3: ( dom (F /. x)) = ((I --> ( cod f)) /. x) by A1, Def1

        .= ( cod f) by A2, Th2;

        

        thus (( doms (F * f)) /. x) = ( dom ((F * f) /. x)) by A2, Def1

        .= ( dom ((F /. x) (*) f)) by A2, Def5

        .= ( dom f) by A3, CAT_1: 17

        .= ((I --> ( dom f)) /. x) by A2, Th2;

      end;

      hence ( doms (F * f)) = (I --> ( dom f)) by Th1;

      now

        let x;

        assume

         A4: x in I;

        

        then

         A5: ( dom (F /. x)) = ((I --> ( cod f)) /. x) by A1, Def1

        .= ( cod f) by A4, Th2;

        

        thus (( cods F) /. x) = ( cod (F /. x)) by A4, Def2

        .= ( cod ((F /. x) (*) f)) by A5, CAT_1: 17

        .= ( cod ((F * f) /. x)) by A4, Def5

        .= (( cods (F * f)) /. x) by A4, Def2;

      end;

      hence thesis by Th1;

    end;

    theorem :: CAT_3:17

    

     Th17: for F be Function of I, the carrier' of C st ( cods F) = (I --> ( dom f)) holds ( doms (f * F)) = ( doms F) & ( cods (f * F)) = (I --> ( cod f))

    proof

      let F be Function of I, the carrier' of C such that

       A1: ( cods F) = (I --> ( dom f));

      now

        let x;

        assume

         A2: x in I;

        

        then

         A3: ( cod (F /. x)) = ((I --> ( dom f)) /. x) by A1, Def2

        .= ( dom f) by A2, Th2;

        

        thus (( doms F) /. x) = ( dom (F /. x)) by A2, Def1

        .= ( dom (f (*) (F /. x))) by A3, CAT_1: 17

        .= ( dom ((f * F) /. x)) by A2, Def6

        .= (( doms (f * F)) /. x) by A2, Def1;

      end;

      hence ( doms (f * F)) = ( doms F) by Th1;

      now

        let x;

        assume

         A4: x in I;

        

        then

         A5: ( cod (F /. x)) = ((I --> ( dom f)) /. x) by A1, Def2

        .= ( dom f) by A4, Th2;

        

        thus (( cods (f * F)) /. x) = ( cod ((f * F) /. x)) by A4, Def2

        .= ( cod (f (*) (F /. x))) by A4, Def6

        .= ( cod f) by A5, CAT_1: 17

        .= ((I --> ( cod f)) /. x) by A4, Th2;

      end;

      hence thesis by Th1;

    end;

    definition

      let C, I;

      let F,G be Function of I, the carrier' of C;

      :: CAT_3:def7

      func F "*" G -> Function of I, the carrier' of C means

      : Def7: for x st x in I holds (it /. x) = ((F /. x) (*) (G /. x));

      correctness

      proof

        deffunc F( set) = ((F /. $1) (*) (G /. $1));

        set A = the carrier' of C;

        thus (ex F be Function of I, A st for x st x in I holds (F /. x) = F(x)) & for F1,F2 be Function of I, A st (for x st x in I holds (F1 /. x) = F(x)) & (for x st x in I holds (F2 /. x) = F(x)) holds F1 = F2 from FuncIdxcorrectness;

      end;

    end

    theorem :: CAT_3:18

    

     Th18: for F,G be Function of I, the carrier' of C st ( doms F) = ( cods G) holds ( doms (F "*" G)) = ( doms G) & ( cods (F "*" G)) = ( cods F)

    proof

      let F,G be Function of I, the carrier' of C such that

       A1: ( doms F) = ( cods G);

      now

        let x;

        assume

         A2: x in I;

        

        then

         A3: ( cod (G /. x)) = (( doms F) /. x) by A1, Def2

        .= ( dom (F /. x)) by A2, Def1;

        

        thus (( doms (F "*" G)) /. x) = ( dom ((F "*" G) /. x)) by A2, Def1

        .= ( dom ((F /. x) (*) (G /. x))) by A2, Def7

        .= ( dom (G /. x)) by A3, CAT_1: 17

        .= (( doms G) /. x) by A2, Def1;

      end;

      hence ( doms (F "*" G)) = ( doms G) by Th1;

      now

        let x;

        assume

         A4: x in I;

        

        then

         A5: ( cod (G /. x)) = (( doms F) /. x) by A1, Def2

        .= ( dom (F /. x)) by A4, Def1;

        

        thus (( cods (F "*" G)) /. x) = ( cod ((F "*" G) /. x)) by A4, Def2

        .= ( cod ((F /. x) (*) (G /. x))) by A4, Def7

        .= ( cod (F /. x)) by A5, CAT_1: 17

        .= (( cods F) /. x) by A4, Def2;

      end;

      hence thesis by Th1;

    end;

    theorem :: CAT_3:19

    x1 <> x2 implies (((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2))) = ((x1,x2) --> ((p1 (*) q1),(p2 (*) q2)))

    proof

      set F1 = ((x1,x2) --> (p1,p2)), F2 = ((x1,x2) --> (q1,q2)), G = ((x1,x2) --> ((p1 (*) q1),(p2 (*) q2)));

      assume

       A1: x1 <> x2;

      now

        let x;

        assume

         A2: x in {x1, x2};

        then x = x1 or x = x2 by TARSKI:def 2;

        then (F1 /. x) = p1 & (F2 /. x) = q1 & (G /. x) = (p1 (*) q1) or (F1 /. x) = p2 & (F2 /. x) = q2 & (G /. x) = (p2 (*) q2) by A1, Th3;

        hence ((F1 "*" F2) /. x) = (G /. x) by A2, Def7;

      end;

      hence thesis by Th1;

    end;

    theorem :: CAT_3:20

    for F be Function of I, the carrier' of C holds (F * f) = (F "*" (I --> f))

    proof

      let F be Function of I, the carrier' of C;

      now

        let x;

        assume

         A1: x in I;

        

        hence ((F * f) /. x) = ((F /. x) (*) f) by Def5

        .= ((F /. x) (*) ((I --> f) /. x)) by A1, Th2

        .= ((F "*" (I --> f)) /. x) by A1, Def7;

      end;

      hence thesis by Th1;

    end;

    theorem :: CAT_3:21

    for F be Function of I, the carrier' of C holds (f * F) = ((I --> f) "*" F)

    proof

      let F be Function of I, the carrier' of C;

      now

        let x;

        assume

         A1: x in I;

        

        hence ((f * F) /. x) = (f (*) (F /. x)) by Def6

        .= (((I --> f) /. x) (*) (F /. x)) by A1, Th2

        .= (((I --> f) "*" F) /. x) by A1, Def7;

      end;

      hence thesis by Th1;

    end;

    begin

    reserve f for Morphism of a, b,

g for Morphism of b, a;

    definition

      let C, a, b;

      let IT be Morphism of a, b;

      :: CAT_3:def8

      attr IT is retraction means ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} & ex g st (IT * g) = ( id b);

      :: CAT_3:def9

      attr IT is coretraction means ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} & ex g st (g * IT) = ( id a);

    end

    theorem :: CAT_3:22

    

     Th22: f is retraction implies f is epi

    proof

      assume

       A1: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} ;

      given g such that

       A2: (f * g) = ( id b);

      thus ( Hom (a,b)) <> {} by A1;

      let c be Object of C such that

       A3: ( Hom (b,c)) <> {} ;

      let p1,p2 be Morphism of b, c;

      assume

       A4: (p1 * f) = (p2 * f);

      

      thus p1 = (p1 * (f * g)) by A3, A2, CAT_1: 29

      .= ((p2 * f) * g) by A3, A1, A4, CAT_1: 25

      .= (p2 * (f * g)) by A3, A1, CAT_1: 25

      .= p2 by A3, A2, CAT_1: 29;

    end;

    theorem :: CAT_3:23

    f is coretraction implies f is monic

    proof

      assume

       A1: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} ;

      given g such that

       A2: (g * f) = ( id a);

      thus ( Hom (a,b)) <> {} by A1;

      let c be Object of C such that

       A3: ( Hom (c,a)) <> {} ;

      let p1,p2 be Morphism of c, a;

      assume

       A4: (f * p1) = (f * p2);

      

      thus p1 = ((g * f) * p1) by A3, A2, CAT_1: 28

      .= (g * (f * p2)) by A3, A1, A4, CAT_1: 25

      .= ((g * f) * p2) by A3, A1, CAT_1: 25

      .= p2 by A3, A2, CAT_1: 28;

    end;

    reserve g for Morphism of b, c;

    theorem :: CAT_3:24

    f is retraction & g is retraction implies (g * f) is retraction

    proof

      assume

       A1: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} ;

      given i be Morphism of b, a such that

       A2: (f * i) = ( id b);

      assume

       A3: ( Hom (b,c)) <> {} & ( Hom (c,b)) <> {} ;

      given j be Morphism of c, b such that

       A4: (g * j) = ( id c);

      thus

       A5: ( Hom (a,c)) <> {} & ( Hom (c,a)) <> {} by A1, A3, CAT_1: 24;

      take (i * j);

      

      thus ((g * f) * (i * j)) = (g * (f * (i * j))) by A1, A3, A5, CAT_1: 25

      .= (g * ((f * i) * j)) by A1, A3, CAT_1: 25

      .= ( id c) by A2, A3, A4, CAT_1: 28;

    end;

    theorem :: CAT_3:25

    f is coretraction & g is coretraction implies (g * f) is coretraction

    proof

      assume

       A1: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} ;

      given i be Morphism of b, a such that

       A2: (i * f) = ( id a);

      assume

       A3: ( Hom (b,c)) <> {} & ( Hom (c,b)) <> {} ;

      given j be Morphism of c, b such that

       A4: (j * g) = ( id b);

      thus

       A5: ( Hom (a,c)) <> {} & ( Hom (c,a)) <> {} by A1, A3, CAT_1: 24;

      take (i * j);

      

      thus ((i * j) * (g * f)) = (i * (j * (g * f))) by A1, A3, A5, CAT_1: 25

      .= (i * ((j * g) * f)) by A1, A3, CAT_1: 25

      .= ( id a) by A1, A2, A4, CAT_1: 28;

    end;

    theorem :: CAT_3:26

    ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} & (g * f) is retraction implies g is retraction

    proof

      assume

       A1: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} ;

      assume

       A2: ( Hom (a,c)) <> {} & ( Hom (c,a)) <> {} ;

      given i be Morphism of c, a such that

       A3: ((g * f) * i) = ( id c);

      thus

       A4: ( Hom (b,c)) <> {} & ( Hom (c,b)) <> {} by A2, A1, CAT_1: 24;

      take (f * i);

      thus (g * (f * i)) = ( id c) by A2, A3, A4, A1, CAT_1: 25;

    end;

    theorem :: CAT_3:27

    ( Hom (b,c)) <> {} & ( Hom (c,b)) <> {} & (g * f) is coretraction implies f is coretraction

    proof

      assume

       A1: ( Hom (b,c)) <> {} & ( Hom (c,b)) <> {} ;

      assume

       A2: ( Hom (a,c)) <> {} & ( Hom (c,a)) <> {} ;

      given i be Morphism of c, a such that

       A3: (i * (g * f)) = ( id a);

      thus

       A4: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} by A1, A2, CAT_1: 24;

      take (i * g);

      thus ((i * g) * f) = ( id a) by A4, A1, A2, A3, CAT_1: 25;

    end;

    theorem :: CAT_3:28

    f is retraction & f is monic implies f is invertible

    proof

      assume

       A1: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} ;

      given i be Morphism of b, a such that

       A2: (f * i) = ( id b);

      assume

       A3: f is monic;

      thus ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} by A1;

      take i;

      thus (f * i) = ( id b) by A2;

      

       A4: (f * (i * f)) = (( id b) * f) by A1, A2, CAT_1: 25

      .= f by A1, CAT_1: 28

      .= (f * ( id a)) by A1, CAT_1: 29;

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

      hence (i * f) = ( id a) by A3, A4;

    end;

    theorem :: CAT_3:29

    

     Th29: f is coretraction & f is epi implies f is invertible

    proof

      assume

       A1: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} ;

      given i be Morphism of b, a such that

       A2: (i * f) = ( id a);

      assume

       A3: f is epi;

      thus ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} by A1;

      take i;

      

       A4: ((f * i) * f) = (f * ( id a)) by A1, A2, CAT_1: 25

      .= f by A1, CAT_1: 29

      .= (( id b) * f) by A1, CAT_1: 28;

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

      hence (f * i) = ( id b) by A3, A4;

      thus (i * f) = ( id a) by A2;

    end;

    theorem :: CAT_3:30

    f is invertible iff f is retraction & f is coretraction by Th22, Th29;

    definition

      let C, a, b;

      let D;

      let T be Functor of C, D, f be Morphism of a, b;

      :: CAT_3:def10

      func T /. f -> Morphism of (T . a), (T . b) equals

      : Def10: (T . f);

      coherence

      proof

        f in ( Hom (a,b)) by A1, CAT_1:def 5;

        then (T . f) in ( Hom ((T . a),(T . b))) by CAT_1: 81;

        hence thesis by CAT_1:def 5;

      end;

    end

    

     Lm1: for T be Functor of C, D, a,b,c be Object of C st ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} holds for f be Morphism of a, b, g be Morphism of b, c holds (T /. (g * f)) = ((T /. g) * (T /. f))

    proof

      let T be Functor of C, D, a,b,c be Object of C such that

       A1: ( Hom (a,b)) <> {} & ( Hom (b,c)) <> {} ;

      let f be Morphism of a, b, g be Morphism of b, c;

      

       A2: ( cod f) = b by A1, CAT_1: 5

      .= ( dom g) by A1, CAT_1: 5;

      reconsider gg = g, ff = f as Morphism of C;

      

       A3: ( Hom (a,c)) <> {} by A1, CAT_1: 24;

      

       A4: (T /. g) = (T . gg) by Def10, A1;

      

       A5: (T /. f) = (T . ff) by Def10, A1;

      

       A6: ( Hom ((T . a),(T . b))) <> {} & ( Hom ((T . b),(T . c))) <> {} by A1, CAT_1: 84;

      (g * f) = (gg (*) ff) by A1, CAT_1:def 13;

      

      hence (T /. (g * f)) = (T . (gg (*) ff)) by Def10, A3

      .= ((T . gg) (*) (T . ff)) by A2, CAT_1: 64

      .= ((T /. g) * (T /. f)) by A6, A4, A5, CAT_1:def 13;

    end;

    

     Lm2: for T be Functor of C, D, c be Object of C holds (T /. ( id c)) = ( id (T . c))

    proof

      let T be Functor of C, D, c be Object of C;

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

      

      hence (T /. ( id c)) = (T . ( id c)) by Def10

      .= ( id (T . c)) by CAT_1: 71;

    end;

    theorem :: CAT_3:31

    for T be Functor of C, D st f is retraction holds (T /. f) is retraction

    proof

      let T be Functor of C, D;

      assume

       A1: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} ;

      given i be Morphism of b, a such that

       A2: (f * i) = ( id b);

      thus ( Hom ((T . a),(T . b))) <> {} & ( Hom ((T . b),(T . a))) <> {} by A1, CAT_1: 84;

      take (T /. i);

      

      thus ((T /. f) * (T /. i)) = (T /. ( id b)) by A1, A2, Lm1

      .= ( id (T . b)) by Lm2;

    end;

    theorem :: CAT_3:32

    for T be Functor of C, D st f is coretraction holds (T /. f) is coretraction

    proof

      let T be Functor of C, D;

      assume

       A1: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} ;

      given i be Morphism of b, a such that

       A2: (i * f) = ( id a);

      thus ( Hom ((T . a),(T . b))) <> {} & ( Hom ((T . b),(T . a))) <> {} by A1, CAT_1: 84;

      take (T /. i);

      

      thus ((T /. i) * (T /. f)) = (T /. ( id a)) by A1, A2, Lm1

      .= ( id (T . a)) by Lm2;

    end;

    theorem :: CAT_3:33

    f is retraction iff (f opp ) is coretraction

    proof

      thus f is retraction implies (f opp ) is coretraction

      proof

        assume

         A1: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} ;

        given i be Morphism of b, a such that

         A2: (f * i) = ( id b);

        thus ( Hom ((b opp ),(a opp ))) <> {} & ( Hom ((a opp ),(b opp ))) <> {} by A1, OPPCAT_1: 5;

        take (i opp );

        

        thus ((i opp ) * (f opp )) = ( id b) by A1, A2, OPPCAT_1: 70

        .= ( id (b opp )) by OPPCAT_1: 71;

      end;

      assume

       A3: ( Hom ((b opp ),(a opp ))) <> {} & ( Hom ((a opp ),(b opp ))) <> {} ;

      given i be Morphism of (a opp ), (b opp ) such that

       A4: (i * (f opp )) = ( id (b opp ));

      thus

       A5: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} by A3, OPPCAT_1: 5;

      take ( opp i);

      

       A6: (( opp i) opp ) = ( opp i) by A5, OPPCAT_1:def 6

      .= i by A3, OPPCAT_1:def 7;

      

      thus (f * ( opp i)) = ( id (b opp )) by A4, A6, A5, OPPCAT_1: 70

      .= ( id b) by OPPCAT_1: 71;

    end;

    theorem :: CAT_3:34

    f is coretraction iff (f opp ) is retraction

    proof

      thus f is coretraction implies (f opp ) is retraction

      proof

        assume

         A1: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} ;

        given i be Morphism of b, a such that

         A2: (i * f) = ( id a);

        thus ( Hom ((b opp ),(a opp ))) <> {} & ( Hom ((a opp ),(b opp ))) <> {} by A1, OPPCAT_1: 5;

        take (i opp );

        

        thus ((f opp ) * (i opp )) = ( id a) by A1, A2, OPPCAT_1: 70

        .= ( id (a opp )) by OPPCAT_1: 71;

      end;

      assume

       A3: ( Hom ((b opp ),(a opp ))) <> {} & ( Hom ((a opp ),(b opp ))) <> {} ;

      given i be Morphism of (a opp ), (b opp ) such that

       A4: ((f opp ) * i) = ( id (a opp ));

      thus

       A5: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} by A3, OPPCAT_1: 5;

      take ( opp i);

      (( opp i) opp ) = ( opp i) by A5, OPPCAT_1:def 6

      .= i by A3, OPPCAT_1:def 7;

      

      hence (( opp i) * f) = ((f opp ) * i) by A5, OPPCAT_1: 70

      .= ( id (a opp )) by A4

      .= ( id a) by OPPCAT_1: 71;

    end;

    begin

    reserve f,g for Morphism of C;

    definition

      let C, a, b;

      assume

       A1: b is terminal;

      :: CAT_3:def11

      func term (a,b) -> Morphism of a, b means not contradiction;

      existence ;

      uniqueness

      proof

        let f1,f2 be Morphism of a, b;

        consider f be Morphism of a, b such that

         A2: for g be Morphism of a, b holds f = g by A1;

        

        thus f1 = f by A2

        .= f2 by A2;

      end;

    end

    theorem :: CAT_3:35

    

     Th35: b is terminal implies ( dom ( term (a,b))) = a & ( cod ( term (a,b))) = b

    proof

      assume b is terminal;

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

      hence thesis by CAT_1: 5;

    end;

    theorem :: CAT_3:36

    

     Th36: b is terminal & ( dom f) = a & ( cod f) = b implies ( term (a,b)) = f

    proof

      assume that

       A1: b is terminal and

       A2: ( dom f) = a & ( cod f) = b;

      consider h be Morphism of a, b such that

       A3: for g be Morphism of a, b holds h = g by A1;

      f is Morphism of a, b by A2, CAT_1: 4;

      

      hence f = h by A3

      .= ( term (a,b)) by A3;

    end;

    theorem :: CAT_3:37

    for f be Morphism of a, b st b is terminal holds ( term (a,b)) = f

    proof

      let f be Morphism of a, b;

      assume

       A1: b is terminal;

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

      then ( dom f) = a & ( cod f) = b by CAT_1: 5;

      hence thesis by A1, Th36;

    end;

    begin

    definition

      let C, a, b;

      assume

       A1: a is initial;

      :: CAT_3:def12

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

      existence ;

      uniqueness

      proof

        let f1,f2 be Morphism of a, b;

        consider f be Morphism of a, b such that

         A2: for g be Morphism of a, b holds f = g by A1;

        

        thus f1 = f by A2

        .= f2 by A2;

      end;

    end

    theorem :: CAT_3:38

    

     Th38: a is initial implies ( dom ( init (a,b))) = a & ( cod ( init (a,b))) = b

    proof

      assume a is initial;

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

      hence thesis by CAT_1: 5;

    end;

    theorem :: CAT_3:39

    

     Th39: a is initial & ( dom f) = a & ( cod f) = b implies ( init (a,b)) = f

    proof

      assume that

       A1: a is initial and

       A2: ( dom f) = a & ( cod f) = b;

      consider h be Morphism of a, b such that

       A3: for g be Morphism of a, b holds h = g by A1;

      f is Morphism of a, b by A2, CAT_1: 4;

      

      hence f = h by A3

      .= ( init (a,b)) by A3;

    end;

    theorem :: CAT_3:40

    for f be Morphism of a, b st a is initial holds ( init (a,b)) = f

    proof

      let f be Morphism of a, b;

      assume

       A1: a is initial;

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

      then ( dom f) = a & ( cod f) = b by CAT_1: 5;

      hence thesis by A1, Th39;

    end;

    begin

    definition

      let C, a, I;

      :: CAT_3:def13

      mode Projections_family of a,I -> Function of I, the carrier' of C means

      : Def13: ( doms it ) = (I --> a);

      existence

      proof

        take F = (I --> ( id a));

        ( doms F) = (I --> ( dom ( id a))) by Th4;

        hence thesis;

      end;

    end

    theorem :: CAT_3:41

    

     Th41: for F be Projections_family of a, I st x in I holds ( dom (F /. x)) = a

    proof

      let F be Projections_family of a, I such that

       A1: x in I;

      (( doms F) /. x) = ((I --> a) /. x) by Def13;

      

      hence ( dom (F /. x)) = ((I --> a) /. x) by A1, Def1

      .= a by A1, Th2;

    end;

    theorem :: CAT_3:42

    

     Th42: for F be Function of {} , the carrier' of C holds F is Projections_family of a, {}

    proof

      let F be Function of {} , the carrier' of C;

      thus ( {} --> a) = ( doms F);

    end;

    theorem :: CAT_3:43

    

     Th43: ( dom f) = a implies (y .--> f) is Projections_family of a, {y}

    proof

      set F = (y .--> f);

      assume

       A1: ( dom f) = a;

      now

        let x;

        assume

         A2: x in {y};

        

        hence (( doms F) /. x) = ( dom (F /. x)) by Def1

        .= a by A1, A2, Th2

        .= ((y .--> a) /. x) by A2, Th2;

      end;

      hence ( doms F) = ( {y} --> a) by Th1;

    end;

    theorem :: CAT_3:44

    

     Th44: ( dom p1) = a & ( dom p2) = a implies ((x1,x2) --> (p1,p2)) is Projections_family of a, {x1, x2}

    proof

      assume

       A1: ( dom p1) = a & ( dom p2) = a;

      ( doms ((x1,x2) --> (p1,p2))) = ((x1,x2) --> (( dom p1),( dom p2))) by Th6

      .= ( {x1, x2} --> a) by A1, FUNCT_4: 65;

      hence thesis by Def13;

    end;

    theorem :: CAT_3:45

    

     Th45: for F be Projections_family of a, I st ( cod f) = a holds (F * f) is Projections_family of ( dom f), I

    proof

      let F be Projections_family of a, I;

      assume ( cod f) = a;

      then ( doms F) = (I --> ( cod f)) by Def13;

      hence ( doms (F * f)) = (I --> ( dom f)) by Th16;

    end;

    theorem :: CAT_3:46

    for F be Function of I, the carrier' of C, G be Projections_family of a, I st ( doms F) = ( cods G) holds (F "*" G) is Projections_family of a, I

    proof

      let F be Function of I, the carrier' of C;

      let G be Projections_family of a, I;

      assume ( doms F) = ( cods G);

      then ( doms (F "*" G)) = ( doms G) by Th18;

      hence ( doms (F "*" G)) = (I --> a) by Def13;

    end;

    theorem :: CAT_3:47

    for F be Projections_family of ( cod f), I holds ((f opp ) * (F opp )) = ((F * f) opp )

    proof

      let F be Projections_family of ( cod f), I;

      now

        let x;

        assume

         A1: x in I;

        

        then

         A2: ( dom (F /. x)) = (( doms F) /. x) by Def1

        .= ((I --> ( cod f)) /. x) by Def13

        .= ( cod f) by A1, Th2;

        reconsider ff = f as Morphism of ( dom f), ( cod f) by CAT_1: 4;

        reconsider gg = (F /. x) as Morphism of ( cod f), ( cod (F /. x)) by A2, CAT_1: 4;

        

         A3: ( Hom (( dom f),( cod f))) <> {} & ( Hom (( dom (F /. x)),( cod (F /. x)))) <> {} by CAT_1: 2;

        then

         A4: (ff opp ) = (f opp ) by OPPCAT_1:def 6;

        

         A5: (gg opp ) = ((F /. x) opp ) by A3, A2, OPPCAT_1:def 6;

        

        thus (((f opp ) * (F opp )) /. x) = ((f opp ) (*) ((F opp ) /. x)) by A1, Def6

        .= ((f opp ) (*) ((F /. x) opp )) by A1, Def3

        .= ((gg (*) ff) opp ) by A2, A4, A5, A3, OPPCAT_1: 16

        .= (((F * f) /. x) opp ) by A1, Def5

        .= (((F * f) opp ) /. x) by A1, Def3;

      end;

      hence thesis by Th1;

    end;

    definition

      let C, a, I;

      let F be Function of I, the carrier' of C;

      :: CAT_3:def14

      pred a is_a_product_wrt F means F is Projections_family of a, I & for b holds for F9 be Projections_family of b, I st ( cods F) = ( cods F9) holds ex h st h in ( Hom (b,a)) & for k st k in ( Hom (b,a)) holds (for x st x in I holds ((F /. x) (*) k) = (F9 /. x)) iff h = k;

    end

    theorem :: CAT_3:48

    

     Th48: for F be Projections_family of c, I, F9 be Projections_family of d, I st c is_a_product_wrt F & d is_a_product_wrt F9 & ( cods F) = ( cods F9) holds (c,d) are_isomorphic

    proof

      let F be Projections_family of c, I, F9 be Projections_family of d, I such that

       A1: c is_a_product_wrt F and

       A2: d is_a_product_wrt F9 and

       A3: ( cods F) = ( cods F9);

      consider gf be Morphism of C such that gf in ( Hom (d,d)) and

       A4: for k st k in ( Hom (d,d)) holds (for x st x in I holds ((F9 /. x) (*) k) = (F9 /. x)) iff gf = k by A2;

      consider f such that

       A5: f in ( Hom (d,c)) and

       A6: for k st k in ( Hom (d,c)) holds (for x st x in I holds ((F /. x) (*) k) = (F9 /. x)) iff f = k by A1, A3;

      reconsider f as Morphism of d, c by A5, CAT_1:def 5;

      consider fg be Morphism of C such that fg in ( Hom (c,c)) and

       A7: for k st k in ( Hom (c,c)) holds (for x st x in I holds ((F /. x) (*) k) = (F /. x)) iff fg = k by A1;

      consider g such that

       A8: g in ( Hom (c,d)) and

       A9: for k st k in ( Hom (c,d)) holds (for x st x in I holds ((F9 /. x) (*) k) = (F /. x)) iff g = k by A2, A3;

      reconsider g as Morphism of c, d by A8, CAT_1:def 5;

      

       A10: ( cod g) = d by A8, CAT_1: 1;

       A11:

      now

        set k = ( id c);

        thus k in ( Hom (c,c)) by CAT_1: 27;

        let x;

        assume x in I;

        then ( dom (F /. x)) = c by Th41;

        hence ((F /. x) (*) k) = (F /. x) by CAT_1: 22;

      end;

       A12:

      now

        set k = ( id d);

        thus k in ( Hom (d,d)) by CAT_1: 27;

        let x;

        assume x in I;

        then ( dom (F9 /. x)) = d by Th41;

        hence ((F9 /. x) (*) k) = (F9 /. x) by CAT_1: 22;

      end;

      take g;

      thus ( Hom (c,d)) <> {} & ( Hom (d,c)) <> {} by A5, A8;

      take f;

      

       A13: ( dom g) = c by A8, CAT_1: 1;

      

       A14: ( cod f) = c by A5, CAT_1: 1;

      

       A15: ( dom f) = d by A5, CAT_1: 1;

       A16:

      now

        ( dom (g (*) f)) = d & ( cod (g (*) f)) = d by A15, A10, A14, A13, CAT_1: 17;

        hence (g (*) f) in ( Hom (d,d));

        let x;

        assume

         A17: x in I;

        then ( dom (F9 /. x)) = d by Th41;

        

        hence ((F9 /. x) (*) (g (*) f)) = (((F9 /. x) (*) g) (*) f) by A10, A14, A13, CAT_1: 18

        .= ((F /. x) (*) f) by A8, A9, A17

        .= (F9 /. x) by A5, A6, A17;

      end;

      

      thus (g * f) = (g (*) f) by A5, A8, CAT_1:def 13

      .= gf by A4, A16

      .= ( id d) by A4, A12;

       A18:

      now

        ( dom (f (*) g)) = c & ( cod (f (*) g)) = c by A15, A10, A14, A13, CAT_1: 17;

        hence (f (*) g) in ( Hom (c,c));

        let x;

        assume

         A19: x in I;

        then ( dom (F /. x)) = c by Th41;

        

        hence ((F /. x) (*) (f (*) g)) = (((F /. x) (*) f) (*) g) by A15, A10, A14, CAT_1: 18

        .= ((F9 /. x) (*) g) by A5, A6, A19

        .= (F /. x) by A8, A9, A19;

      end;

      

      thus (f * g) = (f (*) g) by A5, A8, CAT_1:def 13

      .= fg by A7, A18

      .= ( id c) by A11, A7;

    end;

    theorem :: CAT_3:49

    

     Th49: for F be Projections_family of c, I st c is_a_product_wrt F & for x1, x2 st x1 in I & x2 in I holds ( Hom (( cod (F /. x1)),( cod (F /. x2)))) <> {} holds for x st x in I holds for d be Object of C st d = ( cod (F /. x)) & ( Hom (c,d)) <> {} holds for f be Morphism of c, d st f = (F /. x) holds f is retraction

    proof

      let F be Projections_family of c, I such that

       A1: c is_a_product_wrt F and

       A2: for x1, x2 st x1 in I & x2 in I holds ( Hom (( cod (F /. x1)),( cod (F /. x2)))) <> {} ;

      let x such that

       A3: x in I;

      let d be Object of C such that

       A4: d = ( cod (F /. x)) and

       A5: ( Hom (c,d)) <> {} ;

      let f be Morphism of c, d such that

       A6: f = (F /. x);

      defpred P[ object, object] means ($1 = x implies $2 = ( id d)) & ($1 <> x implies $2 in ( Hom (d,( cod (F /. $1)))));

      

       A7: for y be object st y in I holds ex z be object st z in the carrier' of C & P[y, z]

      proof

        let y be object;

        set z = the Element of ( Hom (d,( cod (F /. y))));

        assume y in I;

        then

         A8: ( Hom (d,( cod (F /. y)))) <> {} by A2, A3, A4;

        then

         A9: z in ( Hom (d,( cod (F /. y))));

        per cases ;

          suppose

           A10: y = x;

          take z = ( id d);

          thus z in the carrier' of C;

          thus thesis by A10;

        end;

          suppose

           A11: y <> x;

          take z;

          thus z in the carrier' of C by A9;

          thus thesis by A8, A11;

        end;

      end;

      consider F9 be Function such that

       A12: ( dom F9) = I & ( rng F9) c= the carrier' of C and

       A13: for y be object st y in I holds P[y, (F9 . y)] from FUNCT_1:sch 6( A7);

      reconsider F9 as Function of I, the carrier' of C by A12, FUNCT_2:def 1, RELSET_1: 4;

      now

        let y;

        assume

         A14: y in I;

        then

         A15: (F9 . y) = (F9 /. y) by FUNCT_2:def 13;

        then

         A16: y <> x implies (F9 /. y) in ( Hom (d,( cod (F /. y)))) by A13, A14;

        y = x implies (F9 /. y) = ( id d) by A13, A14, A15;

        then ( dom (F9 /. y)) = d by A16, CAT_1: 1;

        

        hence (( doms F9) /. y) = d by A14, Def1

        .= ((I --> d) /. y) by A14, Th2;

      end;

      then

       A17: F9 is Projections_family of d, I by Def13, Th1;

      now

        let y;

        assume

         A18: y in I;

        then

         A19: (F9 . y) = (F9 /. y) by FUNCT_2:def 13;

        then

         A20: y <> x implies (F9 /. y) in ( Hom (d,( cod (F /. y)))) by A13, A18;

        y = x implies (F9 /. y) = ( id d) by A13, A18, A19;

        then ( cod (F9 /. y)) = ( cod (F /. y)) by A20, A4, CAT_1: 1;

        

        hence (( cods F9) /. y) = ( cod (F /. y)) by A18, Def2

        .= (( cods F) /. y) by A18, Def2;

      end;

      then

      consider i such that

       A21: i in ( Hom (d,c)) and

       A22: for k st k in ( Hom (d,c)) holds (for y st y in I holds ((F /. y) (*) k) = (F9 /. y)) iff i = k by A1, A17, Th1;

      reconsider i as Morphism of d, c by A21, CAT_1:def 5;

      thus ( Hom (c,d)) <> {} & ( Hom (d,c)) <> {} by A21, A5;

      take i;

      

      thus (f * i) = (f (*) i) by A21, A5, CAT_1:def 13

      .= (F9 /. x) by A3, A21, A22, A6

      .= (F9 . x) by A3, FUNCT_2:def 13

      .= ( id d) by A3, A13;

    end;

    theorem :: CAT_3:50

    

     Th50: for F be Function of {} , the carrier' of C holds a is_a_product_wrt F iff a is terminal

    proof

      let F be Function of {} , the carrier' of C;

      thus a is_a_product_wrt F implies a is terminal

      proof

        assume

         A1: a is_a_product_wrt F;

        let b;

        set F9 = the Projections_family of b, {} ;

        consider h such that

         A2: h in ( Hom (b,a)) and

         A3: for k st k in ( Hom (b,a)) holds (for x st x in {} holds ((F /. x) (*) k) = (F9 /. x)) iff h = k by A1;

        thus ( Hom (b,a)) <> {} by A2;

        reconsider f = h as Morphism of b, a by A2, CAT_1:def 5;

        take f;

        let g be Morphism of b, a;

        

         A4: for x st x in {} holds ((F /. x) (*) g) = (F9 /. x);

        g in ( Hom (b,a)) by A2, CAT_1:def 5;

        hence thesis by A3, A4;

      end;

      assume

       A5: a is terminal;

      thus F is Projections_family of a, {} by Th42;

      let b;

      consider h be Morphism of b, a such that

       A6: for g be Morphism of b, a holds h = g by A5;

      let F9 be Projections_family of b, {} such that ( cods F) = ( cods F9);

      take h;

      ( Hom (b,a)) <> {} by A5;

      hence h in ( Hom (b,a)) by CAT_1:def 5;

      let k;

      assume k in ( Hom (b,a));

      then k is Morphism of b, a by CAT_1:def 5;

      hence thesis by A6;

    end;

    theorem :: CAT_3:51

    

     Th51: for F be Projections_family of a, I st a is_a_product_wrt F holds for f be Morphism of b, a st ( dom f) = b & ( cod f) = a & f is invertible holds b is_a_product_wrt (F * f)

    proof

      let F be Projections_family of a, I such that

       A1: a is_a_product_wrt F;

      let f be Morphism of b, a such that

       A2: ( dom f) = b and

       A3: ( cod f) = a and

       A4: f is invertible;

      thus (F * f) is Projections_family of b, I by A2, A3, Th45;

      let c;

      

       A5: ( doms F) = (I --> ( cod f)) by A3, Def13;

      let F9 be Projections_family of c, I;

      assume ( cods (F * f)) = ( cods F9);

      then ( cods F) = ( cods F9) by A5, Th16;

      then

      consider h such that

       A6: h in ( Hom (c,a)) and

       A7: for k st k in ( Hom (c,a)) holds (for x st x in I holds ((F /. x) (*) k) = (F9 /. x)) iff h = k by A1;

      

       A8: ( cod h) = a by A6, CAT_1: 1;

      consider g be Morphism of a, b such that

       A9: (f * g) = ( id a) and

       A10: (g * f) = ( id b) by A4;

      

       A11: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} by A4;

      then

       A12: ( dom g) = ( cod f) by A3, CAT_1: 5;

      

       A13: ( cod g) = ( dom f) by A2, A11, CAT_1: 5;

      

       A14: (f (*) g) = ( id ( cod f)) by A9, A3, A11, CAT_1:def 13;

      

       A15: (g (*) f) = ( id ( dom f)) by A10, A2, A11, CAT_1:def 13;

      ( dom h) = c by A6, CAT_1: 1;

      then

       A16: ( dom (g (*) h)) = c by A3, A12, A8, CAT_1: 17;

      take gh = (g (*) h);

      ( cod (g (*) h)) = b by A2, A3, A12, A13, A8, CAT_1: 17;

      hence gh in ( Hom (c,b)) by A16;

      let k;

      assume

       A17: k in ( Hom (c,b));

      then

       A18: ( cod k) = b by CAT_1: 1;

      

       A19: ( dom k) = c by A17, CAT_1: 1;

      thus (for x st x in I holds (((F * f) /. x) (*) k) = (F9 /. x)) implies gh = k

      proof

        assume

         A20: for x st x in I holds (((F * f) /. x) (*) k) = (F9 /. x);

        now

          ( dom (f (*) k)) = c & ( cod (f (*) k)) = a by A2, A3, A19, A18, CAT_1: 17;

          hence (f (*) k) in ( Hom (c,a));

          let x;

          assume

           A21: x in I;

          then ( dom (F /. x)) = a by Th41;

          

          hence ((F /. x) (*) (f (*) k)) = (((F /. x) (*) f) (*) k) by A2, A3, A18, CAT_1: 18

          .= (((F * f) /. x) (*) k) by A21, Def5

          .= (F9 /. x) by A20, A21;

        end;

        then (g (*) (f (*) k)) = (g (*) h) by A7;

        

        hence gh = (( id b) (*) k) by A2, A12, A15, A18, CAT_1: 18

        .= k by A18, CAT_1: 21;

      end;

      assume

       A22: gh = k;

      let x;

      assume

       A23: x in I;

      then

       A24: ( dom (F /. x)) = a by Th41;

      

      thus (((F * f) /. x) (*) k) = (((F /. x) (*) f) (*) k) by A23, Def5

      .= ((F /. x) (*) (f (*) (g (*) h))) by A2, A3, A18, A22, A24, CAT_1: 18

      .= ((F /. x) (*) (( id ( cod f)) (*) h)) by A3, A12, A13, A14, A8, CAT_1: 18

      .= ((F /. x) (*) h) by A3, A8, CAT_1: 21

      .= (F9 /. x) by A6, A7, A23;

    end;

    theorem :: CAT_3:52

    a is_a_product_wrt (y .--> ( id a))

    proof

      set F = (y .--> ( id a));

      ( dom ( id a)) = a;

      hence F is Projections_family of a, {y} by Th43;

      let b;

      let F9 be Projections_family of b, {y} such that

       A1: ( cods F) = ( cods F9);

      take h = (F9 /. y);

      

       A2: y in {y} by TARSKI:def 1;

      then

       A3: ( dom h) = b by Th41;

      ( cod h) = (( cods F) /. y) by A1, A2, Def2

      .= ( cod (F /. y)) by A2, Def2

      .= ( cod ( id a)) by A2, Th2

      .= a;

      hence h in ( Hom (b,a)) by A3;

      let k;

      assume k in ( Hom (b,a));

      then

       A4: ( cod k) = a by CAT_1: 1;

      thus (for x st x in {y} holds ((F /. x) (*) k) = (F9 /. x)) implies h = k

      proof

        assume

         A5: for x st x in {y} holds ((F /. x) (*) k) = (F9 /. x);

        

        thus k = (( id a) (*) k) by A4, CAT_1: 21

        .= ((F /. y) (*) k) by A2, Th2

        .= h by A2, A5;

      end;

      assume

       A6: h = k;

      let x;

      assume

       A7: x in {y};

      

      hence (F9 /. x) = k by A6, TARSKI:def 1

      .= (( id a) (*) k) by A4, CAT_1: 21

      .= ((F /. x) (*) k) by A7, Th2;

    end;

    theorem :: CAT_3:53

    for F be Projections_family of a, I st a is_a_product_wrt F & for x st x in I holds ( cod (F /. x)) is terminal holds a is terminal

    proof

      let F be Projections_family of a, I such that

       A1: a is_a_product_wrt F and

       A2: for x st x in I holds ( cod (F /. x)) is terminal;

      now

        thus I = {} implies a is terminal by A1, Th50;

        let b;

        deffunc f( set) = ( term (b,( cod (F /. $1))));

        consider F9 be Function of I, the carrier' of C such that

         A3: for x st x in I holds (F9 /. x) = f(x) from LambdaIdx;

        now

          let x;

          assume

           A4: x in I;

          then

           A5: ( cod (F /. x)) is terminal by A2;

          

          thus (( doms F9) /. x) = ( dom (F9 /. x)) by A4, Def1

          .= ( dom ( term (b,( cod (F /. x))))) by A3, A4

          .= b by A5, Th35

          .= ((I --> b) /. x) by A4, Th2;

        end;

        then

        reconsider F9 as Projections_family of b, I by Def13, Th1;

        now

          let x;

          assume

           A6: x in I;

          then

           A7: ( cod (F /. x)) is terminal by A2;

          

          thus (( cods F) /. x) = ( cod (F /. x)) by A6, Def2

          .= ( cod ( term (b,( cod (F /. x))))) by A7, Th35

          .= ( cod (F9 /. x)) by A3, A6

          .= (( cods F9) /. x) by A6, Def2;

        end;

        then

        consider h such that

         A8: h in ( Hom (b,a)) and

         A9: for k st k in ( Hom (b,a)) holds (for x st x in I holds ((F /. x) (*) k) = (F9 /. x)) iff h = k by A1, Th1;

        thus ( Hom (b,a)) <> {} by A8;

        reconsider h as Morphism of b, a by A8, CAT_1:def 5;

        take h;

        let g be Morphism of b, a;

        now

          thus g in ( Hom (b,a)) by A8, CAT_1:def 5;

          let x;

          set c = ( cod (F /. x));

          

           A10: ( cod g) = a by A8, CAT_1: 5;

          assume

           A11: x in I;

          then c is terminal by A2;

          then

          consider f be Morphism of b, c such that

           A12: for f9 be Morphism of b, c holds f = f9;

          

           A13: ( dom (F /. x)) = a by A11, Th41;

          then

           A14: ( cod ((F /. x) (*) g)) = c by A10, CAT_1: 17;

          ( dom g) = b by A8, CAT_1: 5;

          then ( dom ((F /. x) (*) g)) = b by A10, A13, CAT_1: 17;

          then ((F /. x) (*) g) in ( Hom (b,c)) by A14;

          then

           A15: ((F /. x) (*) g) is Morphism of b, c by CAT_1:def 5;

          (F9 /. x) = ( term (b,c)) by A3, A11;

          

          hence (F9 /. x) = f by A12

          .= ((F /. x) (*) g) by A12, A15;

        end;

        hence h = g by A9;

      end;

      hence thesis;

    end;

    definition

      let C, c, p1, p2;

      :: CAT_3:def15

      pred c is_a_product_wrt p1,p2 means ( dom p1) = c & ( dom p2) = c & for d, f, g st f in ( Hom (d,( cod p1))) & g in ( Hom (d,( cod p2))) holds ex h st h in ( Hom (d,c)) & for k st k in ( Hom (d,c)) holds (p1 (*) k) = f & (p2 (*) k) = g iff h = k;

    end

    theorem :: CAT_3:54

    

     Th54: x1 <> x2 implies (c is_a_product_wrt (p1,p2) iff c is_a_product_wrt ((x1,x2) --> (p1,p2)))

    proof

      set F = ((x1,x2) --> (p1,p2)), I = {x1, x2};

      assume

       A1: x1 <> x2;

      thus c is_a_product_wrt (p1,p2) implies c is_a_product_wrt F

      proof

        assume

         A2: c is_a_product_wrt (p1,p2);

        then ( dom p1) = c & ( dom p2) = c;

        hence F is Projections_family of c, I by Th44;

        let b;

        let F9 be Projections_family of b, I such that

         A3: ( cods F) = ( cods F9);

        set f = (F9 /. x1), g = (F9 /. x2);

        

         A4: x1 in I by TARSKI:def 2;

        then (( cods F) /. x1) = ( cod (F /. x1)) by Def2;

        then ( cod f) = ( cod (F /. x1)) by A3, A4, Def2;

        then

         A5: ( cod f) = ( cod p1) by A1, Th3;

        

         A6: x2 in I by TARSKI:def 2;

        then (( cods F) /. x2) = ( cod (F /. x2)) by Def2;

        then ( cod g) = ( cod (F /. x2)) by A3, A6, Def2;

        then

         A7: ( cod g) = ( cod p2) by A1, Th3;

        ( dom g) = b by A6, Th41;

        then

         A8: g in ( Hom (b,( cod p2))) by A7;

        ( dom f) = b by A4, Th41;

        then f in ( Hom (b,( cod p1))) by A5;

        then

        consider h such that

         A9: h in ( Hom (b,c)) and

         A10: for k st k in ( Hom (b,c)) holds (p1 (*) k) = f & (p2 (*) k) = g iff h = k by A2, A8;

        take h;

        thus h in ( Hom (b,c)) by A9;

        let k such that

         A11: k in ( Hom (b,c));

        thus (for x st x in I holds ((F /. x) (*) k) = (F9 /. x)) implies h = k

        proof

          assume

           A12: for x st x in I holds ((F /. x) (*) k) = (F9 /. x);

          then ((F /. x2) (*) k) = g by A6;

          then

           A13: (p2 (*) k) = g by A1, Th3;

          ((F /. x1) (*) k) = f by A4, A12;

          then (p1 (*) k) = f by A1, Th3;

          hence thesis by A10, A11, A13;

        end;

        assume h = k;

        then

         A14: (p1 (*) k) = f & (p2 (*) k) = g by A10, A11;

        let x;

        assume x in I;

        then x = x1 or x = x2 by TARSKI:def 2;

        hence thesis by A1, A14, Th3;

      end;

      assume

       A15: c is_a_product_wrt F;

      then

       A16: F is Projections_family of c, I;

      x2 in I by TARSKI:def 2;

      then

       A17: ( dom (F /. x2)) = c by A16, Th41;

      x1 in I by TARSKI:def 2;

      then ( dom (F /. x1)) = c by A16, Th41;

      hence ( dom p1) = c & ( dom p2) = c by A1, A17, Th3;

      let d, f, g such that

       A18: f in ( Hom (d,( cod p1))) and

       A19: g in ( Hom (d,( cod p2)));

      ( dom f) = d & ( dom g) = d by A18, A19, CAT_1: 1;

      then

      reconsider F9 = ((x1,x2) --> (f,g)) as Projections_family of d, I by Th44;

      ( cods F) = ((x1,x2) --> (( cod p1),( cod p2))) by Th7

      .= ((x1,x2) --> (( cod f),( cod p2))) by A18, CAT_1: 1

      .= ((x1,x2) --> (( cod f),( cod g))) by A19, CAT_1: 1

      .= ( cods F9) by Th7;

      then

      consider h such that

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

       A21: for k st k in ( Hom (d,c)) holds (for x st x in I holds ((F /. x) (*) k) = (F9 /. x)) iff h = k by A15;

      take h;

      thus h in ( Hom (d,c)) by A20;

      let k such that

       A22: k in ( Hom (d,c));

      thus (p1 (*) k) = f & (p2 (*) k) = g implies h = k

      proof

        assume

         A23: (p1 (*) k) = f & (p2 (*) k) = g;

        now

          let x;

          assume x in I;

          then x = x1 or x = x2 by TARSKI:def 2;

          then (F /. x) = p1 & (F9 /. x) = f or (F /. x) = p2 & (F9 /. x) = g by A1, Th3;

          hence ((F /. x) (*) k) = (F9 /. x) by A23;

        end;

        hence thesis by A21, A22;

      end;

      assume

       A24: h = k;

      x2 in I by TARSKI:def 2;

      then ((F /. x2) (*) k) = (F9 /. x2) by A21, A22, A24;

      then

       A25: ((F /. x2) (*) k) = g by A1, Th3;

      x1 in I by TARSKI:def 2;

      then ((F /. x1) (*) k) = (F9 /. x1) by A21, A22, A24;

      then ((F /. x1) (*) k) = f by A1, Th3;

      hence thesis by A1, A25, Th3;

    end;

    theorem :: CAT_3:55

    ( Hom (c,a)) <> {} & ( Hom (c,b)) <> {} implies for p1 be Morphism of c, a, p2 be Morphism of c, b holds c is_a_product_wrt (p1,p2) iff for d st ( Hom (d,a)) <> {} & ( Hom (d,b)) <> {} holds ( Hom (d,c)) <> {} & for f be Morphism of d, a, g be Morphism of d, b holds ex h be Morphism of d, c st for k be Morphism of d, c holds (p1 * k) = f & (p2 * k) = g iff h = k

    proof

      assume that

       A1: ( Hom (c,a)) <> {} and

       A2: ( Hom (c,b)) <> {} ;

      let p1 be Morphism of c, a, p2 be Morphism of c, b;

      thus c is_a_product_wrt (p1,p2) implies for d st ( Hom (d,a)) <> {} & ( Hom (d,b)) <> {} holds ( Hom (d,c)) <> {} & for f be Morphism of d, a, g be Morphism of d, b holds ex h be Morphism of d, c st for k be Morphism of d, c holds (p1 * k) = f & (p2 * k) = g iff h = k

      proof

        assume that ( dom p1) = c and ( dom p2) = c and

         A3: for d, f, g st f in ( Hom (d,( cod p1))) & g in ( Hom (d,( cod p2))) holds ex h st h in ( Hom (d,c)) & for k st k in ( Hom (d,c)) holds (p1 (*) k) = f & (p2 (*) k) = g iff h = k;

        let d such that

         A4: ( Hom (d,a)) <> {} and

         A5: ( Hom (d,b)) <> {} ;

        set f = the Morphism of d, a, g = the Morphism of d, b;

        

         A6: ( cod p2) = b by A2, CAT_1: 5;

        then

         A7: g in ( Hom (d,( cod p2))) by A5, CAT_1:def 5;

        

         A8: ( cod p1) = a by A1, CAT_1: 5;

        then f in ( Hom (d,( cod p1))) by A4, CAT_1:def 5;

        then

         A9: ex h st h in ( Hom (d,c)) & for k st k in ( Hom (d,c)) holds (p1 (*) k) = f & (p2 (*) k) = g iff h = k by A3, A7;

        hence ( Hom (d,c)) <> {} ;

        let f be Morphism of d, a, g be Morphism of d, b;

        

         A10: g in ( Hom (d,( cod p2))) by A5, A6, CAT_1:def 5;

        f in ( Hom (d,( cod p1))) by A4, A8, CAT_1:def 5;

        then

        consider h such that

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

         A12: for k st k in ( Hom (d,c)) holds (p1 (*) k) = f & (p2 (*) k) = g iff h = k by A3, A10;

        reconsider h as Morphism of d, c by A11, CAT_1:def 5;

        take h;

        let k be Morphism of d, c;

        

         A13: k in ( Hom (d,c)) by A9, CAT_1:def 5;

        (p1 * k) = (p1 (*) k qua Morphism of C) & (p2 * k) = (p2 (*) k qua Morphism of C) by A1, A2, A9, CAT_1:def 13;

        hence thesis by A12, A13;

      end;

      assume

       A14: for d st ( Hom (d,a)) <> {} & ( Hom (d,b)) <> {} holds ( Hom (d,c)) <> {} & for f be Morphism of d, a, g be Morphism of d, b holds ex h be Morphism of d, c st for k be Morphism of d, c holds (p1 * k) = f & (p2 * k) = g iff h = k;

      thus ( dom p1) = c & ( dom p2) = c by A1, A2, CAT_1: 5;

      let d, f, g such that

       A15: f in ( Hom (d,( cod p1))) and

       A16: g in ( Hom (d,( cod p2)));

      

       A17: ( Hom (d,a)) <> {} by A1, A15, CAT_1: 5;

      

       A18: ( cod p1) = a by A1, CAT_1: 5;

      then

       A19: f is Morphism of d, a by A15, CAT_1:def 5;

      

       A20: ( cod p2) = b by A2, CAT_1: 5;

      then g is Morphism of d, b by A16, CAT_1:def 5;

      then

      consider h be Morphism of d, c such that

       A21: for k be Morphism of d, c holds (p1 * k) = f & (p2 * k) = g iff h = k by A14, A16, A20, A19, A17;

      reconsider h9 = h as Morphism of C;

      take h9;

      

       A22: ( Hom (d,c)) <> {} by A14, A15, A16, A18, A20;

      hence h9 in ( Hom (d,c)) by CAT_1:def 5;

      let k;

      assume k in ( Hom (d,c));

      then

      reconsider k9 = k as Morphism of d, c by CAT_1:def 5;

      (p1 (*) k) = (p1 * k9) & (p2 (*) k) = (p2 * k9) by A1, A2, A22, CAT_1:def 13;

      hence thesis by A21;

    end;

    theorem :: CAT_3:56

    c is_a_product_wrt (p1,p2) & d is_a_product_wrt (q1,q2) & ( cod p1) = ( cod q1) & ( cod p2) = ( cod q2) implies (c,d) are_isomorphic

    proof

      assume that

       A1: c is_a_product_wrt (p1,p2) and

       A2: d is_a_product_wrt (q1,q2) and

       A3: ( cod p1) = ( cod q1) & ( cod p2) = ( cod q2);

      set I = { 0 , { 0 }}, F = (( 0 , { 0 }) --> (p1,p2)), F9 = (( 0 , { 0 }) --> (q1,q2));

      

       A4: c is_a_product_wrt F & d is_a_product_wrt F9 by A1, A2, Th54;

      ( cods F) = (( 0 , { 0 }) --> (( cod q1),( cod q2))) by A3, Th7

      .= ( cods F9) by Th7;

      hence thesis by A4, Th48;

    end;

    theorem :: CAT_3:57

    for p1 be Morphism of c, a, p2 be Morphism of c, b st ( Hom (c,a)) <> {} & ( Hom (c,b)) <> {} & c is_a_product_wrt (p1,p2) & ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} holds p1 is retraction & p2 is retraction

    proof

      let p1 be Morphism of c, a, p2 be Morphism of c, b such that

       A1: ( Hom (c,a)) <> {} & ( Hom (c,b)) <> {} and

       A2: c is_a_product_wrt (p1,p2) and

       A3: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} ;

      set I = { 0 , { 0 }};

      ( dom p1) = c & ( dom p2) = c by A2;

      then

      reconsider F = (( 0 , { 0 }) --> (p1,p2)) as Projections_family of c, I by Th44;

      

       A4: (F /. 0 ) = p1 by Th3;

      

       A5: (F /. { 0 }) = p2 by Th3;

       A6:

      now

        thus F is Projections_family of c, I;

        thus c is_a_product_wrt F by A2, Th54;

        let x1, x2;

        assume that

         A7: x1 in I and

         A8: x2 in I;

        

         A9: x2 = 0 or x2 = { 0 } by A8, TARSKI:def 2;

        x1 = 0 or x1 = { 0 } by A7, TARSKI:def 2;

        then

         A10: ( cod (F /. x1)) = a or ( cod (F /. x1)) = b by A4, A5, A1, CAT_1: 5;

        ( cod (F /. x2)) = a or ( cod (F /. x2)) = b by A9, A4, A5, A1, CAT_1: 5;

        hence ( Hom (( cod (F /. x1)),( cod (F /. x2)))) <> {} by A3, A10;

      end;

      

       A11: { 0 } in I by TARSKI:def 2;

      

       A12: 0 in I by TARSKI:def 2;

      ( cod (F /. 0 )) = a & ( cod (F /. { 0 })) = b by A4, A5, A1, CAT_1: 5;

      hence thesis by A4, A6, A11, Th49, A5, A1, A12;

    end;

    theorem :: CAT_3:58

    

     Th58: c is_a_product_wrt (p1,p2) & h in ( Hom (c,c)) & (p1 (*) h) = p1 & (p2 (*) h) = p2 implies h = ( id c)

    proof

      assume that

       A1: ( dom p1) = c & ( dom p2) = c and

       A2: for d, f, g st f in ( Hom (d,( cod p1))) & g in ( Hom (d,( cod p2))) holds ex h st h in ( Hom (d,c)) & for k st k in ( Hom (d,c)) holds (p1 (*) k) = f & (p2 (*) k) = g iff h = k and

       A3: h in ( Hom (c,c)) & (p1 (*) h) = p1 & (p2 (*) h) = p2;

      p1 in ( Hom (c,( cod p1))) & p2 in ( Hom (c,( cod p2))) by A1;

      then

      consider i such that i in ( Hom (c,c)) and

       A4: for k st k in ( Hom (c,c)) holds (p1 (*) k) = p1 & (p2 (*) k) = p2 iff i = k by A2;

      

       A5: ( id c) in ( Hom (c,c)) by CAT_1: 27;

      (p1 (*) ( id c)) = p1 & (p2 (*) ( id c)) = p2 by A1, CAT_1: 22;

      

      hence ( id c) = i by A4, A5

      .= h by A3, A4;

    end;

    theorem :: CAT_3:59

    for f be Morphism of d, c st c is_a_product_wrt (p1,p2) & ( dom f) = d & ( cod f) = c & f is invertible holds d is_a_product_wrt ((p1 (*) f),(p2 (*) f))

    proof

      let f be Morphism of d, c such that

       A1: c is_a_product_wrt (p1,p2) and

       A2: ( dom f) = d & ( cod f) = c & f is invertible;

      c is_a_product_wrt (( 0 , { 0 }) --> (p1,p2)) by A1, Th54;

      then d is_a_product_wrt ((( 0 , { 0 }) --> (p1,p2)) * f) by A2, Th51;

      then d is_a_product_wrt (( 0 , { 0 }) --> ((p1 (*) f),(p2 (*) f))) by Th14;

      hence thesis by Th54;

    end;

    theorem :: CAT_3:60

    c is_a_product_wrt (p1,p2) & ( cod p2) is terminal implies (c,( cod p1)) are_isomorphic

    proof

      set a = ( cod p1), b = ( cod p2);

      assume that

       A1: c is_a_product_wrt (p1,p2) and

       A2: b is terminal;

      set f = ( id a), g = ( term (a,b));

      ( dom g) = a & ( cod g) = b by A2, Th35;

      then f in ( Hom (a,a)) & g in ( Hom (a,b)) by CAT_1: 27;

      then

      consider h such that

       A3: h in ( Hom (a,c)) and

       A4: for k st k in ( Hom (a,c)) holds (p1 (*) k) = f & (p2 (*) k) = g iff h = k by A1;

      

       A5: ( dom h) = a by A3, CAT_1: 1;

      reconsider h as Morphism of a, c by A3, CAT_1:def 5;

      

       A6: ( dom p1) = c by A1;

      then

      reconsider p = p1 as Morphism of c, a by CAT_1: 4;

      

       A7: ( cod h) = c by A3, CAT_1: 1;

      then

       A8: ( cod (h (*) p)) = c by A5, CAT_1: 17;

      

       A9: ( dom p2) = c by A1;

      then

       A10: ( cod (p2 (*) (h (*) p))) = b by A8, CAT_1: 17;

      

       A11: ( dom (h (*) p)) = c by A6, A5, CAT_1: 17;

      then

       A12: (h (*) p) in ( Hom (c,c)) by A8;

      ( dom (p2 (*) (h (*) p))) = c by A9, A11, A8, CAT_1: 17;

      

      then

       A13: (p2 (*) (h (*) p)) = ( term (c,b)) by A2, A10, Th36

      .= p2 by A2, A9, Th36;

      

       A14: ( Hom (c,a)) <> {} by A6, CAT_1: 2;

      take p;

      thus ( Hom (c,a)) <> {} & ( Hom (a,c)) <> {} by A3, A6, CAT_1: 2;

      take h;

      

      thus (p * h) = (p (*) h) by A3, A14, CAT_1:def 13

      .= ( id a) by A3, A4;

      (p1 (*) (h (*) p)) = ((p1 (*) h) (*) p) by A6, A5, A7, CAT_1: 18

      .= (( id ( cod p)) (*) p) by A3, A4

      .= p by CAT_1: 21;

      

      hence ( id c) = (h (*) p) by A1, A13, A12, Th58

      .= (h * p) by A3, A14, CAT_1:def 13;

    end;

    theorem :: CAT_3:61

    c is_a_product_wrt (p1,p2) & ( cod p1) is terminal implies (c,( cod p2)) are_isomorphic

    proof

      set a = ( cod p1), b = ( cod p2);

      assume that

       A1: c is_a_product_wrt (p1,p2) and

       A2: a is terminal;

      set f = ( id b), g = ( term (b,a));

      ( dom g) = b & ( cod g) = a by A2, Th35;

      then f in ( Hom (b,b)) & g in ( Hom (b,a)) by CAT_1: 27;

      then

      consider h such that

       A3: h in ( Hom (b,c)) and

       A4: for k st k in ( Hom (b,c)) holds (p1 (*) k) = g & (p2 (*) k) = f iff h = k by A1;

      

       A5: ( dom h) = b by A3, CAT_1: 1;

      

       A6: ( dom p2) = c by A1;

      then

      reconsider p = p2 as Morphism of c, b by CAT_1: 4;

      

       A7: ( cod h) = c by A3, CAT_1: 1;

      then

       A8: ( cod (h (*) p)) = c by A5, CAT_1: 17;

      

       A9: ( dom p1) = c by A1;

      then

       A10: ( cod (p1 (*) (h (*) p))) = a by A8, CAT_1: 17;

      

       A11: ( dom (h (*) p)) = c by A6, A5, CAT_1: 17;

      then

       A12: (h (*) p) in ( Hom (c,c)) by A8;

      ( dom (p1 (*) (h (*) p))) = c by A9, A11, A8, CAT_1: 17;

      

      then

       A13: (p1 (*) (h (*) p)) = ( term (c,a)) by A2, A10, Th36

      .= p1 by A2, A9, Th36;

      

       A14: ( Hom (c,b)) <> {} by A6, CAT_1: 2;

      take p;

      thus ( Hom (c,b)) <> {} & ( Hom (b,c)) <> {} by A6, A3, CAT_1: 2;

      reconsider h as Morphism of b, c by A3, CAT_1:def 5;

      take h;

      

      thus (p * h) = (p (*) h) by A14, A3, CAT_1:def 13

      .= ( id b) by A3, A4;

      (p (*) h) = ( id ( cod p)) by A3, A4;

      

      then

       A15: (p2 (*) (h (*) p)) = (( id ( cod p)) (*) p) by A6, A5, A7, CAT_1: 18

      .= p by CAT_1: 21;

      

      thus ( id c) = (h (*) p) by A1, A13, A12, Th58, A15

      .= (h * p) by A14, A3, CAT_1:def 13;

    end;

    begin

    definition

      let C, c, I;

      :: CAT_3:def16

      mode Injections_family of c,I -> Function of I, the carrier' of C means

      : Def16: ( cods it ) = (I --> c);

      existence

      proof

        take F = (I --> ( id c));

        ( cods F) = (I --> ( cod ( id c))) by Th5;

        hence thesis;

      end;

    end

    theorem :: CAT_3:62

    

     Th62: for F be Injections_family of c, I st x in I holds ( cod (F /. x)) = c

    proof

      let F be Injections_family of c, I such that

       A1: x in I;

      (( cods F) /. x) = ((I --> c) /. x) by Def16;

      

      hence ( cod (F /. x)) = ((I --> c) /. x) by A1, Def2

      .= c by A1, Th2;

    end;

    theorem :: CAT_3:63

    for F be Function of {} , the carrier' of C holds F is Injections_family of a, {}

    proof

      let F be Function of {} , the carrier' of C;

      thus ( {} --> a) = ( cods F);

    end;

    theorem :: CAT_3:64

    

     Th64: ( cod f) = a implies (y .--> f) is Injections_family of a, {y}

    proof

      set F = (y .--> f);

      assume

       A1: ( cod f) = a;

      now

        let x;

        assume

         A2: x in {y};

        

        hence (( cods F) /. x) = ( cod (F /. x)) by Def2

        .= a by A1, A2, Th2

        .= ((y .--> a) /. x) by A2, Th2;

      end;

      hence ( cods F) = ( {y} --> a) by Th1;

    end;

    theorem :: CAT_3:65

    

     Th65: ( cod p1) = c & ( cod p2) = c implies ((x1,x2) --> (p1,p2)) is Injections_family of c, {x1, x2}

    proof

      assume

       A1: ( cod p1) = c & ( cod p2) = c;

      ( cods ((x1,x2) --> (p1,p2))) = ((x1,x2) --> (( cod p1),( cod p2))) by Th7

      .= ( {x1, x2} --> c) by A1, FUNCT_4: 65;

      hence thesis by Def16;

    end;

    theorem :: CAT_3:66

    

     Th66: for F be Injections_family of b, I st ( dom f) = b holds (f * F) is Injections_family of ( cod f), I

    proof

      let F be Injections_family of b, I;

      assume ( dom f) = b;

      then ( cods F) = (I --> ( dom f)) by Def16;

      hence ( cods (f * F)) = (I --> ( cod f)) by Th17;

    end;

    theorem :: CAT_3:67

    for F be Injections_family of b, I, G be Function of I, the carrier' of C st ( doms F) = ( cods G) holds (F "*" G) is Injections_family of b, I

    proof

      let F be Injections_family of b, I;

      let G be Function of I, the carrier' of C;

      assume ( doms F) = ( cods G);

      then ( cods (F "*" G)) = ( cods F) by Th18;

      hence ( cods (F "*" G)) = (I --> b) by Def16;

    end;

    theorem :: CAT_3:68

    

     Th68: for F be Function of I, the carrier' of C holds F is Projections_family of c, I iff (F opp ) is Injections_family of (c opp ), I

    proof

      let F be Function of I, the carrier' of C;

      thus F is Projections_family of c, I implies (F opp ) is Injections_family of (c opp ), I

      proof

        assume

         A1: ( doms F) = (I --> c);

        now

          let x;

          reconsider gg = (F /. x) as Morphism of ( dom (F /. x)), ( cod (F /. x)) by CAT_1: 4;

          

           A2: ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

          then

           A3: (gg opp ) = ((F /. x) opp ) by OPPCAT_1:def 6;

          assume

           A4: x in I;

          

          hence (( cods (F opp )) /. x) = ( cod ((F opp ) /. x)) by Def2

          .= ( cod ((F /. x) opp )) by A4, Def3

          .= (( dom (F /. x)) opp ) by A2, A3, OPPCAT_1: 12

          .= ((I --> (c opp )) /. x) by A1, A4, Def1;

        end;

        hence ( cods (F opp )) = (I --> (c opp )) by Th1;

      end;

      assume

       A5: ( cods (F opp )) = (I --> (c opp ));

      now

        let x;

        reconsider gg = (F /. x) as Morphism of ( dom (F /. x)), ( cod (F /. x)) by CAT_1: 4;

        

         A6: ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

        then

         A7: (gg opp ) = ((F /. x) opp ) by OPPCAT_1:def 6;

        assume

         A8: x in I;

        

        hence (( doms F) /. x) = ( dom (F /. x)) by Def1

        .= ( cod (gg opp )) by A6, OPPCAT_1: 10

        .= ( cod ((F opp ) /. x)) by A8, Def3, A7

        .= ((I --> c) /. x) by A8, A5, Def2;

      end;

      hence ( doms F) = (I --> c) by Th1;

    end;

    theorem :: CAT_3:69

    

     Th69: for F be Function of I, the carrier' of (C opp ), c be Object of (C opp ) holds F is Injections_family of c, I iff ( opp F) is Projections_family of ( opp c), I

    proof

      let F be Function of I, the carrier' of (C opp ), c be Object of (C opp );

      thus F is Injections_family of c, I implies ( opp F) is Projections_family of ( opp c), I

      proof

        assume

         A1: ( cods F) = (I --> c);

        now

          let x;

          reconsider gg = (F /. x) as Morphism of ( dom (F /. x)), ( cod (F /. x)) by CAT_1: 4;

          

           A2: ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

          assume

           A3: x in I;

          

          hence (( doms ( opp F)) /. x) = ( dom (( opp F) /. x)) by Def1

          .= ( dom ( opp (F /. x))) by A3, Def4

          .= ( opp ( cod (F /. x))) by A2, OPPCAT_1: 13

          .= ((I --> ( opp c)) /. x) by A1, A3, Def2;

        end;

        hence ( doms ( opp F)) = (I --> ( opp c)) by Th1;

      end;

      assume

       A4: ( doms ( opp F)) = (I --> ( opp c));

      now

        let x;

        reconsider gg = (F /. x) as Morphism of ( dom (F /. x)), ( cod (F /. x)) by CAT_1: 4;

        ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

        then

         A5: (gg opp ) = ((F /. x) opp ) by OPPCAT_1:def 6;

        assume

         A6: x in I;

        

        hence (( cods F) /. x) = ( cod (F /. x)) by Def2

        .= ( dom ( opp (F /. x))) by A5, OPPCAT_1: 11

        .= ( dom (( opp F) /. x)) by A6, Def4

        .= ((I --> c) /. x) by A4, A6, Def1;

      end;

      hence ( cods F) = (I --> c) by Th1;

    end;

    theorem :: CAT_3:70

    for F be Injections_family of ( dom f), I holds ((F opp ) * (f opp )) = ((f * F) opp )

    proof

      let F be Injections_family of ( dom f), I;

      now

        let x;

        assume

         A1: x in I;

        

        then

         A2: ( cod (F /. x)) = (( cods F) /. x) by Def2

        .= ((I --> ( dom f)) /. x) by Def16

        .= ( dom f) by A1, Th2;

        reconsider ff = f as Morphism of ( dom f), ( cod f) by CAT_1: 4;

        reconsider gg = (F /. x) as Morphism of ( dom (F /. x)), ( dom f) by A2, CAT_1: 4;

        

         A3: ( Hom (( dom f),( cod f))) <> {} & ( Hom (( dom (F /. x)),( cod (F /. x)))) <> {} by CAT_1: 2;

        then

         A4: (ff opp ) = (f opp ) by OPPCAT_1:def 6;

        

         A5: (gg opp ) = ((F /. x) opp ) by A3, A2, OPPCAT_1:def 6;

        

        thus (((F opp ) * (f opp )) /. x) = (((F opp ) /. x) (*) (f opp )) by A1, Def5

        .= (((F /. x) opp ) (*) (f opp )) by A1, Def3

        .= ((f (*) (F /. x)) opp ) by A2, A4, A5, A3, OPPCAT_1: 16

        .= (((f * F) /. x) opp ) by A1, Def6

        .= (((f * F) opp ) /. x) by A1, Def3;

      end;

      hence thesis by Th1;

    end;

    definition

      let C, c, I;

      let F be Function of I, the carrier' of C;

      :: CAT_3:def17

      pred c is_a_coproduct_wrt F means F is Injections_family of c, I & for d holds for F9 be Injections_family of d, I st ( doms F) = ( doms F9) holds ex h st h in ( Hom (c,d)) & for k st k in ( Hom (c,d)) holds (for x st x in I holds (k (*) (F /. x)) = (F9 /. x)) iff h = k;

    end

    theorem :: CAT_3:71

    for F be Function of I, the carrier' of C holds c is_a_product_wrt F iff (c opp ) is_a_coproduct_wrt (F opp )

    proof

      let F be Function of I, the carrier' of C;

      thus c is_a_product_wrt F implies (c opp ) is_a_coproduct_wrt (F opp )

      proof

        assume

         A1: c is_a_product_wrt F;

        then F is Projections_family of c, I;

        hence (F opp ) is Injections_family of (c opp ), I by Th68;

        let d be Object of (C opp ), F9 be Injections_family of d, I such that

         A2: ( doms (F opp )) = ( doms F9);

        reconsider oppF9 = ( opp F9) as Projections_family of ( opp d), I by Th69;

        now

          let x;

          reconsider gg = (F /. x) as Morphism of ( dom (F /. x)), ( cod (F /. x)) by CAT_1: 4;

          

           A3: ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

          then

           A4: (gg opp ) = ((F /. x) opp ) by OPPCAT_1:def 6;

          reconsider g9 = (F9 /. x) as Morphism of ( dom (F9 /. x)), ( cod (F9 /. x)) by CAT_1: 4;

          ( Hom (( dom g9),( cod g9))) <> {} by CAT_1: 2;

          then

           A5: (g9 opp ) = ((F9 /. x) opp ) by OPPCAT_1:def 6;

          assume

           A6: x in I;

          

          hence (( cods F) /. x) = ( cod (F /. x)) by Def2

          .= ( dom (gg opp )) by A3, OPPCAT_1: 10

          .= ( dom ((F opp ) /. x)) by A6, Def3, A4

          .= (( doms F9) /. x) by A2, A6, Def1

          .= ( dom (F9 /. x)) by A6, Def1

          .= ( cod ( opp (F9 /. x))) by A5, OPPCAT_1: 11

          .= ( cod (oppF9 /. x)) by A6, Def4

          .= (( cods oppF9) /. x) by A6, Def2;

        end;

        then

        consider h such that

         A7: h in ( Hom (( opp d),c)) and

         A8: for k st k in ( Hom (( opp d),c)) holds (for x st x in I holds ((F /. x) (*) k) = (oppF9 /. x)) iff h = k by A1, Th1;

        take (h opp );

        h in ( Hom ((c opp ),(( opp d) opp ))) by A7, OPPCAT_1: 5;

        hence (h opp ) in ( Hom ((c opp ),d));

        let k be Morphism of (C opp );

        assume

         A9: k in ( Hom ((c opp ),d));

        then

         A10: ( opp k) in ( Hom (( opp d),( opp (c opp )))) by OPPCAT_1: 6;

        thus (for x st x in I holds (k (*) ((F opp ) /. x)) = (F9 /. x)) implies (h opp ) = k

        proof

          assume

           A11: for x st x in I holds (k (*) ((F opp ) /. x)) = (F9 /. x);

          now

            let x such that

             A12: x in I;

            reconsider gg = (F /. x) as Morphism of ( dom (F /. x)), ( cod (F /. x)) by CAT_1: 4;

            

             A13: ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

            then

             A14: (gg opp ) = ((F /. x) opp ) by OPPCAT_1:def 6;

            F is Projections_family of c, I by A1;

            then ( dom (F /. x)) = c by A12, Th41;

            then ( cod ((F /. x) opp )) = (c opp ) by A13, A14, OPPCAT_1: 12;

            then ( cod ((F opp ) /. x)) = (c opp ) by A12, Def3;

            then

             A15: ( dom k) = ( cod ((F opp ) /. x)) by A9, CAT_1: 1;

            ( opp (k (*) ((F opp ) /. x))) = ( opp (F9 /. x)) by A11, A12;

            

            hence (oppF9 /. x) = ( opp (k (*) ((F opp ) /. x))) by A12, Def4

            .= (( opp ((F opp ) /. x)) (*) ( opp k)) by A15, OPPCAT_1: 18

            .= (( opp ((F /. x) opp )) (*) ( opp k)) by A12, Def3

            .= ((F /. x) (*) ( opp k));

          end;

          hence thesis by A8, A10;

        end;

        assume

         A16: (h opp ) = k;

        let x such that

         A17: x in I;

        F is Projections_family of c, I by A1;

        then ( dom (F /. x)) = c by A17, Th41;

        then

         A18: ( cod ( opp k)) = ( dom (F /. x)) by A10, CAT_1: 1;

        reconsider ff = ( opp k) as Morphism of ( dom ( opp k)), ( cod ( opp k)) by CAT_1: 4;

        reconsider gg = (F /. x) as Morphism of ( cod ( opp k)), ( cod (F /. x)) by A18, CAT_1: 4;

        

         A19: ( Hom (( dom ( opp k)),( cod ( opp k)))) <> {} & ( Hom (( dom (F /. x)),( cod (F /. x)))) <> {} by CAT_1: 2;

        then

         A20: (ff opp ) = (( opp k) opp ) by OPPCAT_1:def 6;

        

         A21: (gg opp ) = ((F /. x) opp ) by A19, A18, OPPCAT_1:def 6;

        ((F /. x) (*) ( opp k)) = (oppF9 /. x) by A8, A10, A17, A16;

        then ((( opp k) opp ) (*) ((F /. x) opp )) = ((oppF9 /. x) opp ) by A18, A20, A21, A19, OPPCAT_1: 16;

        

        hence (k (*) ((F opp ) /. x)) = ((oppF9 /. x) opp ) by A17, Def3

        .= (( opp (F9 /. x)) opp ) by A17, Def4

        .= (F9 /. x);

      end;

      assume

       A22: (c opp ) is_a_coproduct_wrt (F opp );

      then (F opp ) is Injections_family of (c opp ), I;

      hence F is Projections_family of c, I by Th68;

      let d;

      let F9 be Projections_family of d, I such that

       A23: ( cods F) = ( cods F9);

       A24:

      now

        let x;

        reconsider gg = (F /. x) as Morphism of ( dom (F /. x)), ( cod (F /. x)) by CAT_1: 4;

        

         A25: ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

        then

         A26: (gg opp ) = ((F /. x) opp ) by OPPCAT_1:def 6;

        reconsider g9 = (F9 /. x) as Morphism of ( dom (F9 /. x)), ( cod (F9 /. x)) by CAT_1: 4;

        

         A27: ( Hom (( dom g9),( cod g9))) <> {} by CAT_1: 2;

        then

         A28: (g9 opp ) = ((F9 /. x) opp ) by OPPCAT_1:def 6;

        assume

         A29: x in I;

        

        hence (( doms (F opp )) /. x) = ( dom ((F opp ) /. x)) by Def1

        .= ( dom (gg opp )) by A29, Def3, A26

        .= ( cod (F /. x)) by A25, OPPCAT_1: 10

        .= (( cods F9) /. x) by A23, A29, Def2

        .= ( cod (F9 /. x)) by A29, Def2

        .= ( dom (g9 opp )) by A27, OPPCAT_1: 10

        .= ( dom ((F9 opp ) /. x)) by A29, Def3, A28

        .= (( doms (F9 opp )) /. x) by A29, Def1;

      end;

      reconsider F9opp = (F9 opp ) as Injections_family of (d opp ), I by Th68;

      consider h be Morphism of (C opp ) such that

       A30: h in ( Hom ((c opp ),(d opp ))) and

       A31: for k be Morphism of (C opp ) st k in ( Hom ((c opp ),(d opp ))) holds (for x st x in I holds (k (*) ((F opp ) /. x)) = (F9opp /. x)) iff h = k by A22, A24, Th1;

      take ( opp h);

      ( opp h) in ( Hom (( opp (d opp )),( opp (c opp )))) by A30, OPPCAT_1: 6;

      hence ( opp h) in ( Hom (d,c));

      let k;

      assume

       A32: k in ( Hom (d,c));

      then

       A33: (k opp ) in ( Hom ((c opp ),(d opp ))) by OPPCAT_1: 5;

      thus (for x st x in I holds ((F /. x) (*) k) = (F9 /. x)) implies ( opp h) = k

      proof

        assume

         A34: for x st x in I holds ((F /. x) (*) k) = (F9 /. x);

        now

          let x such that

           A35: x in I;

          reconsider gg = (F /. x) as Morphism of ( dom (F /. x)), ( cod (F /. x)) by CAT_1: 4;

          

           A36: ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

          then

           A37: (gg opp ) = ((F /. x) opp ) by OPPCAT_1:def 6;

          (F opp ) is Injections_family of (c opp ), I by A22;

          then ( cod ((F opp ) /. x)) = (c opp ) by A35, Th62;

          then ( cod (gg opp )) = (c opp ) by A35, Def3, A37;

          then ( dom (F /. x)) = c by A36, OPPCAT_1: 10;

          then

           A38: ( cod k) = ( dom (F /. x)) by A32, CAT_1: 1;

          reconsider ff = k as Morphism of ( dom k), ( cod k) by CAT_1: 4;

          reconsider gg = (F /. x) as Morphism of ( cod k), ( cod (F /. x)) by A38, CAT_1: 4;

          

           A39: ( Hom (( dom k),( cod k))) <> {} & ( Hom (( dom (F /. x)),( cod (F /. x)))) <> {} by CAT_1: 2;

          then

           A40: (ff opp ) = (k opp ) by OPPCAT_1:def 6;

          

           A41: (gg opp ) = ((F /. x) opp ) by A39, A38, OPPCAT_1:def 6;

          ((F /. x) (*) k) = (F9 /. x) by A34, A35;

          then ((k opp ) (*) ((F /. x) opp )) = ((F9 /. x) opp ) by A38, A40, A41, A39, OPPCAT_1: 16;

          

          hence (F9opp /. x) = ((k opp ) (*) ((F /. x) opp )) by A35, Def3

          .= ((k opp ) (*) ((F opp ) /. x)) by A35, Def3;

        end;

        hence thesis by A31, A33;

      end;

      assume

       A42: ( opp h) = k;

      let x such that

       A43: x in I;

      reconsider gg = (F /. x) as Morphism of ( dom (F /. x)), ( cod (F /. x)) by CAT_1: 4;

      

       A44: ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

      then

       A45: (gg opp ) = ((F /. x) opp ) by OPPCAT_1:def 6;

      (F opp ) is Injections_family of (c opp ), I by A22;

      then ( cod ((F opp ) /. x)) = (c opp ) by A43, Th62;

      then ( cod (gg opp )) = (c opp ) by A43, Def3, A45;

      then ( dom (F /. x)) = c by A44, OPPCAT_1: 10;

      then

       A46: ( cod k) = ( dom (F /. x)) by A32, CAT_1: 1;

      reconsider ff = k as Morphism of ( dom k), ( cod k) by CAT_1: 4;

      reconsider gg = (F /. x) as Morphism of ( cod k), ( cod (F /. x)) by A46, CAT_1: 4;

      

       A47: ( Hom (( dom k),( cod k))) <> {} & ( Hom (( dom (F /. x)),( cod (F /. x)))) <> {} by CAT_1: 2;

      then

       A48: (ff opp ) = (k opp ) by OPPCAT_1:def 6;

      

       A49: (gg opp ) = ((F /. x) opp ) by A47, A46, OPPCAT_1:def 6;

      ((k opp ) (*) ((F opp ) /. x)) = (F9opp /. x) by A31, A33, A43, A42;

      then ((k opp ) (*) ((F opp ) /. x)) = ((F9 /. x) opp ) by A43, Def3;

      

      hence (F9 /. x) = ((k opp ) (*) ((F /. x) opp )) by A43, Def3

      .= (((F /. x) (*) k) opp ) by A46, A48, A49, A47, OPPCAT_1: 16

      .= ((F /. x) (*) k);

    end;

    theorem :: CAT_3:72

    

     Th72: for F be Injections_family of c, I, F9 be Injections_family of d, I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & ( doms F) = ( doms F9) holds (c,d) are_isomorphic

    proof

      let F be Injections_family of c, I, F9 be Injections_family of d, I such that

       A1: c is_a_coproduct_wrt F and

       A2: d is_a_coproduct_wrt F9 and

       A3: ( doms F) = ( doms F9);

      consider fg be Morphism of C such that fg in ( Hom (d,d)) and

       A4: for k st k in ( Hom (d,d)) holds (for x st x in I holds (k (*) (F9 /. x)) = (F9 /. x)) iff fg = k by A2;

      consider f such that

       A5: f in ( Hom (c,d)) and

       A6: for k st k in ( Hom (c,d)) holds (for x st x in I holds (k (*) (F /. x)) = (F9 /. x)) iff f = k by A1, A3;

      reconsider f as Morphism of c, d by A5, CAT_1:def 5;

      

       A7: ( dom f) = c by A5, CAT_1: 1;

       A8:

      now

        set k = ( id c);

        thus k in ( Hom (c,c)) by CAT_1: 27;

        let x;

        assume x in I;

        then ( cod (F /. x)) = c by Th62;

        hence (k (*) (F /. x)) = (F /. x) by CAT_1: 21;

      end;

       A9:

      now

        set k = ( id d);

        thus k in ( Hom (d,d)) by CAT_1: 27;

        let x;

        assume x in I;

        then ( cod (F9 /. x)) = d by Th62;

        hence (k (*) (F9 /. x)) = (F9 /. x) by CAT_1: 21;

      end;

      consider gf be Morphism of C such that gf in ( Hom (c,c)) and

       A10: for k st k in ( Hom (c,c)) holds (for x st x in I holds (k (*) (F /. x)) = (F /. x)) iff gf = k by A1;

      consider g such that

       A11: g in ( Hom (d,c)) and

       A12: for k st k in ( Hom (d,c)) holds (for x st x in I holds (k (*) (F9 /. x)) = (F /. x)) iff g = k by A2, A3;

      reconsider g as Morphism of d, c by A11, CAT_1:def 5;

      take f;

      thus ( Hom (c,d)) <> {} & ( Hom (d,c)) <> {} by A11, A5;

      take g;

      

       A13: ( cod f) = d by A5, CAT_1: 1;

      

       A14: ( dom g) = d by A11, CAT_1: 1;

      

       A15: ( cod g) = c by A11, CAT_1: 1;

       A16:

      now

        ( cod (f (*) g)) = d & ( dom (f (*) g)) = d by A13, A14, A7, A15, CAT_1: 17;

        hence (f (*) g) in ( Hom (d,d));

        let x;

        assume

         A17: x in I;

        then ( cod (F9 /. x)) = d by Th62;

        

        hence ((f (*) g) (*) (F9 /. x)) = (f (*) (g (*) (F9 /. x))) by A14, A7, A15, CAT_1: 18

        .= (f (*) (F /. x)) by A11, A12, A17

        .= (F9 /. x) by A5, A6, A17;

      end;

      

      thus (f * g) = (f (*) g) by A11, A5, CAT_1:def 13

      .= fg by A4, A16

      .= ( id d) by A4, A9;

       A18:

      now

        ( cod (g (*) f)) = c & ( dom (g (*) f)) = c by A13, A14, A7, A15, CAT_1: 17;

        hence (g (*) f) in ( Hom (c,c));

        let x;

        assume

         A19: x in I;

        then ( cod (F /. x)) = c by Th62;

        

        hence ((g (*) f) (*) (F /. x)) = (g (*) (f (*) (F /. x))) by A13, A14, A7, CAT_1: 18

        .= (g (*) (F9 /. x)) by A5, A6, A19

        .= (F /. x) by A11, A12, A19;

      end;

      

      thus (g * f) = (g (*) f) by A11, A5, CAT_1:def 13

      .= gf by A10, A18

      .= ( id c) by A8, A10;

    end;

    theorem :: CAT_3:73

    

     Th73: for F be Injections_family of c, I st c is_a_coproduct_wrt F & for x1, x2 st x1 in I & x2 in I holds ( Hom (( dom (F /. x1)),( dom (F /. x2)))) <> {} holds for x st x in I holds for d be Object of C st d = ( dom (F /. x)) & ( Hom (d,c)) <> {} holds for f be Morphism of d, c st f = (F /. x) holds f is coretraction

    proof

      let F be Injections_family of c, I such that

       A1: c is_a_coproduct_wrt F and

       A2: for x1, x2 st x1 in I & x2 in I holds ( Hom (( dom (F /. x1)),( dom (F /. x2)))) <> {} ;

      let x such that

       A3: x in I;

      let d be Object of C such that

       A4: d = ( dom (F /. x)) and

       A5: ( Hom (d,c)) <> {} ;

      let f be Morphism of d, c such that

       A6: f = (F /. x);

      defpred P[ object, object] means ($1 = x implies $2 = ( id d)) & ($1 <> x implies $2 in ( Hom (( dom (F /. $1)),d)));

      

       A7: for y be object st y in I holds ex z be object st z in the carrier' of C & P[y, z]

      proof

        let y be object;

        set z = the Element of ( Hom (( dom (F /. y)),d));

        assume y in I;

        then

         A8: ( Hom (( dom (F /. y)),d)) <> {} by A2, A3, A4;

        then

         A9: z in ( Hom (( dom (F /. y)),d));

        per cases ;

          suppose

           A10: y = x;

          take z = ( id d);

          thus z in the carrier' of C;

          thus thesis by A10;

        end;

          suppose

           A11: y <> x;

          take z;

          thus z in the carrier' of C by A9;

          thus thesis by A8, A11;

        end;

      end;

      consider F9 be Function such that

       A12: ( dom F9) = I & ( rng F9) c= the carrier' of C and

       A13: for y be object st y in I holds P[y, (F9 . y)] from FUNCT_1:sch 6( A7);

      reconsider F9 as Function of I, the carrier' of C by A12, FUNCT_2:def 1, RELSET_1: 4;

      now

        let y;

        assume

         A14: y in I;

        then

         A15: (F9 . y) = (F9 /. y) by FUNCT_2:def 13;

        then

         A16: y <> x implies (F9 /. y) in ( Hom (( dom (F /. y)),d)) by A13, A14;

        y = x implies (F9 /. y) = ( id d) by A13, A14, A15;

        then ( cod (F9 /. y)) = d by A16, CAT_1: 1;

        

        hence (( cods F9) /. y) = d by A14, Def2

        .= ((I --> d) /. y) by A14, Th2;

      end;

      then

       A17: F9 is Injections_family of d, I by Def16, Th1;

      now

        let y;

        assume

         A18: y in I;

        then

         A19: (F9 . y) = (F9 /. y) by FUNCT_2:def 13;

        then

         A20: y <> x implies (F9 /. y) in ( Hom (( dom (F /. y)),d)) by A13, A18;

        y = x implies (F9 /. y) = ( id d) by A13, A18, A19;

        then ( dom (F9 /. y)) = ( dom (F /. y)) by A20, A4, CAT_1: 1;

        

        hence (( doms F9) /. y) = ( dom (F /. y)) by A18, Def1

        .= (( doms F) /. y) by A18, Def1;

      end;

      then

      consider i such that

       A21: i in ( Hom (c,d)) and

       A22: for k st k in ( Hom (c,d)) holds (for y st y in I holds (k (*) (F /. y)) = (F9 /. y)) iff i = k by A1, A17, Th1;

      thus ( Hom (d,c)) <> {} & ( Hom (c,d)) <> {} by A21, A5;

      reconsider i as Morphism of c, d by A21, CAT_1:def 5;

      take i;

      

      thus (i * f) = (i (*) (F /. x)) by A6, A21, A5, CAT_1:def 13

      .= (F9 /. x) by A3, A21, A22

      .= (F9 . x) by A3, FUNCT_2:def 13

      .= ( id d) by A3, A13;

    end;

    theorem :: CAT_3:74

    

     Th74: for f be Morphism of a, b holds for F be Injections_family of a, I st a is_a_coproduct_wrt F & ( dom f) = a & ( cod f) = b & f is invertible holds b is_a_coproduct_wrt (f * F)

    proof

      let f be Morphism of a, b;

      let F be Injections_family of a, I such that

       A1: a is_a_coproduct_wrt F and

       A2: ( dom f) = a and

       A3: ( cod f) = b and

       A4: f is invertible;

      thus (f * F) is Injections_family of b, I by A2, A3, Th66;

      let c;

      

       A5: ( cods F) = (I --> ( dom f)) by A2, Def16;

      let F9 be Injections_family of c, I;

      assume ( doms (f * F)) = ( doms F9);

      then ( doms F) = ( doms F9) by A5, Th17;

      then

      consider h such that

       A6: h in ( Hom (a,c)) and

       A7: for k st k in ( Hom (a,c)) holds (for x st x in I holds (k (*) (F /. x)) = (F9 /. x)) iff h = k by A1;

      

       A8: ( dom h) = a by A6, CAT_1: 1;

      consider g be Morphism of b, a such that

       A9: (f * g) = ( id b) and

       A10: (g * f) = ( id a) by A4;

      

       A11: ( Hom (b,a)) <> {} & ( Hom (a,b)) <> {} by A4;

      then

       A12: ( dom g) = ( cod f) by A3, CAT_1: 5;

      

       A13: ( cod g) = ( dom f) by A2, A11, CAT_1: 5;

      

       A14: (f * g) = (f (*) g) by A11, CAT_1:def 13;

      

       A15: (g * f) = (g (*) f) by A11, CAT_1:def 13;

      ( cod h) = c by A6, CAT_1: 1;

      then

       A16: ( cod (h (*) g)) = c by A2, A13, A8, CAT_1: 17;

      take hg = (h (*) g);

      ( dom (h (*) g)) = b by A2, A3, A12, A13, A8, CAT_1: 17;

      hence hg in ( Hom (b,c)) by A16;

      let k;

      assume

       A17: k in ( Hom (b,c));

      then

       A18: ( dom k) = b by CAT_1: 1;

      

       A19: ( cod k) = c by A17, CAT_1: 1;

      thus (for x st x in I holds (k (*) ((f * F) /. x)) = (F9 /. x)) implies hg = k

      proof

        assume

         A20: for x st x in I holds (k (*) ((f * F) /. x)) = (F9 /. x);

        now

          ( cod (k (*) f)) = c & ( dom (k (*) f)) = a by A2, A3, A19, A18, CAT_1: 17;

          hence (k (*) f) in ( Hom (a,c));

          let x;

          assume

           A21: x in I;

          then ( cod (F /. x)) = a by Th62;

          

          hence ((k (*) f) (*) (F /. x)) = (k (*) (f (*) (F /. x))) by A2, A3, A18, CAT_1: 18

          .= (k (*) ((f * F) /. x)) by A21, Def6

          .= (F9 /. x) by A20, A21;

        end;

        then ((k (*) f) (*) g) = (h (*) g) by A7;

        

        hence hg = (k (*) ( id b)) by A3, A13, A9, A18, A14, CAT_1: 18

        .= k by A18, CAT_1: 22;

      end;

      assume

       A22: hg = k;

      let x;

      assume

       A23: x in I;

      then

       A24: ( cod (F /. x)) = a by Th62;

      then

       A25: ( cod (f (*) (F /. x))) = b by A2, A3, CAT_1: 17;

      

      thus (k (*) ((f * F) /. x)) = (k (*) (f (*) (F /. x))) by A23, Def6

      .= (h (*) (g (*) (f (*) (F /. x)))) by A2, A3, A12, A13, A8, A22, A25, CAT_1: 18

      .= (h (*) (( id ( dom f)) (*) (F /. x))) by A2, A12, A10, A24, A15, CAT_1: 18

      .= (h (*) (F /. x)) by A2, A24, CAT_1: 21

      .= (F9 /. x) by A6, A7, A23;

    end;

    theorem :: CAT_3:75

    

     Th75: for F be Injections_family of a, {} holds a is_a_coproduct_wrt F iff a is initial

    proof

      let F be Injections_family of a, {} ;

      thus a is_a_coproduct_wrt F implies a is initial

      proof

        assume

         A1: a is_a_coproduct_wrt F;

        let b;

        set F9 = the Injections_family of b, {} ;

        consider h such that

         A2: h in ( Hom (a,b)) and

         A3: for k st k in ( Hom (a,b)) holds (for x st x in {} holds (k (*) (F /. x)) = (F9 /. x)) iff h = k by A1;

        thus ( Hom (a,b)) <> {} by A2;

        reconsider f = h as Morphism of a, b by A2, CAT_1:def 5;

        take f;

        let g be Morphism of a, b;

        

         A4: for x st x in {} holds (g (*) (F /. x)) = (F9 /. x);

        g in ( Hom (a,b)) by A2, CAT_1:def 5;

        hence thesis by A3, A4;

      end;

      assume

       A5: a is initial;

      thus F is Injections_family of a, {} ;

      let b;

      consider h be Morphism of a, b such that

       A6: for g be Morphism of a, b holds h = g by A5;

      let F9 be Injections_family of b, {} such that ( doms F) = ( doms F9);

      take h;

      ( Hom (a,b)) <> {} by A5;

      hence h in ( Hom (a,b)) by CAT_1:def 5;

      let k;

      assume k in ( Hom (a,b));

      then k is Morphism of a, b by CAT_1:def 5;

      hence thesis by A6;

    end;

    theorem :: CAT_3:76

    a is_a_coproduct_wrt (y .--> ( id a))

    proof

      set F = (y .--> ( id a));

      ( cod ( id a)) = a;

      hence F is Injections_family of a, {y} by Th64;

      let b;

      let F9 be Injections_family of b, {y} such that

       A1: ( doms F) = ( doms F9);

      take h = (F9 /. y);

      

       A2: y in {y} by TARSKI:def 1;

      then

       A3: ( cod h) = b by Th62;

      ( dom h) = (( doms F) /. y) by A1, A2, Def1

      .= ( dom (F /. y)) by A2, Def1

      .= ( dom ( id a)) by A2, Th2

      .= a;

      hence h in ( Hom (a,b)) by A3;

      let k;

      assume k in ( Hom (a,b));

      then

       A4: ( dom k) = a by CAT_1: 1;

      thus (for x st x in {y} holds (k (*) (F /. x)) = (F9 /. x)) implies h = k

      proof

        assume

         A5: for x st x in {y} holds (k (*) (F /. x)) = (F9 /. x);

        

        thus k = (k (*) ( id a)) by A4, CAT_1: 22

        .= (k (*) (F /. y)) by A2, Th2

        .= h by A2, A5;

      end;

      assume

       A6: h = k;

      let x;

      assume

       A7: x in {y};

      

      hence (F9 /. x) = k by A6, TARSKI:def 1

      .= (k (*) ( id a)) by A4, CAT_1: 22

      .= (k (*) (F /. x)) by A7, Th2;

    end;

    theorem :: CAT_3:77

    for F be Injections_family of a, I st a is_a_coproduct_wrt F & for x st x in I holds ( dom (F /. x)) is initial holds a is initial

    proof

      let F be Injections_family of a, I such that

       A1: a is_a_coproduct_wrt F and

       A2: for x st x in I holds ( dom (F /. x)) is initial;

      now

        thus I = {} implies a is initial by A1, Th75;

        let b;

        deffunc f( set) = ( init (( dom (F /. $1)),b));

        consider F9 be Function of I, the carrier' of C such that

         A3: for x st x in I holds (F9 /. x) = f(x) from LambdaIdx;

        now

          let x;

          assume

           A4: x in I;

          then

           A5: ( dom (F /. x)) is initial by A2;

          

          thus (( cods F9) /. x) = ( cod (F9 /. x)) by A4, Def2

          .= ( cod ( init (( dom (F /. x)),b))) by A3, A4

          .= b by A5, Th38

          .= ((I --> b) /. x) by A4, Th2;

        end;

        then

        reconsider F9 as Injections_family of b, I by Def16, Th1;

        now

          let x;

          assume

           A6: x in I;

          then

           A7: ( dom (F /. x)) is initial by A2;

          

          thus (( doms F) /. x) = ( dom (F /. x)) by A6, Def1

          .= ( dom ( init (( dom (F /. x)),b))) by A7, Th38

          .= ( dom (F9 /. x)) by A3, A6

          .= (( doms F9) /. x) by A6, Def1;

        end;

        then

        consider h such that

         A8: h in ( Hom (a,b)) and

         A9: for k st k in ( Hom (a,b)) holds (for x st x in I holds (k (*) (F /. x)) = (F9 /. x)) iff h = k by A1, Th1;

        thus ( Hom (a,b)) <> {} by A8;

        reconsider h as Morphism of a, b by A8, CAT_1:def 5;

        take h;

        let g be Morphism of a, b;

        now

          thus g in ( Hom (a,b)) by A8, CAT_1:def 5;

          let x;

          set c = ( dom (F /. x));

          

           A10: ( dom g) = a by A8, CAT_1: 5;

          assume

           A11: x in I;

          then c is initial by A2;

          then

          consider f be Morphism of c, b such that

           A12: for f9 be Morphism of c, b holds f = f9;

          

           A13: ( cod (F /. x)) = a by A11, Th62;

          then

           A14: ( dom (g (*) (F /. x))) = c by A10, CAT_1: 17;

          ( cod g) = b by A8, CAT_1: 5;

          then ( cod (g (*) (F /. x))) = b by A10, A13, CAT_1: 17;

          then (g (*) (F /. x)) in ( Hom (c,b)) by A14;

          then

           A15: (g (*) (F /. x)) is Morphism of c, b by CAT_1:def 5;

          (F9 /. x) = ( init (c,b)) by A3, A11;

          

          hence (F9 /. x) = f by A12

          .= (g (*) (F /. x)) by A12, A15;

        end;

        hence h = g by A9;

      end;

      hence thesis;

    end;

    definition

      let C, c, i1, i2;

      :: CAT_3:def18

      pred c is_a_coproduct_wrt i1,i2 means ( cod i1) = c & ( cod i2) = c & for d, f, g st f in ( Hom (( dom i1),d)) & g in ( Hom (( dom i2),d)) holds ex h st h in ( Hom (c,d)) & for k st k in ( Hom (c,d)) holds (k (*) i1) = f & (k (*) i2) = g iff h = k;

    end

    theorem :: CAT_3:78

    c is_a_product_wrt (p1,p2) iff (c opp ) is_a_coproduct_wrt ((p1 opp ),(p2 opp ))

    proof

      set i1 = (p1 opp ), i2 = (p2 opp );

      thus c is_a_product_wrt (p1,p2) implies (c opp ) is_a_coproduct_wrt ((p1 opp ),(p2 opp ))

      proof

        assume that

         A1: ( dom p1) = c & ( dom p2) = c and

         A2: for d, f, g st f in ( Hom (d,( cod p1))) & g in ( Hom (d,( cod p2))) holds ex h st h in ( Hom (d,c)) & for k st k in ( Hom (d,c)) holds (p1 (*) k) = f & (p2 (*) k) = g iff h = k;

        reconsider gg = p1 as Morphism of ( dom p1), ( cod p1) by CAT_1: 4;

        

         A3: ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

        then

         A4: (gg opp ) = (p1 opp ) by OPPCAT_1:def 6;

        thus

         A5: ( cod i1) = (c opp ) by A1, A3, A4, OPPCAT_1: 10;

        reconsider gg = p2 as Morphism of ( dom p2), ( cod p2) by CAT_1: 4;

        

         A6: ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

        then

         A7: (gg opp ) = (p2 opp ) by OPPCAT_1:def 6;

        thus

         A8: ( cod i2) = (c opp ) by A1, A6, A7, OPPCAT_1: 10;

        let d be Object of (C opp ), f,g be Morphism of (C opp );

        assume that

         A9: f in ( Hom (( dom i1),d)) and

         A10: g in ( Hom (( dom i2),d));

        reconsider gg = i2 as Morphism of ( dom i2), ( cod i2) by CAT_1: 4;

        

         A11: ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

        ( opp g) in ( Hom (( opp d),( opp ( dom i2)))) by A10, OPPCAT_1: 6;

        then

         A12: ( opp g) in ( Hom (( opp d),( cod ( opp i2)))) by A11, OPPCAT_1: 13;

        reconsider gg = i1 as Morphism of ( dom i1), ( cod i1) by CAT_1: 4;

        

         A13: ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

        ( opp f) in ( Hom (( opp d),( opp ( dom i1)))) by A9, OPPCAT_1: 6;

        then ( opp f) in ( Hom (( opp d),( cod ( opp i1)))) by A13, OPPCAT_1: 13;

        then

        consider h such that

         A14: h in ( Hom (( opp d),c)) and

         A15: for k st k in ( Hom (( opp d),c)) holds (p1 (*) k) = ( opp f) & (p2 (*) k) = ( opp g) iff h = k by A2, A12;

        take (h opp );

        (h opp ) in ( Hom ((c opp ),(( opp d) opp ))) by A14, OPPCAT_1: 5;

        hence (h opp ) in ( Hom ((c opp ),d));

        let k be Morphism of (C opp );

        assume

         A16: k in ( Hom ((c opp ),d));

        then ( opp k) in ( Hom (( opp d),( opp (c opp )))) by OPPCAT_1: 6;

        then

         A17: (( opp i1) (*) ( opp k)) = f & (( opp i2) (*) ( opp k)) = g iff (h opp ) = k by A15;

        ( dom k) = (c opp ) by A16, CAT_1: 1;

        then ( opp (k (*) i1)) = f & ( opp (k (*) i2)) = g iff (h opp ) = k by A8, A5, A17, OPPCAT_1: 18;

        hence thesis;

      end;

      assume that

       A18: ( cod i1) = (c opp ) & ( cod i2) = (c opp ) and

       A19: for d be Object of (C opp ), f,g be Morphism of (C opp ) st f in ( Hom (( dom i1),d)) & g in ( Hom (( dom i2),d)) holds ex h be Morphism of (C opp ) st h in ( Hom ((c opp ),d)) & for k be Morphism of (C opp ) st k in ( Hom ((c opp ),d)) holds (k (*) i1) = f & (k (*) i2) = g iff h = k;

      reconsider gg = p1 as Morphism of ( dom p1), ( cod p1) by CAT_1: 4;

      

       A20: ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

      then

       A21: (gg opp ) = (p1 opp ) by OPPCAT_1:def 6;

      

       A22: ( dom p1) = (c opp ) by A18, A20, A21, OPPCAT_1: 10;

      reconsider gg = p2 as Morphism of ( dom p2), ( cod p2) by CAT_1: 4;

      

       A23: ( Hom (( dom gg),( cod gg))) <> {} by CAT_1: 2;

      then

       A24: (gg opp ) = (p2 opp ) by OPPCAT_1:def 6;

      

       A25: ( dom p2) = (c opp ) by A18, A23, A24, OPPCAT_1: 10;

      hence ( dom p1) = c & ( dom p2) = c by A22;

      let d, f, g;

      assume that

       A26: f in ( Hom (d,( cod p1))) and

       A27: g in ( Hom (d,( cod p2)));

      (g opp ) in ( Hom ((( cod p2) opp ),(d opp ))) by A27, OPPCAT_1: 5;

      then

       A28: (g opp ) in ( Hom (( dom (p2 opp )),(d opp ))) by A23, A24, OPPCAT_1: 12;

      (f opp ) in ( Hom ((( cod p1) opp ),(d opp ))) by A26, OPPCAT_1: 5;

      then (f opp ) in ( Hom (( dom (p1 opp )),(d opp ))) by A20, A21, OPPCAT_1: 12;

      then

      consider h be Morphism of (C opp ) such that

       A29: h in ( Hom ((c opp ),(d opp ))) and

       A30: for k be Morphism of (C opp ) st k in ( Hom ((c opp ),(d opp ))) holds (k (*) i1) = (f opp ) & (k (*) i2) = (g opp ) iff h = k by A19, A28;

      take ( opp h);

      thus ( opp h) in ( Hom (d,c)) by A29, OPPCAT_1: 5;

      let k;

      assume

       A31: k in ( Hom (d,c));

      then (k opp ) in ( Hom ((c opp ),(d opp ))) by OPPCAT_1: 5;

      then

       A32: ((k opp ) (*) i1) = (f opp ) & ((k opp ) (*) i2) = (g opp ) iff h = (k opp ) by A30;

      

       A33: ( cod k) = c by A31, CAT_1: 1;

      reconsider ff = p1 as Morphism of ( dom p1), ( cod p1) by CAT_1: 4;

      reconsider gg = k as Morphism of ( dom k), ( dom p1) by A33, A22, CAT_1: 4;

      

       A34: ( Hom (( dom k),( cod k))) <> {} & ( Hom (( dom p1),( cod p1))) <> {} by CAT_1: 2;

      then

       A35: (ff opp ) = (p1 opp ) by OPPCAT_1:def 6;

      

       A36: (gg opp ) = (k opp ) by A34, A33, A22, OPPCAT_1:def 6;

      

       A37: ((p1 (*) k) opp ) = ((k opp ) (*) (p1 opp )) by A22, A34, A33, A35, A36, OPPCAT_1: 16;

      reconsider ff = p2 as Morphism of ( dom p2), ( cod p2) by CAT_1: 4;

      reconsider gg = k as Morphism of ( dom k), ( dom p2) by A33, A25, CAT_1: 4;

      

       A38: ( Hom (( dom k),( cod k))) <> {} & ( Hom (( dom p2),( cod p2))) <> {} by CAT_1: 2;

      then

       A39: (ff opp ) = (p2 opp ) by OPPCAT_1:def 6;

      

       A40: (gg opp ) = (k opp ) by A38, A33, A25, OPPCAT_1:def 6;

      ((p2 (*) k) opp ) = ((k opp ) (*) (p2 opp )) by A38, A33, A39, A40, A25, OPPCAT_1: 16;

      hence thesis by A37, A32;

    end;

    theorem :: CAT_3:79

    

     Th79: x1 <> x2 implies (c is_a_coproduct_wrt (i1,i2) iff c is_a_coproduct_wrt ((x1,x2) --> (i1,i2)))

    proof

      set F = ((x1,x2) --> (i1,i2)), I = {x1, x2};

      assume

       A1: x1 <> x2;

      thus c is_a_coproduct_wrt (i1,i2) implies c is_a_coproduct_wrt F

      proof

        assume

         A2: c is_a_coproduct_wrt (i1,i2);

        then ( cod i1) = c & ( cod i2) = c;

        hence F is Injections_family of c, I by Th65;

        let b;

        let F9 be Injections_family of b, I such that

         A3: ( doms F) = ( doms F9);

        set f = (F9 /. x1), g = (F9 /. x2);

        

         A4: x1 in I by TARSKI:def 2;

        then (( doms F) /. x1) = ( dom (F /. x1)) by Def1;

        then ( dom f) = ( dom (F /. x1)) by A3, A4, Def1;

        then

         A5: ( dom f) = ( dom i1) by A1, Th3;

        

         A6: x2 in I by TARSKI:def 2;

        then (( doms F) /. x2) = ( dom (F /. x2)) by Def1;

        then ( dom g) = ( dom (F /. x2)) by A3, A6, Def1;

        then

         A7: ( dom g) = ( dom i2) by A1, Th3;

        ( cod g) = b by A6, Th62;

        then

         A8: g in ( Hom (( dom i2),b)) by A7;

        ( cod f) = b by A4, Th62;

        then f in ( Hom (( dom i1),b)) by A5;

        then

        consider h such that

         A9: h in ( Hom (c,b)) and

         A10: for k st k in ( Hom (c,b)) holds (k (*) i1) = f & (k (*) i2) = g iff h = k by A2, A8;

        take h;

        thus h in ( Hom (c,b)) by A9;

        let k such that

         A11: k in ( Hom (c,b));

        thus (for x st x in I holds (k (*) (F /. x)) = (F9 /. x)) implies h = k

        proof

          assume

           A12: for x st x in I holds (k (*) (F /. x)) = (F9 /. x);

          then (k (*) (F /. x2)) = g by A6;

          then

           A13: (k (*) i2) = g by A1, Th3;

          (k (*) (F /. x1)) = f by A4, A12;

          then (k (*) i1) = f by A1, Th3;

          hence thesis by A10, A11, A13;

        end;

        assume h = k;

        then

         A14: (k (*) i1) = f & (k (*) i2) = g by A10, A11;

        let x;

        assume x in I;

        then x = x1 or x = x2 by TARSKI:def 2;

        hence thesis by A1, A14, Th3;

      end;

      assume

       A15: c is_a_coproduct_wrt F;

      then

       A16: F is Injections_family of c, I;

      x2 in I by TARSKI:def 2;

      then

       A17: ( cod (F /. x2)) = c by A16, Th62;

      x1 in I by TARSKI:def 2;

      then ( cod (F /. x1)) = c by A16, Th62;

      hence ( cod i1) = c & ( cod i2) = c by A1, A17, Th3;

      let d, f, g such that

       A18: f in ( Hom (( dom i1),d)) and

       A19: g in ( Hom (( dom i2),d));

      ( cod f) = d & ( cod g) = d by A18, A19, CAT_1: 1;

      then

      reconsider F9 = ((x1,x2) --> (f,g)) as Injections_family of d, I by Th65;

      ( doms F) = ((x1,x2) --> (( dom i1),( dom i2))) by Th6

      .= ((x1,x2) --> (( dom f),( dom i2))) by A18, CAT_1: 1

      .= ((x1,x2) --> (( dom f),( dom g))) by A19, CAT_1: 1

      .= ( doms F9) by Th6;

      then

      consider h such that

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

       A21: for k st k in ( Hom (c,d)) holds (for x st x in I holds (k (*) (F /. x)) = (F9 /. x)) iff h = k by A15;

      take h;

      thus h in ( Hom (c,d)) by A20;

      let k such that

       A22: k in ( Hom (c,d));

      thus (k (*) i1) = f & (k (*) i2) = g implies h = k

      proof

        assume

         A23: (k (*) i1) = f & (k (*) i2) = g;

        now

          let x;

          assume x in I;

          then x = x1 or x = x2 by TARSKI:def 2;

          then (F /. x) = i1 & (F9 /. x) = f or (F /. x) = i2 & (F9 /. x) = g by A1, Th3;

          hence (k (*) (F /. x)) = (F9 /. x) by A23;

        end;

        hence thesis by A21, A22;

      end;

      assume

       A24: h = k;

      x2 in I by TARSKI:def 2;

      then (k (*) (F /. x2)) = (F9 /. x2) by A21, A22, A24;

      then

       A25: (k (*) (F /. x2)) = g by A1, Th3;

      x1 in I by TARSKI:def 2;

      then (k (*) (F /. x1)) = (F9 /. x1) by A21, A22, A24;

      then (k (*) (F /. x1)) = f by A1, Th3;

      hence thesis by A1, A25, Th3;

    end;

    theorem :: CAT_3:80

    c is_a_coproduct_wrt (i1,i2) & d is_a_coproduct_wrt (j1,j2) & ( dom i1) = ( dom j1) & ( dom i2) = ( dom j2) implies (c,d) are_isomorphic

    proof

      assume that

       A1: c is_a_coproduct_wrt (i1,i2) and

       A2: d is_a_coproduct_wrt (j1,j2) and

       A3: ( dom i1) = ( dom j1) & ( dom i2) = ( dom j2);

      set I = { 0 , { 0 }}, F = (( 0 , { 0 }) --> (i1,i2)), F9 = (( 0 , { 0 }) --> (j1,j2));

      

       A4: c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 by A1, A2, Th79;

      ( doms F) = (( 0 , { 0 }) --> (( dom j1),( dom j2))) by A3, Th6

      .= ( doms F9) by Th6;

      hence thesis by A4, Th72;

    end;

    theorem :: CAT_3:81

    ( Hom (a,c)) <> {} & ( Hom (b,c)) <> {} implies for i1 be Morphism of a, c, i2 be Morphism of b, c holds c is_a_coproduct_wrt (i1,i2) iff for d st ( Hom (a,d)) <> {} & ( Hom (b,d)) <> {} holds ( Hom (c,d)) <> {} & for f be Morphism of a, d, g be Morphism of b, d holds ex h be Morphism of c, d st for k be Morphism of c, d holds (k * i1) = f & (k * i2) = g iff h = k

    proof

      assume that

       A1: ( Hom (a,c)) <> {} and

       A2: ( Hom (b,c)) <> {} ;

      let i1 be Morphism of a, c, i2 be Morphism of b, c;

      thus c is_a_coproduct_wrt (i1,i2) implies for d st ( Hom (a,d)) <> {} & ( Hom (b,d)) <> {} holds ( Hom (c,d)) <> {} & for f be Morphism of a, d, g be Morphism of b, d holds ex h be Morphism of c, d st for k be Morphism of c, d holds (k * i1) = f & (k * i2) = g iff h = k

      proof

        assume that ( cod i1) = c and ( cod i2) = c and

         A3: for d, f, g st f in ( Hom (( dom i1),d)) & g in ( Hom (( dom i2),d)) holds ex h st h in ( Hom (c,d)) & for k st k in ( Hom (c,d)) holds (k (*) i1) = f & (k (*) i2) = g iff h = k;

        let d such that

         A4: ( Hom (a,d)) <> {} and

         A5: ( Hom (b,d)) <> {} ;

        set f = the Morphism of a, d, g = the Morphism of b, d;

        

         A6: ( dom i2) = b by A2, CAT_1: 5;

        then

         A7: g in ( Hom (( dom i2),d)) by A5, CAT_1:def 5;

        

         A8: ( dom i1) = a by A1, CAT_1: 5;

        then f in ( Hom (( dom i1),d)) by A4, CAT_1:def 5;

        then

         A9: ex h st h in ( Hom (c,d)) & for k st k in ( Hom (c,d)) holds (k (*) i1) = f & (k (*) i2) = g iff h = k by A3, A7;

        hence ( Hom (c,d)) <> {} ;

        let f be Morphism of a, d, g be Morphism of b, d;

        

         A10: g in ( Hom (( dom i2),d)) by A5, A6, CAT_1:def 5;

        f in ( Hom (( dom i1),d)) by A4, A8, CAT_1:def 5;

        then

        consider h such that

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

         A12: for k st k in ( Hom (c,d)) holds (k (*) i1) = f & (k (*) i2) = g iff h = k by A3, A10;

        reconsider h as Morphism of c, d by A11, CAT_1:def 5;

        take h;

        let k be Morphism of c, d;

        

         A13: k in ( Hom (c,d)) by A9, CAT_1:def 5;

        (k * i1) = (k (*) i1 qua Morphism of C) & (k * i2) = (k (*) i2 qua Morphism of C) by A1, A2, A9, CAT_1:def 13;

        hence thesis by A12, A13;

      end;

      assume

       A14: for d st ( Hom (a,d)) <> {} & ( Hom (b,d)) <> {} holds ( Hom (c,d)) <> {} & for f be Morphism of a, d, g be Morphism of b, d holds ex h be Morphism of c, d st for k be Morphism of c, d holds (k * i1) = f & (k * i2) = g iff h = k;

      thus ( cod i1) = c & ( cod i2) = c by A1, A2, CAT_1: 5;

      let d, f, g such that

       A15: f in ( Hom (( dom i1),d)) and

       A16: g in ( Hom (( dom i2),d));

      

       A17: ( Hom (a,d)) <> {} by A1, A15, CAT_1: 5;

      

       A18: ( dom i1) = a by A1, CAT_1: 5;

      then

       A19: f is Morphism of a, d by A15, CAT_1:def 5;

      

       A20: ( dom i2) = b by A2, CAT_1: 5;

      then g is Morphism of b, d by A16, CAT_1:def 5;

      then

      consider h be Morphism of c, d such that

       A21: for k be Morphism of c, d holds (k * i1) = f & (k * i2) = g iff h = k by A14, A16, A20, A19, A17;

      reconsider h9 = h as Morphism of C;

      take h9;

      

       A22: ( Hom (c,d)) <> {} by A14, A15, A16, A18, A20;

      hence h9 in ( Hom (c,d)) by CAT_1:def 5;

      let k;

      assume k in ( Hom (c,d));

      then

      reconsider k9 = k as Morphism of c, d by CAT_1:def 5;

      (k (*) i1) = (k9 * i1) & (k (*) i2) = (k9 * i2) by A1, A2, A22, CAT_1:def 13;

      hence thesis by A21;

    end;

    theorem :: CAT_3:82

    for i1 be Morphism of a, c, i2 be Morphism of b, c st ( Hom (a,c)) <> {} & ( Hom (b,c)) <> {} holds c is_a_coproduct_wrt (i1,i2) & ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} implies i1 is coretraction & i2 is coretraction

    proof

      let i1 be Morphism of a, c, i2 be Morphism of b, c such that

       A1: ( Hom (a,c)) <> {} & ( Hom (b,c)) <> {} ;

      assume that

       A2: c is_a_coproduct_wrt (i1,i2) and

       A3: ( Hom (a,b)) <> {} & ( Hom (b,a)) <> {} ;

      set I = { 0 , { 0 }};

      ( cod i1) = c & ( cod i2) = c by A2;

      then

      reconsider F = (( 0 , { 0 }) --> (i1,i2)) as Injections_family of c, I by Th65;

      

       A4: (F /. 0 ) = i1 by Th3;

      

       A5: (F /. { 0 }) = i2 by Th3;

       A6:

      now

        thus F is Injections_family of c, I;

        thus c is_a_coproduct_wrt F by A2, Th79;

        let x1, x2;

        assume that

         A7: x1 in I and

         A8: x2 in I;

        

         A9: x2 = 0 or x2 = { 0 } by A8, TARSKI:def 2;

        x1 = 0 or x1 = { 0 } by A7, TARSKI:def 2;

        then

         A10: ( dom (F /. x1)) = a or ( dom (F /. x1)) = b by A4, A5, A1, CAT_1: 5;

        ( dom (F /. x2)) = a or ( dom (F /. x2)) = b by A9, A4, A5, A1, CAT_1: 5;

        hence ( Hom (( dom (F /. x1)),( dom (F /. x2)))) <> {} by A3, A10;

      end;

      

       A11: { 0 } in I by TARSKI:def 2;

      

       A12: 0 in I by TARSKI:def 2;

      ( dom (F /. 0 )) = a & ( dom (F /. { 0 })) = b by A4, A5, A1, CAT_1: 5;

      hence thesis by A4, A6, A11, Th73, A5, A12, A1;

    end;

    theorem :: CAT_3:83

    

     Th83: c is_a_coproduct_wrt (i1,i2) & h in ( Hom (c,c)) & (h (*) i1) = i1 & (h (*) i2) = i2 implies h = ( id c)

    proof

      assume that

       A1: ( cod i1) = c & ( cod i2) = c and

       A2: for d, f, g st f in ( Hom (( dom i1),d)) & g in ( Hom (( dom i2),d)) holds ex h st h in ( Hom (c,d)) & for k st k in ( Hom (c,d)) holds (k (*) i1) = f & (k (*) i2) = g iff h = k and

       A3: h in ( Hom (c,c)) & (h (*) i1) = i1 & (h (*) i2) = i2;

      i1 in ( Hom (( dom i1),c)) & i2 in ( Hom (( dom i2),c)) by A1;

      then

      consider i such that i in ( Hom (c,c)) and

       A4: for k st k in ( Hom (c,c)) holds (k (*) i1) = i1 & (k (*) i2) = i2 iff i = k by A2;

      

       A5: ( id c) in ( Hom (c,c)) by CAT_1: 27;

      (( id c) (*) i1) = i1 & (( id c) (*) i2) = i2 by A1, CAT_1: 21;

      

      hence ( id c) = i by A4, A5

      .= h by A3, A4;

    end;

    theorem :: CAT_3:84

    for f be Morphism of c, d holds c is_a_coproduct_wrt (i1,i2) & ( dom f) = c & ( cod f) = d & f is invertible implies d is_a_coproduct_wrt ((f (*) i1),(f (*) i2))

    proof

      let f be Morphism of c, d;

      assume that

       A1: c is_a_coproduct_wrt (i1,i2) and

       A2: ( dom f) = c & ( cod f) = d & f is invertible;

      c is_a_coproduct_wrt (( 0 , { 0 }) --> (i1,i2)) by A1, Th79;

      then d is_a_coproduct_wrt (f * (( 0 , { 0 }) --> (i1,i2))) by A2, Th74;

      then d is_a_coproduct_wrt (( 0 , { 0 }) --> ((f (*) i1),(f (*) i2))) by Th15;

      hence thesis by Th79;

    end;

    theorem :: CAT_3:85

    c is_a_coproduct_wrt (i1,i2) & ( dom i2) is initial implies (( dom i1),c) are_isomorphic

    proof

      set a = ( dom i1), b = ( dom i2);

      assume that

       A1: c is_a_coproduct_wrt (i1,i2) and

       A2: b is initial;

      set f = ( id a), g = ( init (b,a));

      ( cod g) = a & ( dom g) = b by A2, Th38;

      then f in ( Hom (a,a)) & g in ( Hom (b,a)) by CAT_1: 27;

      then

      consider h such that

       A3: h in ( Hom (c,a)) and

       A4: for k st k in ( Hom (c,a)) holds (k (*) i1) = f & (k (*) i2) = g iff h = k by A1;

      

       A5: ( cod h) = a by A3, CAT_1: 1;

      

       A6: ( cod i1) = c by A1;

      then

      reconsider i = i1 as Morphism of a, c by CAT_1: 4;

      

       A7: ( dom h) = c by A3, CAT_1: 1;

      then

       A8: ( dom (i (*) h)) = c by A5, CAT_1: 17;

      

       A9: ( cod i2) = c by A1;

      then

       A10: ( dom ((i (*) h) (*) i2)) = b by A8, CAT_1: 17;

      

       A11: ( cod (i (*) h)) = c by A6, A5, CAT_1: 17;

      then

       A12: (i (*) h) in ( Hom (c,c)) by A8;

      ( cod ((i (*) h) (*) i2)) = c by A9, A11, A8, CAT_1: 17;

      

      then

       A13: ((i (*) h) (*) i2) = ( init (b,c)) by A2, A10, Th39

      .= i2 by A2, A9, Th39;

      

       A14: ( Hom (a,c)) <> {} by A6, CAT_1: 2;

      take i;

      thus ( Hom (a,c)) <> {} & ( Hom (c,a)) <> {} by A3, A6, CAT_1: 2;

      reconsider h as Morphism of c, a by A3, CAT_1:def 5;

      take h;

      

       A15: ((i (*) h) (*) i1) = (i (*) (h (*) i1)) by A6, A5, A7, CAT_1: 18

      .= (i (*) ( id ( dom i))) by A3, A4

      .= i by CAT_1: 22;

      

      thus (i * h) = (i (*) h) by A3, A14, CAT_1:def 13

      .= ( id c) by A1, A13, A12, Th83, A15;

      

      thus ( id a) = (h (*) i) by A3, A4

      .= (h * i) by A14, A3, CAT_1:def 13;

    end;

    theorem :: CAT_3:86

    c is_a_coproduct_wrt (i1,i2) & ( dom i1) is initial implies (( dom i2),c) are_isomorphic

    proof

      set a = ( dom i1), b = ( dom i2);

      assume that

       A1: c is_a_coproduct_wrt (i1,i2) and

       A2: a is initial;

      set f = ( id b), g = ( init (a,b));

      ( cod g) = b & ( dom g) = a by A2, Th38;

      then f in ( Hom (b,b)) & g in ( Hom (a,b)) by CAT_1: 27;

      then

      consider h such that

       A3: h in ( Hom (c,b)) and

       A4: for k st k in ( Hom (c,b)) holds (k (*) i1) = g & (k (*) i2) = f iff h = k by A1;

      

       A5: ( cod h) = b by A3, CAT_1: 1;

      

       A6: ( cod i2) = c by A1;

      then

      reconsider i = i2 as Morphism of b, c by CAT_1: 4;

      

       A7: ( dom h) = c by A3, CAT_1: 1;

      then

       A8: ( dom (i (*) h)) = c by A5, CAT_1: 17;

      

       A9: ( cod i1) = c by A1;

      then

       A10: ( dom ((i (*) h) (*) i1)) = a by A8, CAT_1: 17;

      

       A11: ( cod (i (*) h)) = c by A6, A5, CAT_1: 17;

      then

       A12: (i (*) h) in ( Hom (c,c)) by A8;

      ( cod ((i (*) h) (*) i1)) = c by A9, A11, A8, CAT_1: 17;

      

      then

       A13: ((i (*) h) (*) i1) = ( init (a,c)) by A2, A10, Th39

      .= i1 by A2, A9, Th39;

      

       A14: ( Hom (b,c)) <> {} by A6, CAT_1: 2;

      take i;

      thus ( Hom (b,c)) <> {} & ( Hom (c,b)) <> {} by A6, A3, CAT_1: 2;

      reconsider h as Morphism of c, b by A3, CAT_1:def 5;

      take h;

      

       A15: ((i (*) h) (*) i2) = (i (*) (h (*) i2)) by A6, A5, A7, CAT_1: 18

      .= (i (*) ( id ( dom i))) by A3, A4

      .= i by CAT_1: 22;

      

      thus (i * h) = (i (*) h) by A3, A14, CAT_1:def 13

      .= ( id c) by A1, A13, A12, Th83, A15;

      

      thus ( id b) = (h (*) i) by A3, A4

      .= (h * i) by A3, A14, CAT_1:def 13;

    end;