cat_5.miz

    begin

    theorem :: CAT_5:1



     Th1: for C be Category, D be non empty non void CatStr st the CatStr of C = the CatStr of D holds D is Category-like transitive associative reflexive with_identities

    proof

      let C be Category, D be non empty non void CatStr such that

       A1: the CatStr of C = the CatStr of D;

      thus

       A2: for f,g be Morphism of D holds [g, f] in ( dom the Comp of D) iff ( dom g) = ( cod f)

      proof

        let f,g be Morphism of D;

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



         A3: [gg, ff] in ( dom the Comp of D) iff ( dom gg) = ( cod ff) by A1, CAT_1:def 6;

        thus [g, f] in ( dom the Comp of D) implies ( dom g) = ( cod f)

        proof

          assume

           A4: [g, f] in ( dom the Comp of D);



          thus ( dom g) = ( dom gg) by A1

          .= ( cod ff) by A4, A1, CAT_1:def 6

          .= ( cod f) by A1;

        end;

        thus thesis by A1, A3;

      end;

      thus

       A5: for f,g be Morphism of D st ( dom g) = ( cod f) holds ( dom (g (*) f)) = ( dom f) & ( cod (g (*) f)) = ( cod g)

      proof

        let f,g be Morphism of D;

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

        assume

         A6: ( dom g) = ( cod f);



         A7: ( dom gg) = ( cod ff) by A1, A6;

        then [gg, ff] in ( dom the Comp of C) by CAT_1:def 6;

        then

         A8: (the Comp of C . (gg,ff)) = (gg (*) ff) by CAT_1:def 1;

        ( dom (gg (*) ff)) = ( dom ff) & ( cod (gg (*) ff)) = ( cod gg) by A7, CAT_1:def 7;

        hence thesis by A1, A8, A6, A2, CAT_1:def 1;

      end;



       A9: for f,g be Morphism of D st ( cod g) = ( dom f) holds for ff,gg be Morphism of C st ff = f & gg = g holds (f (*) g) = (ff (*) gg)

      proof

        let f,g be Morphism of D such that

         A10: ( cod g) = ( dom f);

        let ff,gg be Morphism of C such that

         A11: ff = f & gg = g;



         A12: ( cod gg) = ( dom ff) by A10, A11, A1;



        thus (f (*) g) = (the Comp of D . (f,g)) by A10, A2, CAT_1:def 1

        .= (the Comp of C . (ff,gg)) by A1, A11

        .= (ff (*) gg) by A12, CAT_1: 16;

      end;

      thus for f,g,h be Morphism of D st ( dom h) = ( cod g) & ( dom g) = ( cod f) holds (h (*) (g (*) f)) = ((h (*) g) (*) f)

      proof

        let f,g,h be Morphism of D;

        reconsider ff = f, gg = g, hh = h as Morphism of C by A1;

        assume that

         A13: ( dom h) = ( cod g) and

         A14: ( dom g) = ( cod f);



         A15: ( dom hh) = ( cod gg) & ( dom gg) = ( cod ff) by A13, A14, A1;



         A16: (g (*) f) = (gg (*) ff) by A14, A9;



         A17: (h (*) g) = (hh (*) gg) by A13, A9;



         A18: ( dom (h (*) g)) = ( dom g) by A13, A5;

        ( cod (g (*) f)) = ( cod g) by A14, A5;



        hence (h (*) (g (*) f)) = (hh (*) (gg (*) ff)) by A9, A16, A13

        .= ((hh (*) gg) (*) ff) by A15, CAT_1:def 8

        .= ((h (*) g) (*) f) by A14, A9, A17, A18;

      end;

      thus D is reflexive

      proof

        let b be Element of D;

        reconsider bb = b as Element of C by A1;

        reconsider ii = ( id bb) as Morphism of D by A1;



         A19: ( cod ii) = ( cod ( id bb)) by A1

        .= b;

        ( dom ii) = ( dom ( id bb)) by A1

        .= b;

        then ( id bb) in ( Hom (b,b)) by A19;

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

      end;

      let a be Element of D;

      reconsider aa = a as Element of C by A1;

      reconsider ii = ( id aa) as Morphism of D by A1;



       A20: ( cod ii) = ( cod ( id aa)) by A1

      .= a;

      ( dom ii) = ( dom ( id aa)) by A1

      .= a;

      then

      reconsider ii as Morphism of a, a by A20, CAT_1: 4;

      take ii;

      let b be Element of D;

      reconsider bb = b as Element of C by A1;

      thus ( Hom (a,b)) <> {} implies for g be Morphism of a, b holds (g (*) ii) = g

      proof

        assume

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

        let g be Morphism of a, b;

        reconsider gg = g as Morphism of C by A1;



         A22: ( cod gg) = ( cod g) by A1

        .= bb by A21, CAT_1: 5;



         A23: ( cod ( id aa)) = aa;



         A24: ( dom gg) = ( dom g) by A1

        .= aa by A21, CAT_1: 5;

        then gg in ( Hom (aa,bb)) by A22;

        then

        reconsider gg as Morphism of aa, bb by CAT_1:def 5;



         A25: ( dom g) = ( dom gg) by A1

        .= a by A24;

        ( cod ii) = ( cod ( id aa)) by A1

        .= a;



        hence (g (*) ii) = (the Comp of D . (g,ii)) by A25, A2, CAT_1:def 1

        .= (the Comp of C . (gg,( id aa))) by A1

        .= (gg (*) ( id aa)) by A23, A24, CAT_1: 16

        .= g by A24, CAT_1: 22;

      end;

      assume

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

      let g be Morphism of b, a;

      reconsider gg = g as Morphism of C by A1;



       A27: ( dom gg) = ( dom g) by A1

      .= bb by A26, CAT_1: 5;



       A28: ( dom ( id aa)) = aa;



       A29: ( cod gg) = ( cod g) by A1

      .= aa by A26, CAT_1: 5;

      then gg in ( Hom (bb,aa)) by A27;

      then

      reconsider gg as Morphism of bb, aa by CAT_1:def 5;



       A30: ( cod g) = ( cod gg) by A1

      .= a by A29;

      ( dom ii) = ( dom ( id aa)) by A1

      .= a;



      hence (ii (*) g) = (the Comp of D . (ii,g)) by A30, A2, CAT_1:def 1

      .= (the Comp of C . (( id aa),gg)) by A1

      .= (( id aa) (*) gg) by A28, A29, CAT_1: 16

      .= g by A29, CAT_1: 21;

    end;



     Lm1: for C,D be Category st the CatStr of C = the CatStr of D holds for c be Element of C, d be Element of D st c = d holds ( id c) = ( id d)

    proof

      let C,D be Category such that

       A1: the CatStr of C = the CatStr of D;

      let c be Element of C, d be Element of D such that

       A2: c = d;

      reconsider ii = ( id c) as Morphism of D by A1;



       A3: ( cod ii) = ( cod ( id c)) by A1

      .= d by A2;



       A4: ( dom ii) = ( dom ( id c)) by A1

      .= d by A2;

      then

      reconsider ii as Morphism of d, d by A3, CAT_1: 4;

      for b be Object of D holds (( Hom (d,b)) <> {} implies for f be Morphism of d, b holds (f (*) ii) = f) & (( Hom (b,d)) <> {} implies for f be Morphism of b, d holds (ii (*) f) = f)

      proof

        let b be Object of D;

        reconsider bb = b as Element of C by A1;

        thus ( Hom (d,b)) <> {} implies for f be Morphism of d, b holds (f (*) ii) = f

        proof

          assume

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

          let f be Morphism of d, b;

          reconsider ff = f as Morphism of C by A1;



           A6: ( dom ff) = ( dom f) by A1

          .= c by A2, A5, CAT_1: 5;



           A7: ( cod ( id c)) = c

          .= ( dom ff) by A6;

          ( cod ii) = d by A3

          .= ( dom f) by A5, CAT_1: 5;



          hence (f (*) ii) = (the Comp of D . (f,ii)) by CAT_1: 16

          .= (the Comp of C . (ff,( id c))) by A1

          .= (ff (*) ( id c)) by A7, CAT_1: 16

          .= f by A6, CAT_1: 22;

        end;

        assume

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

        let f be Morphism of b, d;

        reconsider ff = f as Morphism of C by A1;



         A9: ( cod ff) = ( cod f) by A1

        .= c by A2, A8, CAT_1: 5;



         A10: ( dom ( id c)) = c

        .= ( cod ff) by A9;

        ( dom ii) = d by A4

        .= ( cod f) by A8, CAT_1: 5;



        hence (ii (*) f) = (the Comp of D . (ii,f)) by CAT_1: 16

        .= (the Comp of C . (( id c),ff)) by A1

        .= (( id c) (*) ff) by A10, CAT_1: 16

        .= f by A9, CAT_1: 21;

      end;

      hence ( id c) = ( id d) by CAT_1:def 12;

    end;

    definition

      let IT be non void non empty CatStr;

      :: CAT_5:def1

      attr IT is with_triple-like_morphisms means

      : Def1: for f be Morphism of IT holds ex x be set st f = [ [( dom f), ( cod f)], x];

    end

    registration

      cluster with_triple-like_morphisms for strict Category;

      existence

      proof

        take C = ( 1Cat ( 0 , [ [ 0 , 0 ], 1]));

        let f be Morphism of C;

        take 1;

        ( dom f) = 0 by TARSKI:def 1;

        hence thesis by TARSKI:def 1;

      end;

    end

    theorem :: CAT_5:2



     Th2: for C be with_triple-like_morphisms non void non empty CatStr, f be Morphism of C holds ( dom f) = (f `11 ) & ( cod f) = (f `12 ) & f = [ [( dom f), ( cod f)], (f `2 )]

    proof

      let C be with_triple-like_morphisms non void non empty CatStr;

      let f be Morphism of C;

      ex x be set st (f = [ [( dom f), ( cod f)], x]) by Def1;

      hence thesis by MCART_1: 85;

    end;

    definition

      let C be with_triple-like_morphisms non void non empty CatStr;

      let f be Morphism of C;

      :: original: `11

      redefine

      func f `11 -> Object of C ;

      coherence

      proof

        (f `11 ) = ( dom f) by Th2;

        hence thesis;

      end;

      :: original: `12

      redefine

      func f `12 -> Object of C ;

      coherence

      proof

        (f `12 ) = ( cod f) by Th2;

        hence thesis;

      end;

    end

    scheme :: CAT_5:sch1

    CatEx { A,B() -> non empty set , P[ set, set, set], F( object, object) -> set } :

ex C be with_triple-like_morphisms strict Category st the carrier of C = A() & (for a,b be Element of A(), f be Element of B() st P[a, b, f] holds [ [a, b], f] is Morphism of C) & (for m be Morphism of C holds ex a,b be Element of A(), f be Element of B() st m = [ [a, b], f] & P[a, b, f]) & for m1,m2 be Morphism of C, a1,a2,a3 be Element of A(), f1,f2 be Element of B() st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)]

      provided

       A1: for a,b,c be Element of A(), f,g be Element of B() st P[a, b, f] & P[b, c, g] holds F(g,f) in B() & P[a, c, F(g,f)]

       and

       A2: for a be Element of A() holds ex f be Element of B() st P[a, a, f] & for b be Element of A(), g be Element of B() holds (P[a, b, g] implies F(g,f) = g) & (P[b, a, g] implies F(f,g) = g)

       and

       A3: for a,b,c,d be Element of A(), f,g,h be Element of B() st P[a, b, f] & P[b, c, g] & P[c, d, h] holds F(h,F) = F(F,f);

      set M = { [ [a, b], f] where a be Element of A(), b be Element of A(), f be Element of B() : P[a, b, f] };

      set a0 = the Element of A();

      consider f0 be Element of B() such that

       A4: P[a0, a0, f0] and for b be Element of A(), g be Element of B() holds (P[a0, b, g] implies F(g,f0) = g) & (P[b, a0, g] implies F(f0,g) = g) by A2;



       A5: [ [a0, a0], f0] in M by A4;

      M c= [: [:A(), A():], B():]

      proof

        let x be object;

        assume x in M;

        then ex a,b be Element of A(), f be Element of B() st x = [ [a, b], f] & P[a, b, f];

        hence thesis;

      end;

      then

      reconsider M as non empty Subset of [: [:A(), A():], B():] by A5;

       A6:

      now

        let m be Element of M;

        m in M;

        then

        consider a,b be Element of A(), f be Element of B() such that

         A7: m = [ [a, b], f] and

         A8: P[a, b, f];



         A9: (m `11 ) = a by A7, MCART_1: 85;

        (m `12 ) = b by A7, MCART_1: 85;

        hence m = [ [(m `11 ), (m `12 )], (m `2 )] & P[(m `11 ), (m `12 ), (m `2 )] by A7, A8, A9;

      end;

      deffunc f( Element of M) = ($1 `11 );

      consider DM be Function of M, A() such that

       A10: for m be Element of M holds (DM . m) = f(m) from FUNCT_2:sch 4;

      deffunc g( Element of M) = ($1 `12 );

      consider CM be Function of M, A() such that

       A11: for m be Element of M holds (CM . m) = g(m) from FUNCT_2:sch 4;

      deffunc f( object, object) = [ [($2 `11 ), ($1 `12 )], F(`2,`2)];

      defpred P[ object, object] means ($1 `11 ) = ($2 `12 ) & $1 in M & $2 in M;

       A12:

      now

        let x,y be object;

        assume

         A13: P[x, y];

        then

        consider ax,bx be Element of A(), fx be Element of B() such that

         A14: x = [ [ax, bx], fx] and

         A15: P[ax, bx, fx];

        consider ay,b2 be Element of A(), fy be Element of B() such that

         A16: y = [ [ay, b2], fy] and

         A17: P[ay, b2, fy] by A13;



         A18: (x `11 ) = ax by A14, MCART_1: 85;



         A19: (x `12 ) = bx by A14, MCART_1: 85;



         A20: (y `11 ) = ay by A16, MCART_1: 85;



         A21: (y `12 ) = b2 by A16, MCART_1: 85;



         A22: (x `2 ) = fx by A14;



         A23: (y `2 ) = fy by A16;



         A24: F(fx,fy) in B() by A1, A13, A15, A17, A18, A21;

        P[ay, bx, F(fx,fy)] by A1, A13, A15, A17, A18, A21;

        hence f(x,y) in M by A19, A20, A22, A23, A24;

      end;

      consider CC be PartFunc of [:M, M:], M such that

       A25: for x,y be object holds [x, y] in ( dom CC) iff x in M & y in M & P[x, y] and

       A26: for x,y be object st [x, y] in ( dom CC) holds (CC . (x,y)) = f(x,y) from BINOP_1:sch 6( A12);

      defpred II[ Element of A(), set] means ex f be Element of B() st $2 = [ [$1, $1], f] & P[$1, $1, f] & for b be Element of A(), g be Element of B() holds (P[$1, b, g] implies F(g,f) = g) & (P[b, $1, g] implies F(f,g) = g);

       A27:

      now

        let a be Element of A();

        consider f be Element of B() such that

         A28: P[a, a, f] and

         A29: for b be Element of A(), g be Element of B() holds (P[a, b, g] implies F(g,f) = g) & (P[b, a, g] implies F(f,g) = g) by A2;

         [ [a, a], f] in M by A28;

        then

        reconsider y = [ [a, a], f] as Element of M;

        take y;

        thus II[a, y] by A28, A29;

      end;

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

       A30: for o be Element of A() holds II[o, (I . o)] from FUNCT_2:sch 3( A27);

      set C = CatStr (# A(), M, DM, CM, CC #);



       A31: C is Category-like

      proof

        now

          let f,g be Morphism of C;



           A32: [g, f] in ( dom CC) iff g in M & f in M & (g `11 ) = (f `12 ) & g in M & f in M by A25;

          (DM . g) = (g `11 ) by A10;

          hence [g, f] in ( dom the Comp of C) iff ( dom g) = ( cod f) by A11, A32;

        end;

      end;



       A33: for f,g be Morphism of C holds [g, f] in ( dom the Comp of C) iff ( dom g) = ( cod f) by A31;



       A34: C is transitive

      proof

        let f,g be Morphism of C;



         A35: (the Source of C . f) = (f `11 ) by A10;



         A36: (the Source of C . g) = (g `11 ) by A10;



         A37: (the Target of C . f) = (f `12 ) by A11;



         A38: (the Target of C . g) = (g `12 ) by A11;

        assume

         A39: ( dom g) = ( cod f);

        then

         A40: (CC . (g,f)) = [ [(f `11 ), (g `12 )], F(`2,`2)] by A26, A25, A36, A37;



         A41: ((CC . [g, f]) `11 ) = (f `11 ) by A40, MCART_1: 85;



         A42: (the Comp of C . (g,f)) = (g (*) f) by A39, A25, A36, A37, CAT_1:def 1;

        ((CC . [g, f]) `12 ) = (g `12 ) by A40, MCART_1: 85;

        hence ( dom (g (*) f)) = ( dom f) & ( cod (g (*) f)) = ( cod g) by A10, A11, A35, A38, A41, A42;

      end;



       A43: C is associative

      proof

        let f,g,h be Morphism of C;



         A44: (the Source of C . g) = (g `11 ) by A10;



         A45: (the Source of C . h) = (h `11 ) by A10;



         A46: (the Target of C . f) = (f `12 ) by A11;



         A47: (the Target of C . g) = (g `12 ) by A11;

        assume that

         A48: ( dom h) = ( cod g) and

         A49: ( dom g) = ( cod f);



         A50: [g, f] in ( dom CC) by A25, A44, A46, A49;



         A51: [h, g] in ( dom CC) by A25, A45, A47, A48;



         A52: (CC . [g, f]) in ( rng CC) by A50, FUNCT_1:def 3;

        (CC . [h, g]) in ( rng CC) by A51, FUNCT_1:def 3;

        then

        reconsider gf = (CC . (g,f)), hg = (CC . (h,g)) as Element of M by A52;



         A53: gf = [ [(f `11 ), (g `12 )], F(`2,`2)] by A26, A25, A44, A46, A49;



         A54: hg = [ [(g `11 ), (h `12 )], F(`2,`2)] by A26, A25, A45, A47, A48;



         A55: (DM . gf) = (gf `11 ) by A10;



         A56: (DM . hg) = (hg `11 ) by A10;



         A57: (CM . gf) = (gf `12 ) by A11;



         A58: (CM . hg) = (hg `12 ) by A11;



         A59: (DM . gf) = (f `11 ) by A53, A55, MCART_1: 85;



         A60: (CM . gf) = (g `12 ) by A53, A57, MCART_1: 85;



         A61: (CM . hg) = (h `12 ) by A54, A58, MCART_1: 85;



         A62: [h, gf] in ( dom CC) by A25, A45, A11, A48, A57, A60;



         A63: [hg, f] in ( dom CC) by A25, A44, A46, A49, A56, A54, MCART_1: 85;

        reconsider f9 = f, g9 = g, h9 = h as Element of M;



         A64: P[(f9 `11 ), (f9 `12 ), (f9 `2 )] by A6;



         A65: P[(g9 `11 ), (g9 `12 ), (g9 `2 )] by A6;



         A66: P[(h9 `11 ), (h9 `12 ), (h9 `2 )] by A6;



         A67: (the Comp of C . (h,g)) = (h (*) g) by A33, A48, CAT_1:def 1;



         A68: ( dom (h (*) g)) = ( dom g) by A34, A48;



         A69: (the Comp of C . (g,f)) = (g (*) f) by A33, A49, CAT_1:def 1;

        ( cod (g (*) f)) = ( cod g) by A34, A49;



        hence (h (*) (g (*) f)) = (the Comp of C . (h,(the Comp of C . (g,f)))) by A69, A33, A48, CAT_1:def 1

        .= [ [(f `11 ), (h `12 )], F(`2,`2)] by A26, A55, A59, A62

        .= [ [(f `11 ), (h `12 )], F(`2,F)] by A53

        .= [ [(f `11 ), (h `12 )], F(F,`2)] by A3, A44, A45, A46, A47, A48, A49, A64, A65, A66

        .= [ [(f `11 ), (h `12 )], F(`2,`2)] by A54

        .= (the Comp of C . ((the Comp of C . (h,g)),f)) by A26, A58, A61, A63

        .= ((h (*) g) (*) f) by A67, A33, A49, A68, CAT_1:def 1;

      end;



       A70: C is reflexive

      proof

        let b be Object of C;

        consider f be Element of B() such that

         A71: (I . b) = [ [b, b], f] and P[b, b, f] and for c be Element of A(), g be Element of B() holds (P[b, c, g] implies F(g,f) = g) & (P[c, b, g] implies F(f,g) = g) by A30;

        reconsider bb = b as Element of A();

        reconsider Ib = (I . bb) as Element of M;

        reconsider ii = (I . bb) as Morphism of C;



         A72: ( cod ii) = ((I . b) `12 ) by A11

        .= b by A71, MCART_1: 85;

        ( dom ii) = ((I . b) `11 ) by A10

        .= b by A71, MCART_1: 85;

        then (I . b) in ( Hom (b,b)) by A72;

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

      end;

      C is with_identities

      proof

        let a be Object of C;

        consider f be Element of B() such that

         A73: (I . a) = [ [a, a], f] and P[a, a, f] and

         A74: for c be Element of A(), g be Element of B() holds (P[a, c, g] implies F(g,f) = g) & (P[c, a, g] implies F(f,g) = g) by A30;

        reconsider aa = a as Element of A();

        reconsider Ia = (I . aa) as Element of M;

        reconsider ii = (I . aa) as Morphism of C;



         A75: ( cod ii) = ((I . a) `12 ) by A11

        .= a by A73, MCART_1: 85;

        ( dom ii) = ((I . a) `11 ) by A10

        .= a by A73, MCART_1: 85;

        then

        reconsider ii as Morphism of a, a by A75, CAT_1: 4;

        take ii;

        let b be Element of C;

        thus ( Hom (a,b)) <> {} implies for g be Morphism of a, b holds (g (*) ii) = g

        proof

          assume

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

          let g be Morphism of a, b;

          reconsider bb = b as Element of A();

          g in M;

          then

          consider a1,b1 be Element of A(), f1 be Element of B() such that

           A77: g = [ [a1, b1], f1] and

           A78: P[a1, b1, f1];



           A79: a = ( dom g) by A76, CAT_1: 5

          .= (DM . g)

          .= ( [ [a1, b1], f1] `11 ) by A77, A10

          .= a1 by MCART_1: 85;

          then

           A80: F(f1,f) = f1 by A74, A78;



           A81: ( [ [a, a], f] `11 ) = a1 by A79, MCART_1: 85;



           A82: ( [ [a1, b1], f1] `12 ) = b1 by MCART_1: 85;

          (g `11 ) = ( [ [a1, b1], f1] `11 ) by A77

          .= a by A79, MCART_1: 85

          .= ( [ [a, a], f] `12 ) by MCART_1: 85

          .= (ii `12 ) by A73;

          then

           A83: [g, ii] in ( dom CC) by A25;



          hence (g (*) ii) = (the Comp of C . (g,ii)) by CAT_1:def 1

          .= (CC . (g,ii))

          .= [ [(ii `11 ), (g `12 )], F(`2,`2)] by A26, A83

          .= [ [a1, b1], f1] by A80, A81, A82, A77, A73

          .= g by A77;

        end;

        thus ( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (ii (*) f) = f

        proof

          assume

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

          let g be Morphism of b, a;

          reconsider bb = b as Element of A();

          g in M;

          then

          consider b1,a1 be Element of A(), f1 be Element of B() such that

           A85: g = [ [b1, a1], f1] and

           A86: P[b1, a1, f1];



           A87: a = ( cod g) by A84, CAT_1: 5

          .= (CM . g)

          .= ( [ [b1, a1], f1] `12 ) by A85, A11

          .= a1 by MCART_1: 85;

          then

           A88: F(f,f1) = f1 by A74, A86;



           A89: ( [ [a, a], f] `12 ) = a1 by A87, MCART_1: 85;



           A90: ( [ [b1, a1], f1] `11 ) = b1 by MCART_1: 85;

          (g `12 ) = ( [ [b1, a1], f1] `12 ) by A85

          .= a by A87, MCART_1: 85

          .= ( [ [a, a], f] `11 ) by MCART_1: 85

          .= (ii `11 ) by A73;

          then

           A91: [ii, g] in ( dom CC) by A25;



          hence (ii (*) g) = (the Comp of C . (ii,g)) by CAT_1:def 1

          .= (CC . (ii,g))

          .= [ [(g `11 ), (ii `12 )], F(`2,`2)] by A26, A91

          .= [ [b1, a1], f1] by A88, A89, A90, A85, A73

          .= g by A85;

        end;

      end;

      then

      reconsider C as strict Category by A31, A34, A43, A70;

      C is with_triple-like_morphisms

      proof

        let f be Morphism of C;

        f in M;

        then

        consider a,b be Element of A(), g be Element of B() such that

         A92: f = [ [a, b], g] and P[a, b, g];

        take g;



         A93: ( dom f) = (f `11 ) by A10

        .= a by A92, MCART_1: 85;

        ( cod f) = (f `12 ) by A11

        .= b by A92, MCART_1: 85;

        hence thesis by A92, A93;

      end;

      then

      reconsider C as with_triple-like_morphisms strict Category;

      take C;

      thus the carrier of C = A();

      hereby

        let a,b be Element of A(), f be Element of B();

        assume P[a, b, f];

        then [ [a, b], f] in M;

        hence [ [a, b], f] is Morphism of C;

      end;

      hereby

        let m be Morphism of C;

        m in M;

        hence ex a,b be Element of A(), f be Element of B() st m = [ [a, b], f] & P[a, b, f];

      end;

      let m1,m2 be Morphism of C, a1,a2,a3 be Element of A(), f1,f2 be Element of B();

      assume that

       A94: m1 = [ [a1, a2], f1] and

       A95: m2 = [ [a2, a3], f2];



       A96: (m1 `11 ) = a1 by A94, MCART_1: 85;



       A97: (m1 `12 ) = a2 by A94, MCART_1: 85;



       A98: (m2 `11 ) = a2 by A95, MCART_1: 85;



       A99: (m2 `12 ) = a3 by A95, MCART_1: 85;



      thus (m2 (*) m1) = (CC . (m2,m1)) by A25, A97, A98, CAT_1:def 1

      .= [ [a1, a3], F(`2,`2)] by A26, A96, A99, A25, A97, A98

      .= [ [a1, a3], F(f2,`2)] by A95

      .= [ [a1, a3], F(f2,f1)] by A94;

    end;

    scheme :: CAT_5:sch2

    CatUniq { A,B() -> non empty set , P[ set, set, set], F( set, set) -> set } :

for C1,C2 be strict with_triple-like_morphisms Category st the carrier of C1 = A() & (for a,b be Element of A(), f be Element of B() st P[a, b, f] holds [ [a, b], f] is Morphism of C1) & (for m be Morphism of C1 holds ex a,b be Element of A(), f be Element of B() st m = [ [a, b], f] & P[a, b, f]) & (for m1,m2 be Morphism of C1, a1,a2,a3 be Element of A(), f1,f2 be Element of B() st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)]) & the carrier of C2 = A() & (for a,b be Element of A(), f be Element of B() st P[a, b, f] holds [ [a, b], f] is Morphism of C2) & (for m be Morphism of C2 holds ex a,b be Element of A(), f be Element of B() st m = [ [a, b], f] & P[a, b, f]) & for m1,m2 be Morphism of C2, a1,a2,a3 be Element of A(), f1,f2 be Element of B() st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)] holds C1 = C2

      provided for a be Element of A() holds ex f be Element of B() st P[a, a, f] & for b be Element of A(), g be Element of B() holds (P[a, b, g] implies F(g,f) = g) & (P[b, a, g] implies F(f,g) = g);

      let C1,C2 be strict with_triple-like_morphisms Category such that

       A1: the carrier of C1 = A() and

       A2: for a,b be Element of A(), f be Element of B() st P[a, b, f] holds [ [a, b], f] is Morphism of C1 and

       A3: for m be Morphism of C1 holds ex a,b be Element of A(), f be Element of B() st m = [ [a, b], f] & P[a, b, f] and

       A4: for m1,m2 be Morphism of C1, a1,a2,a3 be Element of A(), f1,f2 be Element of B() st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)] and

       A5: the carrier of C2 = A() and

       A6: for a,b be Element of A(), f be Element of B() st P[a, b, f] holds [ [a, b], f] is Morphism of C2 and

       A7: for m be Morphism of C2 holds ex a,b be Element of A(), f be Element of B() st m = [ [a, b], f] & P[a, b, f] and

       A8: for m1,m2 be Morphism of C2, a1,a2,a3 be Element of A(), f1,f2 be Element of B() st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)];



       A9: the carrier' of C1 = the carrier' of C2

      proof

        hereby

          let x be object;

          assume x in the carrier' of C1;

          then ex a,b be Element of A(), f be Element of B() st x = [ [a, b], f] & P[a, b, f] by A3;

          then x is Morphism of C2 by A6;

          hence x in the carrier' of C2;

        end;

        let x be object;

        assume x in the carrier' of C2;

        then ex a,b be Element of A(), f be Element of B() st x = [ [a, b], f] & P[a, b, f] by A7;

        then x is Morphism of C1 by A2;

        hence thesis;

      end;



       A10: ( dom the Source of C1) = the carrier' of C1 by FUNCT_2:def 1;



       A11: ( dom the Source of C2) = the carrier' of C2 by FUNCT_2:def 1;



       A12: ( dom the Target of C1) = the carrier' of C1 by FUNCT_2:def 1;



       A13: ( dom the Target of C2) = the carrier' of C2 by FUNCT_2:def 1;

       A14:

      now

        let x be object;

        assume x in the carrier' of C1;

        then

        reconsider m1 = x as Morphism of C1;

        reconsider m2 = m1 as Morphism of C2 by A9;



        thus (the Source of C1 . x) = ( dom m1)

        .= (m1 `11 ) by Th2

        .= ( dom m2) by Th2

        .= (the Source of C2 . x);

      end;

      then

       A15: the Source of C1 = the Source of C2 by A9, A10, A11;

      now

        let x be object;

        assume x in the carrier' of C1;

        then

        reconsider m1 = x as Morphism of C1;

        reconsider m2 = m1 as Morphism of C2 by A9;



        thus (the Target of C1 . x) = ( cod m1)

        .= (m1 `12 ) by Th2

        .= ( cod m2) by Th2

        .= (the Target of C2 . x);

      end;

      then

       A16: the Target of C1 = the Target of C2 by A9, A12, A13;



       A17: ( dom the Comp of C1) = ( dom the Comp of C2)

      proof

        hereby

          let x be object;

          assume

           A18: x in ( dom the Comp of C1);

          then

          reconsider xx = x as Element of [:the carrier' of C1, the carrier' of C1:];

          reconsider y = xx as Element of [:the carrier' of C2, the carrier' of C2:] by A9;



           A19: y = [(xx `1 ), (xx `2 )] by MCART_1: 21;

          then ( dom (xx `1 )) = ( cod (xx `2 )) by A18, CAT_1:def 6;

          then ( dom (y `1 )) = ( cod (y `2 )) by A14, A16;

          hence x in ( dom the Comp of C2) by A19, CAT_1:def 6;

        end;

        let x be object;

        assume

         A20: x in ( dom the Comp of C2);

        then

        reconsider xx = x as Element of [:the carrier' of C1, the carrier' of C1:] by A9;

        reconsider y = xx as Element of [:the carrier' of C2, the carrier' of C2:] by A9;



         A21: xx = [(y `1 ), (y `2 )] by MCART_1: 21;

        then ( dom (y `1 )) = ( cod (y `2 )) by A20, CAT_1:def 6;

        then ( dom (xx `1 )) = ( cod (xx `2 )) by A14, A16;

        hence thesis by A21, CAT_1:def 6;

      end;

      now

        let x,y be object;

        assume

         A22: [x, y] in ( dom the Comp of C1);

        then

        reconsider g1 = x, h1 = y as Morphism of C1 by ZFMISC_1: 87;

        reconsider g2 = g1, h2 = h1 as Morphism of C2 by A9;

        consider a1,b1 be Element of A(), f1 be Element of B() such that

         A23: g1 = [ [a1, b1], f1] and P[a1, b1, f1] by A3;

        consider c1,d1 be Element of A(), i1 be Element of B() such that

         A24: h1 = [ [c1, d1], i1] and P[c1, d1, i1] by A3;



         A25: a1 = (g1 `11 ) by A23, MCART_1: 85

        .= ( dom g1) by Th2

        .= ( cod h1) by A22, CAT_1: 15

        .= (h1 `12 ) by Th2

        .= d1 by A24, MCART_1: 85;



        thus (the Comp of C1 . (x,y)) = (g1 (*) h1) by A22, CAT_1:def 1

        .= [ [c1, b1], F(f1,i1)] by A4, A23, A24, A25

        .= (g2 (*) h2) by A8, A23, A24, A25

        .= (the Comp of C2 . (x,y)) by A17, A22, CAT_1:def 1;

      end;

      hence thesis by A1, A5, A9, A15, A16, A17, BINOP_1: 20;

    end;

    scheme :: CAT_5:sch3

    FunctorEx { A,B() -> Category , O( set) -> Object of B() , F( object) -> object } :

ex F be Functor of A(), B() st for f be Morphism of A() holds (F . f) = F(f)

      provided

       A1: for f be Morphism of A() holds F(f) is Morphism of B() & for g be Morphism of B() st g = F(f) holds ( dom g) = O(dom) & ( cod g) = O(cod)

       and

       A2: for a be Object of A() holds F(id) = ( id O(a))

       and

       A3: for f1,f2 be Morphism of A() holds for g1,g2 be Morphism of B() st g1 = F(f1) & g2 = F(f2) & ( dom f2) = ( cod f1) holds F((*)) = (g2 (*) g1);

      consider F be Function such that

       A4: ( dom F) = the carrier' of A() and

       A5: for x be object st x in the carrier' of A() holds (F . x) = F(x) from FUNCT_1:sch 3;

      ( rng F) c= the carrier' of B()

      proof

        let x be object;

        assume x in ( rng F);

        then

        consider y be object such that

         A6: y in ( dom F) and

         A7: x = (F . y) by FUNCT_1:def 3;

        x = F(y) by A4, A5, A6, A7;

        then x is Morphism of B() by A1, A4, A6;

        hence thesis;

      end;

      then

      reconsider F as Function of the carrier' of A(), the carrier' of B() by A4, FUNCT_2:def 1, RELSET_1: 4;

       A8:

      now

        let c be Object of A();

        take d = O(c);



        thus (F . ( id c)) = F(id) by A5

        .= ( id d) by A2;

      end;

       A9:

      now

        let f be Morphism of A();

        reconsider g = F(f) as Morphism of B() by A1;



        thus (F . ( id ( dom f))) = F(id) by A5

        .= ( id O(dom)) by A2

        .= ( id ( dom g)) by A1

        .= ( id ( dom (F . f))) by A5;



        thus (F . ( id ( cod f))) = F(id) by A5

        .= ( id O(cod)) by A2

        .= ( id ( cod g)) by A1

        .= ( id ( cod (F . f))) by A5;

      end;

      now

        let f,g be Morphism of A();

        assume

         A10: ( dom g) = ( cod f);



         A11: (F . g) = F(g) by A5;



         A12: (F . f) = F(f) by A5;

        (F . (g (*) f)) = F((*)) by A5;

        hence (F . (g (*) f)) = ((F . g) (*) (F . f)) by A3, A10, A11, A12;

      end;

      then

      reconsider F as Functor of A(), B() by A8, A9, CAT_1: 61;

      take F;

      thus thesis by A5;

    end;

    theorem :: CAT_5:3



     Th3: for C1 be Category, C2 be Subcategory of C1 st C1 is Subcategory of C2 holds the CatStr of C1 = the CatStr of C2

    proof

      let C1 be Category, C2 be Subcategory of C1;

      assume

       A1: C1 is Subcategory of C2;

      then

       A2: the carrier of C1 c= the carrier of C2 by CAT_2:def 4;

      the carrier of C2 c= the carrier of C1 by CAT_2:def 4;

      then

       A3: the carrier of C1 = the carrier of C2 by A2;



       A4: the carrier' of C1 c= the carrier' of C2 by A1, CAT_2: 7;

      the carrier' of C2 c= the carrier' of C1 by CAT_2: 7;

      then

       A5: the carrier' of C1 = the carrier' of C2 by A4;



       A6: the Comp of C1 c= the Comp of C2 by A1, CAT_2:def 4;

      the Comp of C2 c= the Comp of C1 by CAT_2:def 4;

      then

       A7: the Comp of C1 = the Comp of C2 by A6;

      now

        let m1 be Morphism of C1;

        reconsider m2 = m1 as Morphism of C2 by A4;



        thus (the Source of C1 . m1) = ( dom m1)

        .= ( dom m2) by CAT_2: 9

        .= (the Source of C2 . m1);

      end;

      then

       A8: the Source of C1 = the Source of C2 by A3, A5, FUNCT_2: 63;

      now

        let m1 be Morphism of C1;

        reconsider m2 = m1 as Morphism of C2 by A4;



        thus (the Target of C1 . m1) = ( cod m1)

        .= ( cod m2) by CAT_2: 9

        .= (the Target of C2 . m1);

      end;

      then the Target of C1 = the Target of C2 by A3, A5, FUNCT_2: 63;

      hence thesis by A3, A5, A7, A8;

    end;

    theorem :: CAT_5:4



     Th4: for C be Category, D be Subcategory of C, E be Subcategory of D holds E is Subcategory of C

    proof

      let C be Category, D be Subcategory of C, E be Subcategory of D;



       A1: the carrier of D c= the carrier of C by CAT_2:def 4;



       A2: the Comp of D c= the Comp of C by CAT_2:def 4;



       A3: the carrier of E c= the carrier of D by CAT_2:def 4;



       A4: the Comp of E c= the Comp of D by CAT_2:def 4;

      thus the carrier of E c= the carrier of C by A1, A3;

      hereby

        let a,b be Object of E, a9,b9 be Object of C;

        reconsider a1 = a, b1 = b as Object of D by CAT_2: 6;

        assume that

         A5: a = a9 and

         A6: b = b9;



         A7: ( Hom (a,b)) c= ( Hom (a1,b1)) by CAT_2:def 4;

        ( Hom (a1,b1)) c= ( Hom (a9,b9)) by A5, A6, CAT_2:def 4;

        hence ( Hom (a,b)) c= ( Hom (a9,b9)) by A7;

      end;

      thus the Comp of E c= the Comp of C by A2, A4;

      let a be Object of E, a9 be Object of C;

      reconsider a1 = a as Object of D by CAT_2: 6;

      assume

       A8: a = a9;

      ( id a) = ( id a1) by CAT_2:def 4;

      hence thesis by A8, CAT_2:def 4;

    end;

    definition

      let C1,C2 be Category;

      given C be Category such that

       A1: C1 is Subcategory of C and

       A2: C2 is Subcategory of C;

      given o1 be Object of C1 such that

       A3: o1 is Object of C2;

      :: CAT_5:def2

      func C1 /\ C2 -> strict Category means

      : Def2: the carrier of it = (the carrier of C1 /\ the carrier of C2) & the carrier' of it = (the carrier' of C1 /\ the carrier' of C2) & the Source of it = (the Source of C1 | the carrier' of C2) & the Target of it = (the Target of C1 | the carrier' of C2) & the Comp of it = (the Comp of C1 || the carrier' of C2);

      existence

      proof

        set DD = (the Source of C1 | the carrier' of C2);

        set CC = (the Target of C1 | the carrier' of C2);

        set Cm = (the Comp of C1 || the carrier' of C2);

        reconsider O = (the carrier of C1 /\ the carrier of C2) as non empty set by A3, XBOOLE_0:def 4;

        reconsider o2 = o1 as Object of C2 by A3;

        reconsider o = o1 as Object of C by A1, CAT_2: 6;



         A4: ( id o1) = ( id o) by A1, CAT_2:def 4;

        ( id o2) = ( id o) by A2, CAT_2:def 4;

        then

        reconsider M = (the carrier' of C1 /\ the carrier' of C2) as non empty set by A4, XBOOLE_0:def 4;



         A5: ( dom the Source of C1) = the carrier' of C1 by FUNCT_2:def 1;



         A6: ( dom the Target of C1) = the carrier' of C1 by FUNCT_2:def 1;



         A7: ( dom DD) = M by A5, RELAT_1: 61;



         A8: ( dom CC) = M by A6, RELAT_1: 61;

        ( rng DD) c= O

        proof

          let x be object;

          assume x in ( rng DD);

          then

          consider m be object such that

           A9: m in ( dom DD) and

           A10: x = (DD . m) by FUNCT_1:def 3;

          reconsider m1 = m as Morphism of C1 by A9;

          reconsider m2 = m as Morphism of C2 by A7, A9, XBOOLE_0:def 4;

          reconsider m = m1 as Morphism of C by A1, CAT_2: 8;



           A11: x = ( dom m1) by A9, A10, FUNCT_1: 47;



           A12: ( dom m1) = ( dom m) by A1, CAT_2: 9;

          ( dom m) = ( dom m2) by A2, CAT_2: 9;

          hence thesis by A11, A12, XBOOLE_0:def 4;

        end;

        then

        reconsider DD as Function of M, O by A7, FUNCT_2:def 1, RELSET_1: 4;

        ( rng CC) c= O

        proof

          let x be object;

          assume x in ( rng CC);

          then

          consider m be object such that

           A13: m in ( dom CC) and

           A14: x = (CC . m) by FUNCT_1:def 3;

          reconsider m1 = m as Morphism of C1 by A13;

          reconsider m2 = m as Morphism of C2 by A8, A13, XBOOLE_0:def 4;

          reconsider m = m1 as Morphism of C by A1, CAT_2: 8;



           A15: x = ( cod m1) by A13, A14, FUNCT_1: 47;



           A16: ( cod m1) = ( cod m) by A1, CAT_2: 9;

          ( cod m) = ( cod m2) by A2, CAT_2: 9;

          hence thesis by A15, A16, XBOOLE_0:def 4;

        end;

        then

        reconsider CC as Function of M, O by A8, FUNCT_2:def 1, RELSET_1: 4;



         A17: ( dom Cm) = (( dom the Comp of C1) /\ [:the carrier' of C2, the carrier' of C2:]) by RELAT_1: 61;

        then ( dom Cm) c= ( [:the carrier' of C1, the carrier' of C1:] /\ [:the carrier' of C2, the carrier' of C2:]) by XBOOLE_1: 26;

        then

         A18: ( dom Cm) c= [:M, M:] by ZFMISC_1: 100;

        ( rng Cm) c= M

        proof

          let x be object;

          assume x in ( rng Cm);

          then

          consider m be object such that

           A19: m in ( dom Cm) and

           A20: x = (Cm . m) by FUNCT_1:def 3;



           A21: (m `1 ) in M by A18, A19, MCART_1: 10;



           A22: (m `2 ) in M by A18, A19, MCART_1: 10;



           A23: m = [(m `1 ), (m `2 )] by A17, A19, MCART_1: 21;

          reconsider m1 = (m `1 ), m2 = (m `2 ) as Morphism of C1 by A21, A22, XBOOLE_0:def 4;

          reconsider n1 = (m `1 ), n2 = (m `2 ) as Morphism of C2 by A21, A22, XBOOLE_0:def 4;

          reconsider mm = m1, n = m2 as Morphism of C by A1, CAT_2: 8;



           A24: m in ( dom the Comp of C1) by A17, A19, XBOOLE_0:def 4;

          then

           A25: ( dom m1) = ( cod m2) by A23, CAT_1: 15;



           A26: x = (the Comp of C1 . (m1,m2)) by A19, A20, A23, FUNCT_1: 47;



           A27: ( dom m1) = ( dom mm) by A1, CAT_2: 9;



           A28: ( dom n1) = ( dom mm) by A2, CAT_2: 9;



           A29: ( cod m2) = ( cod n) by A1, CAT_2: 9;



           A30: ( cod n2) = ( cod n) by A2, CAT_2: 9;



           A31: x = (m1 (*) m2) by A23, A24, A26, CAT_1:def 1;



           A32: (m1 (*) m2) = (mm (*) n) by A1, A25, CAT_2: 11;

          (mm (*) n) = (n1 (*) n2) by A2, A25, A27, A28, A29, A30, CAT_2: 11;

          hence thesis by A31, A32, XBOOLE_0:def 4;

        end;

        then

        reconsider Cm as PartFunc of [:M, M:], M by A18, RELSET_1: 4;

        set CAT = CatStr (# O, M, DD, CC, Cm #);



         A33: CAT is Category-like

        proof

          let f,g be Morphism of CAT;

          reconsider g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def 4;



           A34: g in the carrier' of C2 by XBOOLE_0:def 4;



           A35: f in the carrier' of C2 by XBOOLE_0:def 4;

          hereby

            assume [g, f] in ( dom the Comp of CAT);

            then

             A36: [g, f] in ( dom the Comp of C1) by A17, XBOOLE_0:def 4;



            thus ( dom g) = ( dom g9) by A34, FUNCT_1: 49

            .= ( cod f9) by A36, CAT_1:def 6

            .= ( cod f) by A35, FUNCT_1: 49;

          end;

          assume

           A37: ( dom g) = ( cod f);



           A38: ( dom g) = ( dom g9) by A7, FUNCT_1: 47;



           A39: ( dom g) = ( cod f9) by A8, A37, FUNCT_1: 47;



           A40: [g, f] in [:the carrier' of C2, the carrier' of C2:] by A34, A35, ZFMISC_1: 87;

           [g, f] in ( dom the Comp of C1) by A38, A39, CAT_1:def 6;

          hence [g, f] in ( dom the Comp of CAT) by A17, A40, XBOOLE_0:def 4;

        end;



         A41: for f,g be Morphism of CAT holds [g, f] in ( dom the Comp of CAT) iff ( dom g) = ( cod f) by A33;



         A42: CAT is transitive

        proof

          let f,g be Morphism of CAT;

          reconsider g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def 4;

          assume

           A43: ( dom g) = ( cod f);

          then

           A44: [g, f] in ( dom the Comp of CAT) by A41;



           A45: ( dom the Comp of CAT) c= ( dom the Comp of C1) by RELAT_1: 60;

          reconsider h = (g (*) f) as Morphism of CAT;

          reconsider h9 = h as Morphism of C1 by XBOOLE_0:def 4;



           A46: h = (the Comp of CAT . (g,f)) by A44, CAT_1:def 1

          .= (the Comp of C1 . (g9,f9)) by A44, FUNCT_1: 47

          .= (g9 (*) f9) by A45, A44, CAT_1:def 1;



           A47: ( dom f) = ( dom f9) by A7, FUNCT_1: 47;



           A48: ( dom g) = ( dom g9) by A7, FUNCT_1: 47;



           A49: ( dom h) = ( dom h9) by A7, FUNCT_1: 47;



           A50: ( cod f) = ( cod f9) by A8, FUNCT_1: 47;



           A51: ( cod g) = ( cod g9) by A8, FUNCT_1: 47;



           A52: ( cod h) = ( cod h9) by A8, FUNCT_1: 47;

          thus ( dom (g (*) f)) = ( dom f) by A43, A47, A48, A49, A50, A46, CAT_1:def 7;

          thus ( cod (g (*) f)) = ( cod g) by A43, A46, A48, A50, A51, A52, CAT_1:def 7;

        end;



         A53: for f,g be Morphism of CAT st ( dom g) = ( cod f) holds ( dom (g (*) f)) = ( dom f) & ( cod (g (*) f)) = ( cod g) by A42;



         A54: CAT is associative

        proof

          let f,g,h be Morphism of CAT;

          reconsider h9 = h, g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def 4;

          assume that

           A55: ( dom h) = ( cod g) and

           A56: ( dom g) = ( cod f);



           A57: [h, g] in ( dom the Comp of CAT) by A41, A55;



           A58: [g, f] in ( dom the Comp of CAT) by A41, A56;

          then

          reconsider hg = (the Comp of CAT . (h,g)), gf = (the Comp of CAT . (g,f)) as Morphism of CAT by A57, PARTFUN1: 4;

          reconsider hg9 = hg, gf9 = gf as Morphism of C1 by XBOOLE_0:def 4;



           A59: ( dom hg) = ( dom (h (*) g)) by A57, CAT_1:def 1

          .= ( dom g) by A53, A55;



           A60: ( cod gf) = ( cod (g (*) f)) by A58, CAT_1:def 1

          .= ( cod g) by A53, A56;



           A61: [hg, f] in ( dom the Comp of CAT) by A41, A56, A59;



           A62: [h, gf] in ( dom the Comp of CAT) by A41, A55, A60;



           A63: ( dom h9) = ( dom h) by A7, FUNCT_1: 47;



           A64: ( cod g9) = ( cod g) by A8, FUNCT_1: 47;

          then

           A65: (h9 (*) g9) = (the Comp of C1 . (h9,g9)) by A63, A55, CAT_1: 16;



           A66: ( dom g9) = ( dom g) by A7, FUNCT_1: 47;



           A67: ( cod f9) = ( cod f) by A8, FUNCT_1: 47;

          then

           A68: (g9 (*) f9) = (the Comp of C1 . (g9,f9)) by A66, A56, CAT_1: 16;



           A69: ( cod (g9 (*) f9)) = ( cod g9) by A56, A66, A67, CAT_1:def 7;



           A70: ( dom (h9 (*) g9)) = ( dom g9) by A55, A63, A64, CAT_1:def 7;



           A71: hg = (h (*) g) by A57, CAT_1:def 1;

          gf = (g (*) f) by A58, CAT_1:def 1;



          hence (h (*) (g (*) f)) = (the Comp of CAT . (h,(the Comp of CAT . (g,f)))) by A62, CAT_1:def 1

          .= (the Comp of C1 . [h9, gf9]) by A62, FUNCT_1: 47

          .= (the Comp of C1 . (h9,(the Comp of C1 . (g9,f9)))) by A58, FUNCT_1: 47

          .= (h9 (*) (g9 (*) f9)) by A69, A68, A55, A63, A64, CAT_1: 16

          .= ((h9 (*) g9) (*) f9) by A55, A56, A63, A64, A66, A67, CAT_1:def 8

          .= (the Comp of C1 . ((the Comp of C1 . (h9,g9)),f9)) by A70, A65, A56, A66, A67, CAT_1: 16

          .= (the Comp of C1 . [hg9, f9]) by A57, FUNCT_1: 47

          .= (the Comp of CAT . ((the Comp of CAT . (h,g)),f)) by A61, FUNCT_1: 47

          .= ((h (*) g) (*) f) by A71, A61, CAT_1:def 1;

        end;



         A72: CAT is reflexive

        proof

          let b be Object of CAT;

          reconsider b1 = b as Object of C1 by XBOOLE_0:def 4;

          reconsider b2 = b as Object of C2 by XBOOLE_0:def 4;



           A73: the carrier of C1 c= the carrier of C by A1, CAT_2:def 4;

          reconsider bb = b1 as Object of C by A73;



           A74: ( id b1) = ( id bb) by A1, CAT_2:def 4

          .= ( id b2) by A2, CAT_2:def 4;

          ( id b2) in (the carrier' of C1 /\ the carrier' of C2) by A74, XBOOLE_0:def 4;

          then ( id b2) in M;

          then

          reconsider ii = ( id b2) as Morphism of CAT;



           A75: ( dom ii) = ( dom ( id b1)) by A74, FUNCT_1: 49

          .= b;

          ( cod ii) = ( cod ( id b1)) by A74, FUNCT_1: 49

          .= b;

          then ii in ( Hom (b,b)) by A75;

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

        end;

        CAT is with_identities

        proof

          let a be Element of CAT;

          reconsider a1 = a as Object of C1 by XBOOLE_0:def 4;

          reconsider a2 = a as Object of C2 by XBOOLE_0:def 4;



           A76: the carrier of C1 c= the carrier of C by A1, CAT_2:def 4;

          reconsider aa = a1 as Object of C by A76;



           A77: ( id a1) = ( id aa) by A1, CAT_2:def 4

          .= ( id a2) by A2, CAT_2:def 4;

          ( id a2) in (the carrier' of C1 /\ the carrier' of C2) by A77, XBOOLE_0:def 4;

          then ( id a2) in M;

          then

          reconsider ii = ( id a2) as Morphism of CAT;



           A78: ( dom ii) = ( dom ( id a1)) by A77, FUNCT_1: 49

          .= a;

          ( cod ii) = ( cod ( id a1)) by A77, FUNCT_1: 49

          .= a;

          then ii in ( Hom (a,a)) by A78;

          then

          reconsider ii as Morphism of a, a by CAT_1:def 5;

          take ii;

          let b be Element of CAT;

          thus ( Hom (a,b)) <> {} implies for g be Morphism of a, b holds (g (*) ii) = g

          proof

            assume

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

            let g be Morphism of a, b;

            g in the carrier' of C1 by XBOOLE_0:def 4;

            then

            reconsider gg = g as Morphism of C1;



             A80: g in the carrier' of C2 by XBOOLE_0:def 4;



             A81: ( dom gg) = (the Source of C1 . g)

            .= ((the Source of C1 | the carrier' of C2) . g) by A80, FUNCT_1: 49

            .= ( dom g)

            .= a1 by A79, CAT_1: 5;



             A82: ( cod ( id a1)) = a1;

            ( cod ii) = ( cod ( id a1)) by A77, FUNCT_1: 49

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

            then

             A83: [g, ii] in ( dom the Comp of CAT) by A33;



            hence (g (*) ii) = (Cm . (g,ii)) by CAT_1:def 1

            .= ((the Comp of C1 || the carrier' of C2) . (g,ii))

            .= (the Comp of C1 . (gg,( id a1))) by A77, A83, FUNCT_1: 47

            .= (gg (*) ( id a1)) by A82, A81, CAT_1: 16

            .= g by A81, CAT_1: 22;

          end;

          assume

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

          let g be Morphism of b, a;

          g in the carrier' of C1 by XBOOLE_0:def 4;

          then

          reconsider gg = g as Morphism of C1;



           A85: g in the carrier' of C2 by XBOOLE_0:def 4;



           A86: ( cod gg) = (the Target of C1 . g)

          .= ((the Target of C1 | the carrier' of C2) . g) by A85, FUNCT_1: 49

          .= ( cod g)

          .= a1 by A84, CAT_1: 5;



           A87: ( dom ( id a1)) = a1;

          ( dom ii) = ( dom ( id a1)) by A77, FUNCT_1: 49

          .= ( cod g) by A84, CAT_1: 5;

          then

           A88: [ii, g] in ( dom the Comp of CAT) by A33;



          hence (ii (*) g) = (Cm . (ii,g)) by CAT_1:def 1

          .= ((the Comp of C1 || the carrier' of C2) . (ii,g))

          .= (the Comp of C1 . (( id a1),gg)) by A77, A88, FUNCT_1: 47

          .= (( id a1) (*) gg) by A87, A86, CAT_1: 16

          .= g by A86, CAT_1: 21;

        end;

        hence thesis by A33, A42, A54, A72;

      end;

      uniqueness ;

    end

    reserve C for Category,

C1,C2 for Subcategory of C;

    theorem :: CAT_5:5



     Th5: the carrier of C1 meets the carrier of C2 implies (C1 /\ C2) = (C2 /\ C1)

    proof

      assume (the carrier of C1 /\ the carrier of C2) <> {} ;

      then

      reconsider O = (the carrier of C1 /\ the carrier of C2) as non empty set;

      set o = the Element of O;

      set C12 = (C1 /\ C2), C21 = (C2 /\ C1);

      set M1 = the carrier' of C1, M2 = the carrier' of C2;

      set O1 = the carrier of C1, O2 = the carrier of C2;



       A1: o is Object of C1 by XBOOLE_0:def 4;



       A2: o is Object of C2 by XBOOLE_0:def 4;

      then

       A3: the carrier of C12 = O by A1, Def2;



       A4: the carrier of C21 = O by A1, A2, Def2;



       A5: the carrier' of C12 = (the carrier' of C1 /\ the carrier' of C2) by A1, A2, Def2;



       A6: the Source of C21 = (the Source of C2 | M1) by A1, A2, Def2;



       A7: the Source of C12 = (the Source of C1 | M2) by A1, A2, Def2;



       A8: the Target of C21 = (the Target of C2 | M1) by A1, A2, Def2;



       A9: the Target of C12 = (the Target of C1 | M2) by A1, A2, Def2;



       A10: the Comp of C21 = (the Comp of C2 || M1) by A1, A2, Def2;



       A11: the Comp of C12 = (the Comp of C1 || M2) by A1, A2, Def2;



       A12: the Source of C1 = (the Source of C | M1) by NATTRA_1: 8;



       A13: the Target of C1 = (the Target of C | M1) by NATTRA_1: 8;



       A14: the Source of C2 = (the Source of C | M2) by NATTRA_1: 8;



       A15: the Target of C2 = (the Target of C | M2) by NATTRA_1: 8;



       A16: the Source of C12 = (the Source of C | (M1 /\ M2)) by A7, A12, RELAT_1: 71

      .= the Source of C21 by A6, A14, RELAT_1: 71;



       A17: the Target of C12 = (the Target of C | (M1 /\ M2)) by A9, A13, RELAT_1: 71

      .= the Target of C21 by A8, A15, RELAT_1: 71;

      the Comp of C12 = ((the Comp of C || M1) || M2) by A11, NATTRA_1: 8

      .= (the Comp of C | ( [:M1, M1:] /\ [:M2, M2:])) by RELAT_1: 71

      .= ((the Comp of C || M2) || M1) by RELAT_1: 71

      .= the Comp of C21 by A10, NATTRA_1: 8;

      hence thesis by A1, A2, A3, A4, A5, A16, A17, Def2;

    end;

    theorem :: CAT_5:6



     Th6: the carrier of C1 meets the carrier of C2 implies (C1 /\ C2) is Subcategory of C1 & (C1 /\ C2) is Subcategory of C2

    proof

      assume

       A1: the carrier of C1 meets the carrier of C2;

      then

       A2: (the carrier of C1 /\ the carrier of C2) <> {} ;



       A3: (C1 /\ C2) = (C2 /\ C1) by A1, Th5;

      now

        let C1,C2 be Subcategory of C;

        assume

         A4: (the carrier of C1 /\ the carrier of C2) <> {} ;



         A5: (the carrier of C1 /\ the carrier of C2) c= the carrier of C1 by XBOOLE_1: 17;



         A6: (the carrier' of C1 /\ the carrier' of C2) c= the carrier' of C1 by XBOOLE_1: 17;

        reconsider O = (the carrier of C1 /\ the carrier of C2) as non empty set by A4;

        set o = the Element of O;



         A7: o is Object of C1 by XBOOLE_0:def 4;



         A8: o is Object of C2 by XBOOLE_0:def 4;

        then

         A9: the carrier of (C1 /\ C2) = (the carrier of C1 /\ the carrier of C2) by A7, Def2;



         A10: the carrier' of (C1 /\ C2) = (the carrier' of C1 /\ the carrier' of C2) by A7, A8, Def2;



         A11: the Source of (C1 /\ C2) = (the Source of C1 | the carrier' of C2) by A7, A8, Def2;



         A12: the Target of (C1 /\ C2) = (the Target of C1 | the carrier' of C2) by A7, A8, Def2;



         A13: the Comp of (C1 /\ C2) = (the Comp of C1 || the carrier' of C2) by A7, A8, Def2;



         A14: the Source of C1 = (the Source of C1 | ( dom the Source of C1));

        ( dom the Source of C1) = the carrier' of C1 by FUNCT_2:def 1;

        then

         A15: the Source of (C1 /\ C2) = (the Source of C1 | the carrier' of (C1 /\ C2)) by A10, A11, A14, RELAT_1: 71;



         A16: the Target of C1 = (the Target of C1 | ( dom the Target of C1));

        ( dom the Target of C1) = the carrier' of C1 by FUNCT_2:def 1;

        then

         A17: the Target of (C1 /\ C2) = (the Target of C1 | the carrier' of (C1 /\ C2)) by A10, A12, A16, RELAT_1: 71;



         A18: for o be Element of C1 st o in O holds ( id o) in (the carrier' of C1 /\ the carrier' of C2)

        proof

          let o1 be Element of C1;

          assume o1 in O;

          then

          reconsider o2 = o1 as Element of C2 by XBOOLE_0:def 4;



           A19: the carrier of C1 c= the carrier of C by CAT_2:def 4;

          reconsider o = o1 as Element of C by A19;



           A20: ( id o1) = ( id o) by CAT_2:def 4;

          ( id o2) = ( id o) by CAT_2:def 4;

          hence ( id o1) in (the carrier' of C1 /\ the carrier' of C2) by A20, XBOOLE_0:def 4;

        end;

        the Comp of C1 = (the Comp of C1 || the carrier' of C1);

        then the Comp of (C1 /\ C2) = (the Comp of C1 | ( [:the carrier' of C1, the carrier' of C1:] /\ [:the carrier' of C2, the carrier' of C2:])) by A13, RELAT_1: 71;

        then the Comp of (C1 /\ C2) = (the Comp of C1 || the carrier' of (C1 /\ C2)) by A10, ZFMISC_1: 100;

        hence (C1 /\ C2) is Subcategory of C1 by A5, A6, A9, A10, A15, A17, A18, NATTRA_1: 9;

      end;

      hence thesis by A2, A3;

    end;

    definition

      let C,D be Category;

      let F be Functor of C, D;

      :: CAT_5:def3

      func Image F -> strict Subcategory of D means

      : Def3: the carrier of it = ( rng ( Obj F)) & ( rng F) c= the carrier' of it & for E be Subcategory of D st the carrier of E = ( rng ( Obj F)) & ( rng F) c= the carrier' of E holds it is Subcategory of E;

      existence

      proof

        set a = the Object of C;



         A1: ( dom ( Obj F)) = the carrier of C by FUNCT_2:def 1;

        then (( Obj F) . a) in ( rng ( Obj F)) by FUNCT_1:def 3;

        then

        reconsider O = ( rng ( Obj F)) as non empty set;

        reconsider O as non empty Subset of the carrier of D;

        set f = the Morphism of C;



         A2: ( dom F) = the carrier' of C by FUNCT_2:def 1;



         A3: ( dom the Source of D) = the carrier' of D by FUNCT_2:def 1;



         A4: ( dom the Target of D) = the carrier' of D by FUNCT_2:def 1;

        defpred P[ set] means ( rng F) c= $1 & ex E be Subcategory of D st the carrier of E = O & the carrier' of E = $1;

        consider MM be set such that

         A5: for x be set holds x in MM iff x in ( bool the carrier' of D) & P[x] from XFAMILY:sch 1;

        set HH = { ( Hom (a0,b)) where a0 be Object of D, b be Object of D : a0 in O & b in O };

        reconsider M0 = ( union HH) as non empty Subset of the carrier' of D by CAT_2: 19;

        reconsider D0 = (the Source of D | M0), C0 = (the Target of D | M0) as Function of M0, O by CAT_2: 20;

        reconsider CC = (the Comp of D || M0) as PartFunc of [:M0, M0:], M0 by CAT_2: 20;

         CatStr (# O, M0, D0, C0, CC #) is full Subcategory of D by CAT_2: 21;

        then

         A6: CatStr (# O, M0, D0, C0, CC #) is Subcategory of D;

        ( rng F) c= M0

        proof

          let y be object;

          assume y in ( rng F);

          then

          consider x be object such that

           A7: x in ( dom F) and

           A8: y = (F . x) by FUNCT_1:def 3;

          reconsider x as Morphism of C by A7;



           A9: (( Obj F) . ( dom x)) in O by A1, FUNCT_1:def 3;



           A10: (( Obj F) . ( cod x)) in O by A1, FUNCT_1:def 3;



           A11: ( dom (F . x)) in O by A9, CAT_1: 69;



           A12: ( cod (F . x)) in O by A10, CAT_1: 69;



           A13: y in ( Hom (( dom (F . x)),( cod (F . x)))) by A8;

          ( Hom (( dom (F . x)),( cod (F . x)))) in HH by A11, A12;

          hence thesis by A13, TARSKI:def 4;

        end;

        then

         A14: M0 in MM by A5, A6;

        set M = ( meet MM);



         A15: for Z be set st Z in MM holds ( rng F) c= Z by A5;

        now

          let X be set;

          assume X in MM;

          then

           A16: ( rng F) c= X by A5;

          (F . f) in ( rng F) by A2, FUNCT_1:def 3;

          hence (F . f) in X by A16;

        end;

        then

        reconsider M as non empty set by A14, SETFAM_1:def 1;

        M c= the carrier' of D

        proof

          let x be object;

          assume x in M;

          then x in M0 by A14, SETFAM_1:def 1;

          hence thesis;

        end;

        then

        reconsider M as non empty Subset of the carrier' of D;

        set DOM = (the Source of D | M);

        set COD = (the Target of D | M);

        set COMP = (the Comp of D || M);



         A17: ( dom DOM) = M by A3, RELAT_1: 62;

        ( rng DOM) c= O

        proof

          let y be object;

          assume y in ( rng DOM);

          then

          consider x be object such that

           A18: x in M and

           A19: y = (DOM . x) by A17, FUNCT_1:def 3;

          reconsider x as Morphism of D by A18;

          x in M0 by A14, A18, SETFAM_1:def 1;

          then

          consider X be set such that

           A20: x in X and

           A21: X in HH by TARSKI:def 4;

          consider a,b be Object of D such that

           A22: X = ( Hom (a,b)) and

           A23: a in O and b in O by A21;

          ( dom x) = a by A20, A22, CAT_1: 1;

          hence thesis by A17, A18, A19, A23, FUNCT_1: 47;

        end;

        then

        reconsider DOM as Function of M, O by A17, FUNCT_2:def 1, RELSET_1: 4;



         A24: ( dom COD) = M by A4, RELAT_1: 62;

        ( rng COD) c= O

        proof

          let y be object;

          assume y in ( rng COD);

          then

          consider x be object such that

           A25: x in M and

           A26: y = (COD . x) by A24, FUNCT_1:def 3;

          reconsider x as Morphism of D by A25;

          x in M0 by A14, A25, SETFAM_1:def 1;

          then

          consider X be set such that

           A27: x in X and

           A28: X in HH by TARSKI:def 4;

          consider a,b be Object of D such that

           A29: X = ( Hom (a,b)) and a in O and

           A30: b in O by A28;

          ( cod x) = b by A27, A29, CAT_1: 1;

          hence thesis by A24, A25, A26, A30, FUNCT_1: 47;

        end;

        then

        reconsider COD as Function of M, O by A24, FUNCT_2:def 1, RELSET_1: 4;



         A31: ( dom COMP) c= [:M, M:] by RELAT_1: 58;

        ( rng COMP) c= M

        proof

          let y be object;

          assume y in ( rng COMP);

          then

          consider x be object such that

           A32: x in ( dom COMP) and

           A33: y = (COMP . x) by FUNCT_1:def 3;

          reconsider x1 = (x `1 ), x2 = (x `2 ) as Element of M by A31, A32, MCART_1: 10;



           A34: x = [x1, x2] by A31, A32, MCART_1: 21;

          now

            let X be set;

            assume

             A35: X in MM;

            then

            consider E be Subcategory of D such that the carrier of E = O and

             A36: the carrier' of E = X by A5;

            reconsider y1 = x1, y2 = x2 as Morphism of E by A35, A36, SETFAM_1:def 1;

            ( dom COMP) = (( dom the Comp of D) /\ [:M, M:]) by RELAT_1: 61;

            then x in ( dom the Comp of D) by A32, XBOOLE_0:def 4;

            then

             A37: ( dom x1) = ( cod x2) by A34, CAT_1: 15;



             A38: ( dom y1) = ( dom x1) by CAT_2: 9;

            ( cod y2) = ( cod x2) by CAT_2: 9;

            then

             A39: x in ( dom the Comp of E) by A34, A37, A38, CAT_1: 15;

            the Comp of E c= the Comp of D by CAT_2:def 4;



            then (the Comp of E . x) = (the Comp of D . x) by A39, GRFUNC_1: 2

            .= y by A32, A33, FUNCT_1: 47;

            then y in ( rng the Comp of E) by A39, FUNCT_1:def 3;

            hence y in X by A36;

          end;

          hence thesis by A14, SETFAM_1:def 1;

        end;

        then

        reconsider COMP as PartFunc of [:M, M:], M by A31, RELSET_1: 4;

        for o be Element of D st o in O holds ( id o) in M

        proof

          let o be Element of D;

          assume

           A40: o in O;

          for X be set st X in MM holds ( id o) in X

          proof

            let X be set;

            assume X in MM;

            then P[X] by A5;

            then

            consider E be Subcategory of D such that

             A41: the carrier of E = O and

             A42: the carrier' of E = X;

            o in the carrier of E by A40, A41;

            then

            reconsider oo = o as Element of E;

            ( id oo) = ( id o) by CAT_2:def 4;

            hence ( id o) in X by A42;

          end;

          hence ( id o) in M by A14, SETFAM_1:def 1;

        end;

        then

        reconsider T = CatStr (# O, M, DOM, COD, COMP #) as strict Subcategory of D by NATTRA_1: 9;

        take T;

        thus the carrier of T = ( rng ( Obj F)) & ( rng F) c= the carrier' of T by A14, A15, SETFAM_1: 5;

        let E be Subcategory of D;

        assume that

         A43: the carrier of E = ( rng ( Obj F)) and

         A44: ( rng F) c= the carrier' of E;

        thus the carrier of T c= the carrier of E by A43;

        the carrier' of E c= the carrier' of D by CAT_2: 7;

        then the carrier' of E in MM by A5, A43, A44;

        then

         A45: M c= the carrier' of E by SETFAM_1: 3;

        hereby

          let a,b be Object of T, a9,b9 be Object of E;

          assume that

           A46: a = a9 and

           A47: b = b9;

          thus ( Hom (a,b)) c= ( Hom (a9,b9))

          proof

            let x be object;

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

            then

            consider f be Morphism of T such that

             A48: x = f and

             A49: ( dom f) = a and

             A50: ( cod f) = b;

            reconsider g = f as Morphism of D by TARSKI:def 3;

            reconsider f as Morphism of E by A45;



             A51: ( dom g) = a by A49, CAT_2: 9;



             A52: ( cod g) = b by A50, CAT_2: 9;



             A53: a9 = ( dom f) by A46, A51, CAT_2: 9;

            b9 = ( cod f) by A47, A52, CAT_2: 9;

            hence thesis by A48, A53;

          end;

        end;



         A54: ( dom the Comp of T) c= ( dom the Comp of E)

        proof

          let x be object;

          assume

           A55: x in ( dom the Comp of T);

          then

          reconsider x1 = (x `1 ), x2 = (x `2 ) as Element of M by MCART_1: 10;

          reconsider y1 = x1, y2 = x2 as Morphism of T;

          reconsider z1 = x1, z2 = x2 as Morphism of E by A45;



           A56: x = [x1, x2] by A55, MCART_1: 21;

          then

           A57: ( dom y1) = ( cod y2) by A55, CAT_1: 15;



           A58: ( dom y1) = ( dom x1) by CAT_2: 9;



           A59: ( dom z1) = ( dom x1) by CAT_2: 9;



           A60: ( cod y2) = ( cod x2) by CAT_2: 9;

          ( cod z2) = ( cod x2) by CAT_2: 9;

          hence thesis by A56, A57, A58, A59, A60, CAT_1: 15;

        end;

        now

          let x be object;

          assume

           A61: x in ( dom the Comp of T);



           A62: the Comp of T c= the Comp of D by CAT_2:def 4;



           A63: the Comp of E c= the Comp of D by CAT_2:def 4;



          thus (the Comp of T . x) = (the Comp of D . x) by A61, A62, GRFUNC_1: 2

          .= (the Comp of E . x) by A54, A61, A63, GRFUNC_1: 2;

        end;

        hence the Comp of T c= the Comp of E by A54, GRFUNC_1: 2;

        let a be Object of T, a9 be Object of E;

        reconsider b = a as Object of D by TARSKI:def 3;

        assume

         A64: a = a9;

        ( id a) = ( id b) by CAT_2:def 4;

        hence thesis by A64, CAT_2:def 4;

      end;

      uniqueness

      proof

        let C1,C2 be strict Subcategory of D such that

         A65: the carrier of C1 = ( rng ( Obj F)) and

         A66: ( rng F) c= the carrier' of C1 and

         A67: for E be Subcategory of D st the carrier of E = ( rng ( Obj F)) & ( rng F) c= the carrier' of E holds C1 is Subcategory of E and

         A68: the carrier of C2 = ( rng ( Obj F)) and

         A69: ( rng F) c= the carrier' of C2 and

         A70: for E be Subcategory of D st the carrier of E = ( rng ( Obj F)) & ( rng F) c= the carrier' of E holds C2 is Subcategory of E;



         A71: C1 is Subcategory of C2 by A67, A68, A69;

        C2 is Subcategory of C1 by A65, A66, A70;

        hence thesis by A71, Th3;

      end;

    end

    theorem :: CAT_5:7



     Th7: for C,D be Category, E be Subcategory of D, F be Functor of C, D st ( rng F) c= the carrier' of E holds F is Functor of C, E

    proof

      let C,D be Category, E be Subcategory of D, F be Functor of C, D;

      assume

       A1: ( rng F) c= the carrier' of E;



       A2: ( dom F) = the carrier' of C by FUNCT_2:def 1;



       A3: ( dom ( Obj F)) = the carrier of C by FUNCT_2:def 1;

      reconsider G = F as Function of the carrier' of C, the carrier' of E by A1, A2, FUNCT_2:def 1, RELSET_1: 4;



       A4: ( rng ( Obj F)) c= the carrier of E

      proof

        let y be object;

        assume y in ( rng ( Obj F));

        then

        consider x be object such that

         A5: x in ( dom ( Obj F)) and

         A6: y = (( Obj F) . x) by FUNCT_1:def 3;

        reconsider x as Object of C by A5;

        (F . ( id x)) = ( id (( Obj F) . x)) by CAT_1: 68;

        then ( id (( Obj F) . x)) in ( rng F) by A2, FUNCT_1:def 3;

        then

        reconsider f = ( id (( Obj F) . x)) as Morphism of E by A1;



         A7: ( dom ( id (( Obj F) . x))) = y by A6;

        ( dom ( id (( Obj F) . x))) = ( dom f) by CAT_2: 9;

        hence thesis by A7;

      end;

       A8:

      now

        let c be Object of C;

        (( Obj F) . c) in ( rng ( Obj F)) by A3, FUNCT_1:def 3;

        then

        reconsider d = (( Obj F) . c) as Object of E by A4;

        take d;



        thus (G . ( id c)) = ( id (( Obj F) . c)) by CAT_1: 68

        .= ( id d) by CAT_2:def 4;

      end;

       A9:

      now

        let f be Morphism of C;



         A10: ( dom (F . f)) = ( dom (G . f)) by CAT_2: 9;



         A11: ( cod (F . f)) = ( cod (G . f)) by CAT_2: 9;



        thus (G . ( id ( dom f))) = ( id (F . ( dom f))) by CAT_1: 71

        .= ( id ( dom (F . f))) by CAT_1: 72

        .= ( id ( dom (G . f))) by A10, CAT_2:def 4;



        thus (G . ( id ( cod f))) = ( id (F . ( cod f))) by CAT_1: 71

        .= ( id ( cod (F . f))) by CAT_1: 72

        .= ( id ( cod (G . f))) by A11, CAT_2:def 4;

      end;

      now

        let f,g be Morphism of C;

        assume

         A12: ( dom g) = ( cod f);

        then

         A13: (F . (g (*) f)) = ((F . g) (*) (F . f)) by CAT_1: 64;



         A14: ( dom (F . g)) = ( cod (F . f)) by A12, CAT_1: 64;



         A15: ( dom (F . g)) = ( dom (G . g)) by CAT_2: 9;

        ( cod (F . f)) = ( cod (G . f)) by CAT_2: 9;

        hence (G . (g (*) f)) = ((G . g) (*) (G . f)) by A13, A14, A15, CAT_2: 11;

      end;

      hence thesis by A8, A9, CAT_1: 61;

    end;

    theorem :: CAT_5:8

    for C,D be Category, F be Functor of C, D holds F is Functor of C, ( Image F)

    proof

      let C,D be Category, F be Functor of C, D;

      ( rng F) c= the carrier' of ( Image F) by Def3;

      hence thesis by Th7;

    end;

    theorem :: CAT_5:9



     Th9: for C,D be Category, E be Subcategory of D, F be Functor of C, E holds for G be Functor of C, D st F = G holds ( Image F) = ( Image G)

    proof

      let C,D be Category, E be Subcategory of D;

      let F be Functor of C, E, G be Functor of C, D such that

       A1: F = G;

      reconsider S = ( Image F) as strict Subcategory of D by Th4;

       A2:

      now

        thus ( dom ( Obj F)) = the carrier of C & ( dom ( Obj G)) = the carrier of C by FUNCT_2:def 1;

        let x be object;

        assume x in the carrier of C;

        then

        reconsider a = x as Object of C;

        reconsider b = (( Obj F) . a) as Object of D by CAT_2: 6;

        (G . ( id a)) = ( id (( Obj F) . a)) by A1, CAT_1: 68

        .= ( id b) by CAT_2:def 4;

        hence (( Obj G) . x) = (( Obj F) . x) by CAT_1: 67;

      end;

      then

       A3: ( Obj F) = ( Obj G);

      then

       A4: the carrier of S = ( rng ( Obj G)) by Def3;



       A5: ( rng G) c= the carrier' of S by A1, Def3;

      now

        let T be Subcategory of D;

        assume that

         A6: the carrier of T = ( rng ( Obj G)) and

         A7: ( rng G) c= the carrier' of T;

        set x = the Object of C;



         A8: (( Obj G) . x) in ( rng ( Obj G)) by A2, FUNCT_1:def 3;



         A9: (( Obj G) . x) = (( Obj F) . x) by A2;

        then (( Obj G) . x) in (the carrier of T /\ the carrier of E) by A6, A8, XBOOLE_0:def 4;

        then

         A10: the carrier of T meets the carrier of E;

        then

        reconsider E1 = (T /\ E) as Subcategory of E by Th6;

        the carrier of E1 = (the carrier of T /\ the carrier of E) by A6, A8, A9, Def2;

        then

         A11: the carrier of E1 = ( rng ( Obj F)) by A3, A6, XBOOLE_1: 28;

        the carrier' of E1 = (the carrier' of T /\ the carrier' of E) by A6, A8, A9, Def2;

        then ( rng F) c= the carrier' of E1 by A1, A7, XBOOLE_1: 19;

        then

         A12: ( Image F) is Subcategory of E1 by A11, Def3;

        E1 is Subcategory of T by A10, Th6;

        hence S is Subcategory of T by A12, Th4;

      end;

      hence thesis by A4, A5, Def3;

    end;

    begin

    definition

      let IT be set;

      :: CAT_5:def4

      attr IT is categorial means

      : Def4: for x be set st x in IT holds x is Category;

    end

    definition

      let X be non empty set;

      :: original: categorial

      redefine

      :: CAT_5:def5

      attr X is categorial means for x be Element of X holds x is Category;

      compatibility ;

    end

    registration

      cluster categorial for non empty set;

      existence

      proof

        take X = {( 1Cat ( 0 , { 0 }))};

        let x be Element of X;

        thus thesis by TARSKI:def 1;

      end;

    end

    definition

      let X be non empty categorial set;

      :: original: Element

      redefine

      mode Element of X -> Category ;

      coherence by Def4;

    end

    definition

      let C be Category;

      :: CAT_5:def6

      attr C is Categorial means

      : Def6: the carrier of C is categorial & (for a be Object of C, A be Category st a = A holds ( id a) = [ [A, A], ( id A)]) & (for m be Morphism of C holds for A,B be Category st A = ( dom m) & B = ( cod m) holds ex F be Functor of A, B st m = [ [A, B], F]) & for m1,m2 be Morphism of C holds for A,B,C be Category holds for F be Functor of A, B holds for G be Functor of B, C st m1 = [ [A, B], F] & m2 = [ [B, C], G] holds (m2 (*) m1) = [ [A, C], (G * F)];

    end

    registration

      cluster Categorial -> with_triple-like_morphisms for Category;

      coherence

      proof

        let C be Category;

        assume

         A1: C is Categorial;

        then

         A2: the carrier of C is categorial;

        let f be Morphism of C;

        reconsider A = ( dom f), B = ( cod f) as Category by A2;

        ex F be Functor of A, B st f = [ [A, B], F] by A1;

        hence thesis;

      end;

    end

    theorem :: CAT_5:10



     Th10: for C,D be Category st the CatStr of C = the CatStr of D holds C is Categorial implies D is Categorial

    proof

      let C,D be Category;

      assume

       A1: the CatStr of C = the CatStr of D;

      assume that

       A2: the carrier of C is categorial and

       A3: for a be Object of C, A be Category st a = A holds ( id a) = [ [A, A], ( id A)] and

       A4: for m be Morphism of C holds for A,B be Category st A = ( dom m) & B = ( cod m) holds ex F be Functor of A, B st m = [ [A, B], F] and

       A5: for m1,m2 be Morphism of C holds for A,B,C be Category holds for F be Functor of A, B holds for G be Functor of B, C st m1 = [ [A, B], F] & m2 = [ [B, C], G] holds (m2 (*) m1) = [ [A, C], (G * F)];

      thus the carrier of D is categorial by A1, A2;

      thus for a be Object of D, A be Category st a = A holds ( id a) = [ [A, A], ( id A)]

      proof

        let a be Object of D, A be Category;

        reconsider b = a as Object of C by A1;

        assume a = A;

        then [ [A, A], ( id A)] = ( id b) by A3;

        hence ( id a) = [ [A, A], ( id A)] by A1, Lm1;

      end;

      hereby

        let m be Morphism of D;

        reconsider m9 = m as Morphism of C by A1;

        let A,B be Category;

        assume that

         A6: A = ( dom m) and

         A7: B = ( cod m);



         A8: A = ( dom m9) by A1, A6;

        B = ( cod m9) by A1, A7;

        hence ex F be Functor of A, B st m = [ [A, B], F] by A4, A8;

      end;

      let m1,m2 be Morphism of D;

      reconsider f1 = m1, f2 = m2 as Morphism of C by A1;

      let a,b,c be Category;

      let F be Functor of a, b, G be Functor of b, c;

      assume that

       A9: m1 = [ [a, b], F] and

       A10: m2 = [ [b, c], G];

      reconsider a1 = ( dom f1), b1 = ( cod f1), a2 = ( dom f2), b2 = ( cod f2) as Category by A2;



       A11: ex F1 be Functor of a1, b1 st (f1 = [ [a1, b1], F1]) by A4;

      ex F2 be Functor of a2, b2 st (f2 = [ [a2, b2], F2]) by A4;

      then

       A12: ( dom f2) = (m2 `11 ) by MCART_1: 85;



       A13: (m2 `11 ) = b by A10, MCART_1: 85;



       A14: ( cod f1) = (m1 `12 ) by A11, MCART_1: 85;

      (m1 `12 ) = b by A9, MCART_1: 85;

      then

       A15: [f2, f1] in ( dom the Comp of C) by A12, A13, A14, CAT_1: 15;



      hence (m2 (*) m1) = (the Comp of D . (m2,m1)) by A1, CAT_1:def 1

      .= (f2 (*) f1) by A1, A15, CAT_1:def 1

      .= [ [a, c], (G * F)] by A5, A9, A10;

    end;

    theorem :: CAT_5:11



     Th11: for C be Category holds ( 1Cat (C, [ [C, C], ( id C)])) is Categorial

    proof

      let A be Category;

      set F = [ [A, A], ( id A)];

      set C = ( 1Cat (A,F));

      thus for x be Object of C holds x is Category by TARSKI:def 1;

      hereby

        let a be Object of C, D be Category;

        assume a = D;

        then D = A by TARSKI:def 1;

        hence ( id a) = [ [D, D], ( id D)] by TARSKI:def 1;

      end;

      hereby

        let m be Morphism of C;

        let C1,C2 be Category;

        assume that

         A1: C1 = ( dom m) and

         A2: C2 = ( cod m);



         A3: C1 = A by A1, TARSKI:def 1;



         A4: C2 = A by A2, TARSKI:def 1;

        reconsider G = ( id A) as Functor of C1, C2 by A2, A3, TARSKI:def 1;

        take G;

        thus m = [ [C1, C2], G] by A3, A4, TARSKI:def 1;

      end;

      let m1,m2 be Morphism of C;

      let A1,B,C be Category, F1 be Functor of A1, B, F2 be Functor of B, C;

      assume that

       A5: m1 = [ [A1, B], F1] and

       A6: m2 = [ [B, C], F2];



       A7: [ [A1, B], F1] = F by A5, TARSKI:def 1;



       A8: [ [B, C], F2] = F by A6, TARSKI:def 1;



       A9: [A1, B] = [A, A] by A7, XTUPLE_0: 1;



       A10: [A, A] = [B, C] by A8, XTUPLE_0: 1;



       A11: F1 = ( id A) by A7, XTUPLE_0: 1;



       A12: F2 = ( id A) by A8, XTUPLE_0: 1;



       A13: A1 = A by A9, XTUPLE_0: 1;



       A14: C = A by A10, XTUPLE_0: 1;

      (F2 * F1) = ( id A) by A11, A12, FUNCT_2: 17;

      hence thesis by A13, A14, TARSKI:def 1;

    end;

    registration

      cluster Categorial for strict Category;

      existence

      proof

        set A = ( 1Cat ( 0 , { 0 }));

        take ( 1Cat (A, [ [A, A], ( id A)]));

        thus thesis by Th11;

      end;

    end

    theorem :: CAT_5:12



     Th12: for C be Categorial Category, a be Object of C holds a is Category

    proof

      let C be Categorial Category;

      the carrier of C is categorial by Def6;

      hence thesis;

    end;

    theorem :: CAT_5:13



     Th13: for C be Categorial Category, f be Morphism of C holds ( dom f) = (f `11 ) & ( cod f) = (f `12 )

    proof

      let C be Categorial Category;

      let f be Morphism of C;

      reconsider A = ( dom f), B = ( cod f) as Category by Th12;

      ex F be Functor of A, B st f = [ [A, B], F] by Def6;

      hence thesis by MCART_1: 85;

    end;

    definition

      let C be Categorial Category;

      let m be Morphism of C;

      :: original: `11

      redefine

      func m `11 -> Category ;

      coherence

      proof

        ( dom m) = (m `11 ) by Th13;

        hence thesis by Th12;

      end;

      :: original: `12

      redefine

      func m `12 -> Category ;

      coherence

      proof

        ( cod m) = (m `12 ) by Th13;

        hence thesis by Th12;

      end;

    end

    theorem :: CAT_5:14



     Th14: for C1,C2 be Categorial Category st the carrier of C1 = the carrier of C2 & the carrier' of C1 = the carrier' of C2 holds the CatStr of C1 = the CatStr of C2

    proof

      let C1,C2 be Categorial Category;

      assume that

       A1: the carrier of C1 = the carrier of C2 and

       A2: the carrier' of C1 = the carrier' of C2;



       A3: ( dom the Source of C1) = the carrier' of C1 by FUNCT_2:def 1;



       A4: ( dom the Source of C2) = the carrier' of C2 by FUNCT_2:def 1;



       A5: ( dom the Target of C1) = the carrier' of C1 by FUNCT_2:def 1;



       A6: ( dom the Target of C2) = the carrier' of C2 by FUNCT_2:def 1;

      now

        let x be object;

        assume x in the carrier' of C1;

        then

        reconsider m1 = x as Morphism of C1;

        reconsider m2 = m1 as Morphism of C2 by A2;



        thus (the Source of C1 . x) = ( dom m1)

        .= (m1 `11 ) by Th13

        .= ( dom m2) by Th13

        .= (the Source of C2 . x);

      end;

      then

       A7: the Source of C1 = the Source of C2 by A2, A3, A4;

       A8:

      now

        let x be object;

        assume x in the carrier' of C1;

        then

        reconsider m1 = x as Morphism of C1;

        reconsider m2 = m1 as Morphism of C2 by A2;



        thus (the Target of C1 . x) = ( cod m1)

        .= (m1 `12 ) by Th13

        .= ( cod m2) by Th13

        .= (the Target of C2 . x);

      end;

      then

       A9: the Target of C1 = the Target of C2 by A2, A5, A6;



       A10: ( dom the Comp of C1) = ( dom the Comp of C2)

      proof

        hereby

          let x be object;

          assume

           A11: x in ( dom the Comp of C1);

          then

          reconsider xx = x as Element of [:the carrier' of C1, the carrier' of C1:];

          reconsider y = xx as Element of [:the carrier' of C2, the carrier' of C2:] by A2;



           A12: y = [(xx `1 ), (xx `2 )] by MCART_1: 21;

          then ( dom (xx `1 )) = ( cod (xx `2 )) by A11, CAT_1:def 6;

          then ( dom (y `1 )) = ( cod (y `2 )) by A8, A7;

          hence x in ( dom the Comp of C2) by A12, CAT_1:def 6;

        end;

        let x be object;

        assume

         A13: x in ( dom the Comp of C2);

        then

        reconsider xx = x as Element of [:the carrier' of C1, the carrier' of C1:] by A2;

        reconsider y = xx as Element of [:the carrier' of C2, the carrier' of C2:] by A2;



         A14: xx = [(y `1 ), (y `2 )] by MCART_1: 21;

        then ( dom (y `1 )) = ( cod (y `2 )) by A13, CAT_1:def 6;

        then ( dom (xx `1 )) = ( cod (xx `2 )) by A8, A7;

        hence thesis by A14, CAT_1:def 6;

      end;

      now

        let x,y be object;

        assume

         A15: [x, y] in ( dom the Comp of C1);

        then

        reconsider g1 = x, h1 = y as Morphism of C1 by ZFMISC_1: 87;

        reconsider g2 = g1, h2 = h1 as Morphism of C2 by A2;

        reconsider a1 = ( dom g1), b1 = ( cod g1) as Category by Th12;

        consider f1 be Functor of a1, b1 such that

         A16: g1 = [ [a1, b1], f1] by Def6;

        reconsider c1 = ( dom h1), d1 = ( cod h1) as Category by Th12;

        consider i1 be Functor of c1, d1 such that

         A17: h1 = [ [c1, d1], i1] by Def6;



         A18: a1 = d1 by A15, CAT_1: 15;



        thus (the Comp of C1 . (x,y)) = (g1 (*) h1) by A15, CAT_1:def 1

        .= [ [c1, b1], (f1 * i1)] by A16, A17, A18, Def6

        .= (g2 (*) h2) by A16, A17, A18, Def6

        .= (the Comp of C2 . (x,y)) by A10, A15, CAT_1:def 1;

      end;

      then the Comp of C1 = the Comp of C2 by A2, A10, BINOP_1: 20;

      hence thesis by A1, A2, A7, A9;

    end;

    registration

      let C be Categorial Category;

      cluster -> Categorial for Subcategory of C;

      coherence

      proof

        let D be Subcategory of C;



         A1: the carrier of C is categorial by Def6;

        thus the carrier of D is categorial

        proof

          let x be Object of D;

          x is Object of C by CAT_2: 6;

          hence thesis by A1;

        end;

        hereby

          let a be Object of D, A be Category;

          reconsider b = a as Object of C by CAT_2: 6;

          assume a = A;

          then [ [A, A], ( id A)] = ( id b) by Def6;

          hence ( id a) = [ [A, A], ( id A)] by CAT_2:def 4;

        end;

        hereby

          let m be Morphism of D;

          reconsider m9 = m as Morphism of C by CAT_2: 8;

          let a,b be Category;

          assume that

           A2: a = ( dom m) and

           A3: b = ( cod m);



           A4: ( dom m9) = a by A2, CAT_2: 9;

          ( cod m9) = b by A3, CAT_2: 9;

          hence ex F be Functor of a, b st m = [ [a, b], F] by A4, Def6;

        end;

        let m1,m2 be Morphism of D;

        let a,b,c be Category;

        reconsider m19 = m1, m29 = m2 as Morphism of C by CAT_2: 8;

        let f be Functor of a, b;

        let g be Functor of b, c;

        assume that

         A5: m1 = [ [a, b], f] and

         A6: m2 = [ [b, c], g];



         A7: ( dom m2) = ( dom m29) by CAT_2: 9;



         A8: ( cod m1) = ( cod m19) by CAT_2: 9;



         A9: ( dom m29) = (m2 `11 ) by Th13;



         A10: ( cod m19) = (m1 `12 ) by Th13;



         A11: ( dom m2) = b by A6, A7, A9, MCART_1: 85;

        ( cod m1) = b by A5, A8, A10, MCART_1: 85;



        hence (m2 (*) m1) = (m29 (*) m19) by A11, CAT_2: 11

        .= [ [a, c], (g * f)] by A5, A6, Def6;

      end;

    end

    theorem :: CAT_5:15



     Th15: for C,D be Categorial Category st the carrier' of C c= the carrier' of D holds C is Subcategory of D

    proof

      let C,D be Categorial Category;

      assume

       A1: the carrier' of C c= the carrier' of D;

      thus the carrier of C c= the carrier of D

      proof

        let x be object;

        assume x in the carrier of C;

        then

        reconsider a = x as Object of C;

        reconsider i = ( id a) as Morphism of D by A1;



         A2: ( dom i) = (i `11 ) by Th13;

        ( dom ( id a)) = (i `11 ) by Th13;

        hence thesis by A2;

      end;

      hereby

        let a,b be Object of C, a9,b9 be Object of D;

        assume that

         A3: a = a9 and

         A4: b = b9;

        thus ( Hom (a,b)) c= ( Hom (a9,b9))

        proof

          let x be object;

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

          then

          consider f be Morphism of C such that

           A5: x = f and

           A6: ( dom f) = a and

           A7: ( cod f) = b;

          reconsider A = a, B = b as Category by Th12;



           A8: ex F be Functor of A, B st (f = [ [A, B], F]) by A6, A7, Def6;

          reconsider f as Morphism of D by A1;



           A9: ( dom f) = (f `11 ) by Th13;



           A10: ( cod f) = (f `12 ) by Th13;



           A11: (f `11 ) = A by A8, MCART_1: 85;

          (f `12 ) = B by A8, MCART_1: 85;

          hence thesis by A3, A4, A5, A9, A10, A11;

        end;

      end;



       A12: ( dom the Comp of C) c= ( dom the Comp of D)

      proof

        let x be object;

        assume

         A13: x in ( dom the Comp of C);

        then

        reconsider g = (x `1 ), f = (x `2 ) as Morphism of C by MCART_1: 10;

        reconsider g9 = g, f9 = f as Morphism of D by A1;



         A14: x = [g, f] by A13, MCART_1: 21;

        then

         A15: ( dom g) = ( cod f) by A13, CAT_1: 15;



         A16: ( dom g) = (g `11 ) by Th13;



         A17: ( dom g9) = (g `11 ) by Th13;



         A18: ( cod f) = (f `12 ) by Th13;

        ( cod f9) = (f `12 ) by Th13;

        hence thesis by A14, A15, A16, A17, A18, CAT_1: 15;

      end;

      now

        let x be object;

        assume

         A19: x in ( dom the Comp of C);

        then

        reconsider g = (x `1 ), f = (x `2 ) as Morphism of C by MCART_1: 10;

        reconsider g9 = g, f9 = f as Morphism of D by A1;



         A20: x = [g, f] by A19, MCART_1: 21;



         A21: ( dom g) = (g `11 ) by Th13;

        ( cod g) = (g `12 ) by Th13;

        then

        consider G be Functor of (g `11 ), (g `12 ) such that

         A22: g = [ [(g `11 ), (g `12 )], G] by A21, Def6;



         A23: ( dom f) = (f `11 ) by Th13;

        ( cod f) = ( dom g) by A19, A20, CAT_1: 15;

        then

        consider F be Functor of (f `11 ), (g `11 ) such that

         A24: f = [ [(f `11 ), (g `11 )], F] by A21, A23, Def6;



        thus (the Comp of C . x) = (the Comp of C . (g,f)) by A19, MCART_1: 21

        .= (g (*) f) by A19, A20, CAT_1:def 1

        .= [ [(f `11 ), (g `12 )], (G * F)] by A22, A24, Def6

        .= (g9 (*) f9) by A22, A24, Def6

        .= (the Comp of D . (g,f)) by A12, A19, A20, CAT_1:def 1

        .= (the Comp of D . x) by A19, MCART_1: 21;

      end;

      hence the Comp of C c= the Comp of D by A12, GRFUNC_1: 2;

      let a be Object of C, a9 be Object of D;

      assume

       A25: a = a9;

      reconsider A = a as Category by Th12;



      thus ( id a) = [ [A, A], ( id A)] by Def6

      .= ( id a9) by A25, Def6;

    end;

    definition

      let a be object;

      :: CAT_5:def7

      func cat a -> Category equals

      : Def7: a;

      correctness by A1;

    end

    theorem :: CAT_5:16



     Th16: for C be Categorial Category, c be Object of C holds ( cat c) = c

    proof

      let C be Categorial Category, c be Object of C;

      the carrier of C is categorial by Def6;

      then c is Category;

      hence thesis by Def7;

    end;

    definition

      let C be Categorial Category;

      let m be Morphism of C;

      :: original: `2

      redefine

      func m `2 -> Functor of ( cat ( dom m)), ( cat ( cod m)) ;

      coherence

      proof

        the carrier of C is categorial by Def6;

        then

        reconsider A = ( dom m), B = ( cod m) as Category;

        consider F be Functor of A, B such that

         A1: m = [ [A, B], F] by Def6;



         A2: (m `2 ) = F by A1;

        ( cat A) = A by Def7;

        hence thesis by A2, Def7;

      end;

    end

    theorem :: CAT_5:17



     Th17: for X be categorial non empty set, Y be non empty set st (for A,B,C be Element of X holds for F be Functor of A, B, G be Functor of B, C st F in Y & G in Y holds (G * F) in Y) & (for A be Element of X holds ( id A) in Y) holds ex C be strict Categorial Category st the carrier of C = X & for A,B be Element of X, F be Functor of A, B holds [ [A, B], F] is Morphism of C iff F in Y

    proof

      let X be categorial non empty set, Y be non empty set such that

       A1: for A,B,C be Element of X holds for F be Functor of A, B, G be Functor of B, C st F in Y & G in Y holds (G * F) in Y and

       A2: for A be Element of X holds ( id A) in Y;

      set B = { b where b be Element of Y : b is Function };

      set a = the Element of X;

      ( id a) in Y by A2;

      then ( id a) in B;

      then

      reconsider B as non empty set;

      B is functional

      proof

        let x be object;

        assume x in B;

        then ex b be Element of Y st x = b & b is Function;

        hence thesis;

      end;

      then

      reconsider B as non empty functional set;

      reconsider A = X as non empty categorial set;

      defpred P[ Element of A, Element of A, set] means $3 is Functor of $1, $2;

      deffunc F( Function, Function) = ($1 * $2);



       A3: for a,b,c be Element of A, f,g be Element of B st P[a, b, f] & P[b, c, g] holds F(g,f) in B & P[a, c, F(g,f)]

      proof

        let a,b,c be Element of A, f,g be Element of B;

        assume that

         A4: P[a, b, f] and

         A5: P[b, c, g];

        reconsider f as Functor of a, b by A4;

        reconsider g as Functor of b, c by A5;



         A6: f in B;



         A7: g in B;



         A8: ex b be Element of Y st f = b & b is Function by A6;

        ex b be Element of Y st g = b & b is Function by A7;

        then (g * f) in Y by A1, A8;

        hence thesis;

      end;



       A9: for a be Element of A holds ex f be Element of B st P[a, a, f] & for b be Element of A, g be Element of B holds ( P[a, b, g] implies F(g,f) = g) & ( P[b, a, g] implies F(f,g) = g)

      proof

        let a be Element of A;

        reconsider f = ( id a) as Element of Y by A2;

        f in B;

        then

        reconsider f as Element of B;

        take f;

        thus P[a, a, f];

        let b be Element of A, g be Element of B;

        thus P[a, b, g] implies (g * f) = g by FUNCT_2: 17;

        assume P[b, a, g];

        then

        reconsider G = g as Functor of b, a;

        (( id a) * G) = G by FUNCT_2: 17;

        hence thesis;

      end;



       A10: for a,b,c,d be Element of A, f,g,h be Element of B st P[a, b, f] & P[b, c, g] & P[c, d, h] holds F(h,F) = F(F,f) by RELAT_1: 36;

      consider C be strict with_triple-like_morphisms Category such that

       A11: the carrier of C = A & (for a,b be Element of A, f be Element of B st P[a, b, f] holds [ [a, b], f] is Morphism of C) & (for m be Morphism of C holds ex a,b be Element of A, f be Element of B st m = [ [a, b], f] & P[a, b, f]) & for m1,m2 be Morphism of C, a1,a2,a3 be Element of A, f1,f2 be Element of B st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)] from CatEx( A3, A9, A10);

      C is Categorial

      proof

        thus the carrier of C is categorial by A11;

        hereby

          let a be Object of C, D be Category;

          assume

           A12: a = D;

          then ( id D) in Y by A2, A11;

          then ( id D) in B;

          then

          reconsider f = ( id D) as Element of B;

          reconsider x = a as Element of A by A11;

          reconsider F = [ [x, x], f] as Morphism of C by A11, A12;

          consider b,c be Element of A, g be Element of B such that

           A13: ( id a) = [ [b, c], g] and

           A14: P[b, c, g] by A11;



           A15: ( dom ( id a)) = (( id a) `11 ) by Th2;



           A16: (( id a) `11 ) = b by A13, MCART_1: 85;

          ( cod F) = (F `12 ) by Th2

          .= x by MCART_1: 85;



          then F = (( id a) (*) F) by CAT_1: 21

          .= [ [x, c], (g * ( id the carrier' of D))] by A11, A13, A15, A16

          .= [ [x, c], g] by A12, A14, A15, A16, FUNCT_2: 17;

          hence ( id a) = [ [D, D], ( id D)] by A12, A13, A15, MCART_1: 85;

        end;

        hereby

          let m be Morphism of C;

          consider a,b be Element of A, f be Element of B such that

           A17: m = [ [a, b], f] and

           A18: P[a, b, f] by A11;



           A19: ( dom m) = (m `11 ) by Th2;



           A20: ( cod m) = (m `12 ) by Th2;



           A21: ( dom m) = a by A17, A19, MCART_1: 85;

          ( cod m) = b by A17, A20, MCART_1: 85;

          hence for A,B be Category st A = ( dom m) & B = ( cod m) holds ex F be Functor of A, B st m = [ [A, B], F] by A17, A18, A21;

        end;

        let m1,m2 be Morphism of C;

        consider a1,b1 be Element of A, f1 be Element of B such that

         A22: m1 = [ [a1, b1], f1] and P[a1, b1, f1] by A11;

        consider a2,b2 be Element of A, f2 be Element of B such that

         A23: m2 = [ [a2, b2], f2] and P[a2, b2, f2] by A11;

        let A,B,C be Category;

        let F be Functor of A, B;

        let G be Functor of B, C;

        assume that

         A24: m1 = [ [A, B], F] and

         A25: m2 = [ [B, C], G];



         A26: [A, B] = [a1, b1] by A22, A24, XTUPLE_0: 1;



         A27: [B, C] = [a2, b2] by A23, A25, XTUPLE_0: 1;



         A28: f1 = F by A22, A24, XTUPLE_0: 1;



         A29: f2 = G by A23, A25, XTUPLE_0: 1;



         A30: A = a1 by A26, XTUPLE_0: 1;



         A31: B = b1 by A26, XTUPLE_0: 1;

        C = b2 by A27, XTUPLE_0: 1;

        hence thesis by A11, A22, A25, A28, A29, A30, A31;

      end;

      then

      reconsider C as Categorial strict Category;

      take C;

      thus the carrier of C = X by A11;

      let A9,B9 be Element of X, F be Functor of A9, B9;

      hereby

        assume [ [A9, B9], F] is Morphism of C;

        then

        reconsider m = [ [A9, B9], F] as Morphism of C;

        consider a,b be Element of A, f be Element of B such that

         A32: m = [ [a, b], f] and P[a, b, f] by A11;

        (m `2 ) = f by A32;

        then F in B;

        then ex b be Element of Y st F = b & b is Function;

        hence F in Y;

      end;

      assume F in Y;

      then F in B;

      hence thesis by A11;

    end;

    theorem :: CAT_5:18



     Th18: for X be categorial non empty set, Y be non empty set holds for C1,C2 be strict Categorial Category st the carrier of C1 = X & (for A,B be Element of X, F be Functor of A, B holds [ [A, B], F] is Morphism of C1 iff F in Y) & the carrier of C2 = X & (for A,B be Element of X, F be Functor of A, B holds [ [A, B], F] is Morphism of C2 iff F in Y) holds C1 = C2

    proof

      let X be categorial non empty set, Y be non empty set;

      let C1,C2 be strict Categorial Category such that

       A1: the carrier of C1 = X and

       A2: for A,B be Element of X, F be Functor of A, B holds [ [A, B], F] is Morphism of C1 iff F in Y and

       A3: the carrier of C2 = X and

       A4: for A,B be Element of X, F be Functor of A, B holds [ [A, B], F] is Morphism of C2 iff F in Y;

      the carrier' of C1 = the carrier' of C2

      proof

        hereby

          let x be object;

          assume x in the carrier' of C1;

          then

          reconsider m = x as Morphism of C1;

          reconsider a = ( dom m), b = ( cod m) as Category by Th12;

          consider f be Functor of a, b such that

           A5: m = [ [a, b], f] by Def6;

          f in Y by A1, A2, A5;

          then x is Morphism of C2 by A1, A4, A5;

          hence x in the carrier' of C2;

        end;

        let x be object;

        assume x in the carrier' of C2;

        then

        reconsider m = x as Morphism of C2;

        reconsider a = ( dom m), b = ( cod m) as Category by Th12;

        consider f be Functor of a, b such that

         A6: m = [ [a, b], f] by Def6;

        f in Y by A3, A4, A6;

        then x is Morphism of C1 by A2, A3, A6;

        hence thesis;

      end;

      hence thesis by A1, A3, Th14;

    end;

    definition

      let IT be Categorial Category;

      :: CAT_5:def8

      attr IT is full means

      : Def8: for a,b be Category st a is Object of IT & b is Object of IT holds for F be Functor of a, b holds [ [a, b], F] is Morphism of IT;

    end

    registration

      cluster full for Categorial strict Category;

      existence

      proof

        set A = ( 1Cat ( 0 , { 0 }));

        reconsider C = ( 1Cat (A, [ [A, A], ( id A)])) as Categorial strict Category by Th11;

        take C;

        let a,b be Category;

        assume that

         A1: a is Object of C and

         A2: b is Object of C;

        let F be Functor of a, b;



         A3: a = A by A1, TARSKI:def 1;



         A4: b = A by A2, TARSKI:def 1;

        then ( id A) = F by A3, FUNCT_2: 51;

        hence thesis by A3, A4, TARSKI:def 1;

      end;

    end

    theorem :: CAT_5:19

    for C1,C2 be full Categorial Category st the carrier of C1 = the carrier of C2 holds the CatStr of C1 = the CatStr of C2

    proof

      let C1,C2 be full Categorial Category;

      assume

       A1: the carrier of C1 = the carrier of C2;

      reconsider A = the carrier of C1 as categorial non empty set by Def6;

      set B = the set of all (m `2 ) where m be Morphism of C1;

      set m = the Morphism of C1;

      (m `2 ) in B;

      then

      reconsider B as non empty set;

      reconsider D1 = the CatStr of C1, D2 = the CatStr of C2 as strict Category by Th1;



       A2: D1 is Categorial by Th10;



       A3: D2 is Categorial by Th10;

       A4:

      now

        let a,b be Element of A, F be Functor of a, b;

        reconsider m = [ [a, b], F] as Morphism of C1 by Def8;

        (m `2 ) = F;

        hence [ [a, b], F] is Morphism of the CatStr of C1 iff F in B;

      end;

      now

        let a,b be Element of A, F be Functor of a, b;

        reconsider a9 = a, b9 = b as Object of C2 by A1;



         A5: ( cat a9) = a by Th16;

        ( cat b9) = b by Th16;

        then

        reconsider m2 = [ [a, b], F] as Morphism of C2 by A5, Def8;

        reconsider m = [ [a, b], F] as Morphism of C1 by Def8;



         A6: (m `2 ) = F;

        m2 = m2;

        hence [ [a, b], F] is Morphism of the CatStr of C2 iff F in B by A6;

      end;

      hence thesis by A1, A2, A3, A4, Th18;

    end;

    theorem :: CAT_5:20



     Th20: for A be categorial non empty set holds ex C be full Categorial strict Category st the carrier of C = A

    proof

      let AA be categorial non empty set;

      set dFF = the set of all ( Funct (a,b)) where a be Element of AA, b be Element of AA;

      set a = the Element of AA, f = the Functor of a, a;



       A1: f in ( Funct (a,a)) by CAT_2:def 2;

      ( Funct (a,a)) in dFF;

      then

      reconsider FF = ( union dFF) as non empty set by A1, TARSKI:def 4;

       A2:

      now

        let A,B,C be Element of AA;

        let F be Functor of A, B, G be Functor of B, C;

        assume that F in FF and G in FF;



         A3: (G * F) in ( Funct (A,C)) by CAT_2:def 2;

        ( Funct (A,C)) in dFF;

        hence (G * F) in FF by A3, TARSKI:def 4;

      end;

      now

        let A be Element of AA;



         A4: ( id A) in ( Funct (A,A)) by CAT_2:def 2;

        ( Funct (A,A)) in dFF;

        hence ( id A) in FF by A4, TARSKI:def 4;

      end;

      then

      consider C be strict Categorial Category such that

       A5: the carrier of C = AA and

       A6: for A,B be Element of AA, F be Functor of A, B holds [ [A, B], F] is Morphism of C iff F in FF by A2, Th17;

      C is full

      proof

        let a,b be Category;

        assume that

         A7: a is Object of C and

         A8: b is Object of C;

        reconsider A = a, B = b as Element of AA by A5, A7, A8;

        let F be Functor of a, b;



         A9: F in ( Funct (A,B)) by CAT_2:def 2;

        ( Funct (A,B)) in dFF;

        then F in FF by A9, TARSKI:def 4;

        then [ [A, B], F] is Morphism of C by A6;

        hence thesis;

      end;

      hence thesis by A5;

    end;

    theorem :: CAT_5:21



     Th21: for C be Categorial Category, D be full Categorial Category st the carrier of C c= the carrier of D holds C is Subcategory of D

    proof

      let C be Categorial Category;

      let D be full Categorial Category;

      assume

       A1: the carrier of C c= the carrier of D;

      the carrier' of C c= the carrier' of D

      proof

        let x be object;

        assume x in the carrier' of C;

        then

        reconsider x as Morphism of C;

        reconsider y1 = ( dom x), y2 = ( cod x) as Category by Th12;

        consider F be Functor of y1, y2 such that

         A2: x = [ [y1, y2], F] by Def6;



         A3: y1 is Object of D by A1;

        y2 is Object of D by A1;

        then [ [y1, y2], F] is Morphism of D by A3, Def8;

        hence thesis by A2;

      end;

      hence thesis by Th15;

    end;

    theorem :: CAT_5:22

    for C be Category, D1,D2 be Categorial Category holds for F1 be Functor of C, D1 holds for F2 be Functor of C, D2 st F1 = F2 holds ( Image F1) = ( Image F2)

    proof

      let C be Category, D1,D2 be Categorial Category;

      let F1 be Functor of C, D1;

      let F2 be Functor of C, D2;

      assume

       A1: F1 = F2;

      reconsider DD = (the carrier of D1 \/ the carrier of D2) as non empty set;

      DD is categorial

      proof

        let d be Element of DD;

        d is Object of D1 or d is Object of D2 by XBOOLE_0:def 3;

        hence thesis by Th12;

      end;

      then

      reconsider DD = (the carrier of D1 \/ the carrier of D2) as non empty categorial set;

      consider D be full Categorial strict Category such that

       A2: the carrier of D = DD by Th20;

      reconsider D1, D2 as Subcategory of D by A2, Th21, XBOOLE_1: 7;

      reconsider F1 as Functor of C, D1;

      reconsider F2 as Functor of C, D2;

      ( rng F1) c= the carrier' of D1;

      then F1 = (( incl D1) * F1) by RELAT_1: 53;

      then

      reconsider G1 = F1 as Functor of C, D;

      ( Image F1) = ( Image G1) by Th9

      .= ( Image F2) by A1, Th9;

      hence thesis;

    end;

    begin

    definition

      let C be Category;

      let o be Object of C;

      :: CAT_5:def9

      func Hom o -> Subset of the carrier' of C equals (the Target of C " {o});

      coherence ;

      :: CAT_5:def10

      func o Hom -> Subset of the carrier' of C equals (the Source of C " {o});

      coherence ;

    end

    registration

      let C be Category;

      let o be Object of C;

      cluster ( Hom o) -> non empty;

      coherence

      proof



         A1: (the Target of C . ( id o)) = ( cod ( id o))

        .= o;



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

        ( dom the Target of C) = the carrier' of C by FUNCT_2:def 1;

        hence thesis by A1, A2, FUNCT_1:def 7;

      end;

      cluster (o Hom ) -> non empty;

      coherence

      proof



         A3: (the Source of C . ( id o)) = ( dom ( id o))

        .= o;



         A4: o in {o} by TARSKI:def 1;

        ( dom the Source of C) = the carrier' of C by FUNCT_2:def 1;

        hence thesis by A3, A4, FUNCT_1:def 7;

      end;

    end

    theorem :: CAT_5:23



     Th23: for C be Category, a be Object of C, f be Morphism of C holds f in ( Hom a) iff ( cod f) = a

    proof

      let C be Category, a be Object of C, f be Morphism of C;

      ( cod f) in {a} iff ( cod f) = a by TARSKI:def 1;

      hence thesis by FUNCT_2: 38;

    end;

    theorem :: CAT_5:24



     Th24: for C be Category, a be Object of C, f be Morphism of C holds f in (a Hom ) iff ( dom f) = a

    proof

      let C be Category, a be Object of C, f be Morphism of C;

      ( dom f) in {a} iff ( dom f) = a by TARSKI:def 1;

      hence thesis by FUNCT_2: 38;

    end;

    theorem :: CAT_5:25

    for C be Category, a,b be Object of C holds ( Hom (a,b)) = ((a Hom ) /\ ( Hom b))

    proof

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

      hereby

        let x be object;

        assume

         A1: x in ( Hom (a,b));

        then

        reconsider f = x as Morphism of C;



         A2: ( dom f) = a by A1, CAT_1: 1;



         A3: ( cod f) = b by A1, CAT_1: 1;



         A4: f in (a Hom ) by A2, Th24;

        f in ( Hom b) by A3, Th23;

        hence x in ((a Hom ) /\ ( Hom b)) by A4, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A5: x in ((a Hom ) /\ ( Hom b));

      then

       A6: x in (a Hom ) by XBOOLE_0:def 4;



       A7: x in ( Hom b) by A5, XBOOLE_0:def 4;

      reconsider f = x as Morphism of C by A5;



       A8: ( dom f) = a by A6, Th24;

      ( cod f) = b by A7, Th23;

      hence thesis by A8;

    end;

    theorem :: CAT_5:26

    for C be Category, f be Morphism of C holds f in (( dom f) Hom ) & f in ( Hom ( cod f)) by Th23, Th24;

    theorem :: CAT_5:27



     Th27: for C be Category, f be Morphism of C, g be Element of ( Hom ( dom f)) holds (f (*) g) in ( Hom ( cod f))

    proof

      let C be Category, f be Morphism of C, g be Element of ( Hom ( dom f));

      ( cod g) = ( dom f) by Th23;

      then ( cod (f (*) g)) = ( cod f) by CAT_1: 17;

      hence thesis by Th23;

    end;

    theorem :: CAT_5:28



     Th28: for C be Category, f be Morphism of C, g be Element of (( cod f) Hom ) holds (g (*) f) in (( dom f) Hom )

    proof

      let C be Category, f be Morphism of C, g be Element of (( cod f) Hom );

      ( cod f) = ( dom g) by Th24;

      then ( dom (g (*) f)) = ( dom f) by CAT_1: 17;

      hence thesis by Th24;

    end;

    definition

      let C be Category, o be Object of C;

      set A = ( Hom o);

      set B = the carrier' of C;

      defpred P[ Element of A, Element of A, Element of B] means ( dom $2) = ( cod $3) & $1 = ($2 (*) $3);

      deffunc F( Morphism of C, Morphism of C) = ($1 (*) $2);



       A1: for a,b,c be Element of A, f,g be Element of B st P[a, b, f] & P[b, c, g] holds F(g,f) in B & P[a, c, F(g,f)]

      proof

        let a,b,c be Element of ( Hom o), f,g be Morphism of C;

        assume that

         A2: ( dom b) = ( cod f) and

         A3: a = (b (*) f) and

         A4: ( dom c) = ( cod g) and

         A5: b = (c (*) g);

        ( dom g) = ( cod f) by A2, A4, A5, CAT_1: 17;

        hence thesis by A3, A4, A5, CAT_1: 17, CAT_1: 18;

      end;



       A6: for a be Element of A holds ex f be Element of B st P[a, a, f] & for b be Element of A, g be Element of B holds ( P[a, b, g] implies F(g,f) = g) & ( P[b, a, g] implies F(f,g) = g)

      proof

        let a be Element of ( Hom o);

        take f = ( id ( dom a));

        thus ( dom a) = ( cod f) & a = (a (*) f) by CAT_1: 22;

        let b be Element of ( Hom o), g be Morphism of C;

        hereby

          assume that

           A7: ( dom b) = ( cod g) and

           A8: a = (b (*) g);

          ( dom a) = ( dom g) by A7, A8, CAT_1: 17;

          hence (g (*) f) = g by CAT_1: 22;

        end;

        thus thesis by CAT_1: 21;

      end;



       A9: for a,b,c,d be Element of A, f,g,h be Element of B st P[a, b, f] & P[b, c, g] & P[c, d, h] holds F(h,F) = F(F,f)

      proof

        let a,b,c,d be Element of ( Hom o), f,g,h be Morphism of C;

        assume that

         A10: ( dom b) = ( cod f) and a = (b (*) f) and

         A11: ( dom c) = ( cod g) and

         A12: b = (c (*) g) and

         A13: ( dom d) = ( cod h) and

         A14: c = (d (*) h);



         A15: ( dom g) = ( cod f) by A10, A11, A12, CAT_1: 17;

        ( dom h) = ( cod g) by A11, A13, A14, CAT_1: 17;

        hence thesis by A15, CAT_1: 18;

      end;

      :: CAT_5:def11

      func C -SliceCat (o) -> strict with_triple-like_morphisms Category means

      : Def11: the carrier of it = ( Hom o) & (for a,b be Element of ( Hom o), f be Morphism of C st ( dom b) = ( cod f) & a = (b (*) f) holds [ [a, b], f] is Morphism of it ) & (for m be Morphism of it holds ex a,b be Element of ( Hom o), f be Morphism of C st m = [ [a, b], f] & ( dom b) = ( cod f) & a = (b (*) f)) & for m1,m2 be Morphism of it , a1,a2,a3 be Element of ( Hom o), f1,f2 be Morphism of C st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], (f2 (*) f1)];

      existence

      proof

        thus ex F be with_triple-like_morphisms strict Category st the carrier of F = A & (for a,b be Element of A, f be Element of B st P[a, b, f] holds [ [a, b], f] is Morphism of F) & (for m be Morphism of F holds ex a,b be Element of A, f be Element of B st m = [ [a, b], f] & P[a, b, f]) & for m1,m2 be Morphism of F, a1,a2,a3 be Element of A, f1,f2 be Element of B st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)] from CatEx( A1, A6, A9);

      end;

      uniqueness

      proof

        thus for C1,C2 be strict with_triple-like_morphisms Category st the carrier of C1 = A & (for a,b be Element of A, f be Element of B st P[a, b, f] holds [ [a, b], f] is Morphism of C1) & (for m be Morphism of C1 holds ex a,b be Element of A, f be Element of B st m = [ [a, b], f] & P[a, b, f]) & (for m1,m2 be Morphism of C1, a1,a2,a3 be Element of A, f1,f2 be Element of B st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)]) & the carrier of C2 = A & (for a,b be Element of A, f be Element of B st P[a, b, f] holds [ [a, b], f] is Morphism of C2) & (for m be Morphism of C2 holds ex a,b be Element of A, f be Element of B st m = [ [a, b], f] & P[a, b, f]) & for m1,m2 be Morphism of C2, a1,a2,a3 be Element of A, f1,f2 be Element of B st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)] holds C1 = C2 from CatUniq( A6);

      end;

      set X = (o Hom );

      defpred R[ Element of X, Element of X, Element of B] means ( dom $3) = ( cod $1) & $2 = ($3 (*) $1);



       A16: for a,b,c be Element of X, f,g be Element of B st R[a, b, f] & R[b, c, g] holds F(g,f) in B & R[a, c, F(g,f)]

      proof

        let a,b,c be Element of (o Hom ), f,g be Morphism of C;

        assume that

         A17: ( dom f) = ( cod a) and

         A18: (f (*) a) = b and

         A19: ( dom g) = ( cod b) and

         A20: (g (*) b) = c;

        ( dom g) = ( cod f) by A17, A18, A19, CAT_1: 17;

        hence thesis by A17, A18, A20, CAT_1: 17, CAT_1: 18;

      end;



       A21: for a be Element of X holds ex f be Element of B st R[a, a, f] & for b be Element of X, g be Element of B holds ( R[a, b, g] implies F(g,f) = g) & ( R[b, a, g] implies F(f,g) = g)

      proof

        let a be Element of (o Hom );

        take f = ( id ( cod a));

        thus ( dom f) = ( cod a) & (f (*) a) = a by CAT_1: 21;

        let b be Element of (o Hom ), g be Morphism of C;

        thus ( dom g) = ( cod a) & (g (*) a) = b implies (g (*) f) = g by CAT_1: 22;

        assume that

         A22: ( dom g) = ( cod b) and

         A23: (g (*) b) = a;

        ( cod g) = ( cod a) by A22, A23, CAT_1: 17;

        hence thesis by CAT_1: 21;

      end;



       A24: for a,b,c,d be Element of X, f,g,h be Element of B st R[a, b, f] & R[b, c, g] & R[c, d, h] holds F(h,F) = F(F,f)

      proof

        let a,b,c,d be Element of (o Hom ), f,g,h be Morphism of C;

        assume that

         A25: ( dom f) = ( cod a) and

         A26: (f (*) a) = b and

         A27: ( dom g) = ( cod b) and

         A28: (g (*) b) = c and

         A29: ( dom h) = ( cod c) and (h (*) c) = d;



         A30: ( dom g) = ( cod f) by A25, A26, A27, CAT_1: 17;

        ( dom h) = ( cod g) by A27, A28, A29, CAT_1: 17;

        hence thesis by A30, CAT_1: 18;

      end;

      :: CAT_5:def12

      func o -SliceCat (C) -> strict with_triple-like_morphisms Category means

      : Def12: the carrier of it = (o Hom ) & (for a,b be Element of (o Hom ), f be Morphism of C st ( dom f) = ( cod a) & (f (*) a) = b holds [ [a, b], f] is Morphism of it ) & (for m be Morphism of it holds ex a,b be Element of (o Hom ), f be Morphism of C st m = [ [a, b], f] & ( dom f) = ( cod a) & (f (*) a) = b) & for m1,m2 be Morphism of it , a1,a2,a3 be Element of (o Hom ), f1,f2 be Morphism of C st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], (f2 (*) f1)];

      existence

      proof

        thus ex F be with_triple-like_morphisms strict Category st the carrier of F = X & (for a,b be Element of X, f be Element of B st R[a, b, f] holds [ [a, b], f] is Morphism of F) & (for m be Morphism of F holds ex a,b be Element of X, f be Element of B st m = [ [a, b], f] & R[a, b, f]) & for m1,m2 be Morphism of F, a1,a2,a3 be Element of X, f1,f2 be Element of B st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)] from CatEx( A16, A21, A24);

      end;

      uniqueness

      proof

        thus for C1,C2 be strict with_triple-like_morphisms Category st the carrier of C1 = X & (for a,b be Element of X, f be Element of B st R[a, b, f] holds [ [a, b], f] is Morphism of C1) & (for m be Morphism of C1 holds ex a,b be Element of X, f be Element of B st m = [ [a, b], f] & R[a, b, f]) & (for m1,m2 be Morphism of C1, a1,a2,a3 be Element of X, f1,f2 be Element of B st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)]) & the carrier of C2 = X & (for a,b be Element of X, f be Element of B st R[a, b, f] holds [ [a, b], f] is Morphism of C2) & (for m be Morphism of C2 holds ex a,b be Element of X, f be Element of B st m = [ [a, b], f] & R[a, b, f]) & for m1,m2 be Morphism of C2, a1,a2,a3 be Element of X, f1,f2 be Element of B st m1 = [ [a1, a2], f1] & m2 = [ [a2, a3], f2] holds (m2 (*) m1) = [ [a1, a3], F(f2,f1)] holds C1 = C2 from CatUniq( A21);

      end;

    end

    definition

      let C be Category;

      let o be Object of C;

      let m be Morphism of (C -SliceCat o);

      :: original: `2

      redefine

      func m `2 -> Morphism of C ;

      coherence

      proof

        ex a,b be Element of ( Hom o), f be Morphism of C st (m = [ [a, b], f]) & (( dom b) = ( cod f)) & (a = (b (*) f)) by Def11;

        hence thesis;

      end;

      :: original: `11

      redefine

      func m `11 -> Element of ( Hom o) ;

      coherence

      proof

        ex a,b be Element of ( Hom o), f be Morphism of C st (m = [ [a, b], f]) & (( dom b) = ( cod f)) & (a = (b (*) f)) by Def11;

        hence thesis by MCART_1: 85;

      end;

      :: original: `12

      redefine

      func m `12 -> Element of ( Hom o) ;

      coherence

      proof

        ex a,b be Element of ( Hom o), f be Morphism of C st (m = [ [a, b], f]) & (( dom b) = ( cod f)) & (a = (b (*) f)) by Def11;

        hence thesis by MCART_1: 85;

      end;

    end

    theorem :: CAT_5:29



     Th29: for C be Category, a be Object of C, m be Morphism of (C -SliceCat a) holds m = [ [(m `11 ), (m `12 )], (m `2 )] & ( dom (m `12 )) = ( cod (m `2 )) & (m `11 ) = ((m `12 ) (*) (m `2 )) & ( dom m) = (m `11 ) & ( cod m) = (m `12 )

    proof

      let C be Category, o be Object of C, m be Morphism of (C -SliceCat o);

      consider a,b be Element of ( Hom o), f be Morphism of C such that

       A1: m = [ [a, b], f] and

       A2: ( dom b) = ( cod f) and

       A3: a = (b (*) f) by Def11;



       A4: (m `11 ) = a by A1, MCART_1: 85;

      (m `12 ) = b by A1, MCART_1: 85;

      hence thesis by A1, A2, A3, A4, Th2;

    end;

    theorem :: CAT_5:30



     Th30: for C be Category, o be Object of C, f be Element of ( Hom o) holds for a be Object of (C -SliceCat o) st a = f holds ( id a) = [ [a, a], ( id ( dom f))]

    proof

      let C be Category, o be Object of C, f be Element of ( Hom o);

      let a be Object of (C -SliceCat o);

      assume

       A1: a = f;

      consider b,c be Element of ( Hom o), g be Morphism of C such that

       A2: ( id a) = [ [b, c], g] and

       A3: ( dom c) = ( cod g) and b = (c (*) g) by Def11;



       A4: ( cod ( id ( dom f))) = ( dom f);

      f = (f (*) ( id ( dom f))) by CAT_1: 22;

      then

      reconsider h = [ [f, f], ( id ( dom f))] as Morphism of (C -SliceCat o) by A4, Def11;



       A5: (( id a) `11 ) = b by A2, MCART_1: 85;



       A6: (( id a) `12 ) = c by A2, MCART_1: 85;



       A7: ( dom ( id a)) = b by A5, Th2;



       A8: ( cod ( id a)) = c by A6, Th2;



       A9: b = a by A7;



       A10: c = a by A8;

      ( dom h) = (h `11 ) by Th2

      .= a by A1, MCART_1: 85;



      then h = (h (*) ( id a)) by CAT_1: 22

      .= [ [f, f], (( id ( dom f)) (*) g)] by A1, A2, A9, A10, Def11

      .= [ [f, f], g] by A1, A3, A10, CAT_1: 21;

      hence thesis by A1, A2, A7, A10;

    end;

    definition

      let C be Category;

      let o be Object of C;

      let m be Morphism of (o -SliceCat C);

      :: original: `2

      redefine

      func m `2 -> Morphism of C ;

      coherence

      proof

        ex a,b be Element of (o Hom ), f be Morphism of C st (m = [ [a, b], f]) & (( dom f) = ( cod a)) & ((f (*) a) = b) by Def12;

        hence thesis;

      end;

      :: original: `11

      redefine

      func m `11 -> Element of (o Hom ) ;

      coherence

      proof

        ex a,b be Element of (o Hom ), f be Morphism of C st (m = [ [a, b], f]) & (( dom f) = ( cod a)) & ((f (*) a) = b) by Def12;

        hence thesis by MCART_1: 85;

      end;

      :: original: `12

      redefine

      func m `12 -> Element of (o Hom ) ;

      coherence

      proof

        ex a,b be Element of (o Hom ), f be Morphism of C st (m = [ [a, b], f]) & (( dom f) = ( cod a)) & ((f (*) a) = b) by Def12;

        hence thesis by MCART_1: 85;

      end;

    end

    theorem :: CAT_5:31



     Th31: for C be Category, a be Object of C, m be Morphism of (a -SliceCat C) holds m = [ [(m `11 ), (m `12 )], (m `2 )] & ( dom (m `2 )) = ( cod (m `11 )) & ((m `2 ) (*) (m `11 )) = (m `12 ) & ( dom m) = (m `11 ) & ( cod m) = (m `12 )

    proof

      let C be Category, o be Object of C, m be Morphism of (o -SliceCat C);

      consider a,b be Element of (o Hom ), f be Morphism of C such that

       A1: m = [ [a, b], f] and

       A2: ( dom f) = ( cod a) and

       A3: (f (*) a) = b by Def12;



       A4: (m `11 ) = a by A1, MCART_1: 85;

      (m `12 ) = b by A1, MCART_1: 85;

      hence thesis by A1, A2, A3, A4, Th2;

    end;

    theorem :: CAT_5:32



     Th32: for C be Category, o be Object of C, f be Element of (o Hom ) holds for a be Object of (o -SliceCat C) st a = f holds ( id a) = [ [a, a], ( id ( cod f))]

    proof

      let C be Category, o be Object of C, f be Element of (o Hom );

      let a be Object of (o -SliceCat C);

      assume

       A1: a = f;

      consider b,c be Element of (o Hom ), g be Morphism of C such that

       A2: ( id a) = [ [b, c], g] and

       A3: ( dom g) = ( cod b) and (g (*) b) = c by Def12;



       A4: ( dom ( id ( cod f))) = ( cod f);

      f = (( id ( cod f)) (*) f) by CAT_1: 21;

      then

      reconsider h = [ [f, f], ( id ( cod f))] as Morphism of (o -SliceCat C) by A4, Def12;



       A5: (( id a) `11 ) = b by A2, MCART_1: 85;



       A6: (( id a) `12 ) = c by A2, MCART_1: 85;



       A7: ( dom ( id a)) = b by A5, Th2;



       A8: ( cod ( id a)) = c by A6, Th2;



       A9: b = a by A7;



       A10: c = a by A8;

      ( cod h) = (h `12 ) by Th2

      .= a by A1, MCART_1: 85;



      then h = (( id a) (*) h) by CAT_1: 21

      .= [ [f, f], (g (*) ( id ( cod f)))] by A1, A2, A9, A10, Def12

      .= [ [f, f], g] by A1, A3, A9, CAT_1: 22;

      hence thesis by A1, A2, A8, A9;

    end;

    begin

    definition

      let C be Category, f be Morphism of C;

      :: CAT_5:def13

      func SliceFunctor f -> Functor of (C -SliceCat ( dom f)), (C -SliceCat ( cod f)) means

      : Def13: for m be Morphism of (C -SliceCat ( dom f)) holds (it . m) = [ [(f (*) (m `11 )), (f (*) (m `12 ))], (m `2 )];

      existence

      proof

        set C1 = (C -SliceCat ( dom f)), C2 = (C -SliceCat ( cod f));

        deffunc f( Morphism of C1) = [ [(f (*) ($1 `11 )), (f (*) ($1 `12 ))], ($1 `2 )];

        consider F be Function of the carrier' of C1, the carrier' of [: [:C, C:], C:] such that

         A1: for m be Morphism of C1 holds (F . m) = f(m) from FUNCT_2:sch 4;



         A2: ( dom F) = the carrier' of C1 by FUNCT_2:def 1;

        ( rng F) c= the carrier' of C2

        proof

          let x be object;

          assume x in ( rng F);

          then

          consider m be object such that

           A3: m in ( dom F) and

           A4: x = (F . m) by FUNCT_1:def 3;

          reconsider m as Morphism of C1 by A3;



           A5: x = [ [(f (*) (m `11 )), (f (*) (m `12 ))], (m `2 )] by A1, A4;



           A6: ( dom (m `12 )) = ( cod (m `2 )) by Th29;



           A7: (m `11 ) = ((m `12 ) (*) (m `2 )) by Th29;



           A8: ( cod (m `12 )) = ( dom f) by Th23;



           A9: (f (*) (m `11 )) in ( Hom ( cod f)) by Th27;



           A10: (f (*) (m `12 )) in ( Hom ( cod f)) by Th27;



           A11: ( dom (f (*) (m `12 ))) = ( cod (m `2 )) by A6, A8, CAT_1: 17;

          (f (*) (m `11 )) = ((f (*) (m `12 )) (*) (m `2 )) by A6, A7, A8, CAT_1: 18;

          then x is Morphism of C2 by A5, A9, A10, A11, Def11;

          hence thesis;

        end;

        then

        reconsider F as Function of the carrier' of C1, the carrier' of C2 by A2, FUNCT_2:def 1, RELSET_1: 4;

         A12:

        now

          let c be Object of C1;

          reconsider g = c as Element of ( Hom ( dom f)) by Def11;

          reconsider h = (f (*) g) as Element of ( Hom ( cod f)) by Th27;

          reconsider d = h as Object of C2 by Def11;

          take d;



           A13: ( id c) = [ [c, c], ( id ( dom g))] by Th30;



           A14: ( id d) = [ [d, d], ( id ( dom h))] by Th30;



           A15: (( id c) `11 ) = c by A13, MCART_1: 85;



           A16: (( id c) `12 ) = c by A13, MCART_1: 85;



           A17: (( id c) `2 ) = ( id ( dom g)) by A13;



           A18: ( cod g) = ( dom f) by Th23;



          thus (F . ( id c)) = [ [h, h], (( id c) `2 )] by A1, A15, A16

          .= ( id d) by A14, A17, A18, CAT_1: 17;

        end;

         A19:

        now

          let m be Morphism of C1;

          reconsider g1 = (f (*) (m `11 )), g2 = (f (*) (m `12 )) as Element of ( Hom ( cod f)) by Th27;



           A20: ( dom f) = ( cod (m `11 )) by Th23;



           A21: ( dom f) = ( cod (m `12 )) by Th23;

          (F . m) = [ [g1, g2], (m `2 )] by A1;



          then ( dom (F . m)) = ( [ [g1, g2], (m `2 )] `11 ) by Th29

          .= g1 by MCART_1: 85;

          then

           A22: ( id ( dom (F . m))) = [ [g1, g1], ( id ( dom g1))] by Th30;

          ( dom m) = (m `11 ) by Th29;

          then

           A23: ( id ( dom m)) = [ [(m `11 ), (m `11 )], ( id ( dom (m `11 )))] by Th30;

          then

           A24: (( id ( dom m)) `11 ) = (m `11 ) by MCART_1: 85;



           A25: (( id ( dom m)) `12 ) = (m `11 ) by A23, MCART_1: 85;

          (( id ( dom m)) `2 ) = ( id ( dom (m `11 ))) by A23;



          hence (F . ( id ( dom m))) = [ [g1, g1], ( id ( dom (m `11 )))] by A1, A24, A25

          .= ( id ( dom (F . m))) by A20, A22, CAT_1: 17;

          (F . m) = [ [g1, g2], (m `2 )] by A1;



          then ( cod (F . m)) = ( [ [g1, g2], (m `2 )] `12 ) by Th29

          .= g2 by MCART_1: 85;

          then

           A26: ( id ( cod (F . m))) = [ [g2, g2], ( id ( dom g2))] by Th30;

          ( cod m) = (m `12 ) by Th29;

          then

           A27: ( id ( cod m)) = [ [(m `12 ), (m `12 )], ( id ( dom (m `12 )))] by Th30;

          then

           A28: (( id ( cod m)) `11 ) = (m `12 ) by MCART_1: 85;



           A29: (( id ( cod m)) `12 ) = (m `12 ) by A27, MCART_1: 85;

          (( id ( cod m)) `2 ) = ( id ( dom (m `12 ))) by A27;



          hence (F . ( id ( cod m))) = [ [g2, g2], ( id ( dom (m `12 )))] by A1, A28, A29

          .= ( id ( cod (F . m))) by A21, A26, CAT_1: 17;

        end;

        now

          let f1,f2 be Morphism of C1;

          consider a1,b1 be Element of ( Hom ( dom f)), g1 be Morphism of C such that

           A30: f1 = [ [a1, b1], g1] and ( dom b1) = ( cod g1) and a1 = (b1 (*) g1) by Def11;

          consider a2,b2 be Element of ( Hom ( dom f)), g2 be Morphism of C such that

           A31: f2 = [ [a2, b2], g2] and ( dom b2) = ( cod g2) and a2 = (b2 (*) g2) by Def11;



           A32: ( dom f2) = (f2 `11 ) by Th2;



           A33: ( cod f1) = (f1 `12 ) by Th2;



           A34: ( dom f2) = a2 by A31, A32, MCART_1: 85;



           A35: ( cod f1) = b1 by A30, A33, MCART_1: 85;

          reconsider ha1 = (f (*) a1), ha2 = (f (*) a2), hb1 = (f (*) b1), hb2 = (f (*) b2) as Element of ( Hom ( cod f)) by Th27;



           A36: (f1 `11 ) = a1 by A30, MCART_1: 85;



           A37: (f1 `12 ) = b1 by A30, MCART_1: 85;



           A38: (f1 `2 ) = g1 by A30;



           A39: (f2 `11 ) = a2 by A31, MCART_1: 85;



           A40: (f2 `12 ) = b2 by A31, MCART_1: 85;



           A41: (f2 `2 ) = g2 by A31;



           A42: (F . f1) = [ [ha1, hb1], g1] by A1, A36, A37, A38;



           A43: (F . f2) = [ [ha2, hb2], g2] by A1, A39, A40, A41;

          assume

           A44: ( dom f2) = ( cod f1);

          then

           A45: (f2 (*) f1) = [ [a1, b2], (g2 (*) g1)] by A30, A31, A34, A35, Def11;



           A46: ((F . f2) (*) (F . f1)) = [ [ha1, hb2], (g2 (*) g1)] by A34, A35, A42, A43, A44, Def11;



           A47: ((f2 (*) f1) `11 ) = a1 by A45, MCART_1: 85;



           A48: ((f2 (*) f1) `12 ) = b2 by A45, MCART_1: 85;

          ((f2 (*) f1) `2 ) = (g2 (*) g1) by A45;

          hence (F . (f2 (*) f1)) = ((F . f2) (*) (F . f1)) by A1, A46, A47, A48;

        end;

        then

        reconsider F as Functor of C1, C2 by A12, A19, CAT_1: 61;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be Functor of (C -SliceCat ( dom f)), (C -SliceCat ( cod f)) such that

         A49: for m be Morphism of (C -SliceCat ( dom f)) holds (F1 . m) = [ [(f (*) (m `11 )), (f (*) (m `12 ))], (m `2 )] and

         A50: for m be Morphism of (C -SliceCat ( dom f)) holds (F2 . m) = [ [(f (*) (m `11 )), (f (*) (m `12 ))], (m `2 )];

        now

          let m be Morphism of (C -SliceCat ( dom f));



          thus (F1 . m) = [ [(f (*) (m `11 )), (f (*) (m `12 ))], (m `2 )] by A49

          .= (F2 . m) by A50;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      :: CAT_5:def14

      func SliceContraFunctor f -> Functor of (( cod f) -SliceCat C), (( dom f) -SliceCat C) means

      : Def14: for m be Morphism of (( cod f) -SliceCat C) holds (it . m) = [ [((m `11 ) (*) f), ((m `12 ) (*) f)], (m `2 )];

      existence

      proof

        set C1 = (( cod f) -SliceCat C), C2 = (( dom f) -SliceCat C);

        deffunc f( Morphism of C1) = [ [(($1 `11 ) (*) f), (($1 `12 ) (*) f)], ($1 `2 )];

        consider F be Function of the carrier' of C1, the carrier' of [: [:C, C:], C:] such that

         A51: for m be Morphism of C1 holds (F . m) = f(m) from FUNCT_2:sch 4;



         A52: ( dom F) = the carrier' of C1 by FUNCT_2:def 1;

        ( rng F) c= the carrier' of C2

        proof

          let x be object;

          assume x in ( rng F);

          then

          consider m be object such that

           A53: m in ( dom F) and

           A54: x = (F . m) by FUNCT_1:def 3;

          reconsider m as Morphism of C1 by A53;



           A55: x = [ [((m `11 ) (*) f), ((m `12 ) (*) f)], (m `2 )] by A51, A54;



           A56: ( dom (m `2 )) = ( cod (m `11 )) by Th31;



           A57: (m `12 ) = ((m `2 ) (*) (m `11 )) by Th31;



           A58: ( dom (m `11 )) = ( cod f) by Th24;



           A59: ((m `11 ) (*) f) in (( dom f) Hom ) by Th28;



           A60: ((m `12 ) (*) f) in (( dom f) Hom ) by Th28;



           A61: ( cod ((m `11 ) (*) f)) = ( dom (m `2 )) by A56, A58, CAT_1: 17;

          ((m `12 ) (*) f) = ((m `2 ) (*) ((m `11 ) (*) f)) by A56, A57, A58, CAT_1: 18;

          then x is Morphism of C2 by A55, A59, A60, A61, Def12;

          hence thesis;

        end;

        then

        reconsider F as Function of the carrier' of C1, the carrier' of C2 by A52, FUNCT_2:def 1, RELSET_1: 4;

         A62:

        now

          let c be Object of C1;

          reconsider g = c as Element of (( cod f) Hom ) by Def12;

          reconsider h = (g (*) f) as Element of (( dom f) Hom ) by Th28;

          reconsider d = h as Object of C2 by Def12;

          take d;



           A63: ( id c) = [ [c, c], ( id ( cod g))] by Th32;



           A64: ( id d) = [ [d, d], ( id ( cod h))] by Th32;



           A65: (( id c) `11 ) = c by A63, MCART_1: 85;



           A66: (( id c) `12 ) = c by A63, MCART_1: 85;



           A67: (( id c) `2 ) = ( id ( cod g)) by A63;



           A68: ( dom g) = ( cod f) by Th24;



          thus (F . ( id c)) = [ [h, h], (( id c) `2 )] by A51, A65, A66

          .= ( id d) by A64, A67, A68, CAT_1: 17;

        end;

         A69:

        now

          let m be Morphism of C1;

          reconsider g1 = ((m `11 ) (*) f), g2 = ((m `12 ) (*) f) as Element of (( dom f) Hom ) by Th28;



           A70: ( cod f) = ( dom (m `11 )) by Th24;



           A71: ( cod f) = ( dom (m `12 )) by Th24;

          (F . m) = [ [g1, g2], (m `2 )] by A51;



          then ( dom (F . m)) = ( [ [g1, g2], (m `2 )] `11 ) by Th31

          .= g1 by MCART_1: 85;

          then

           A72: ( id ( dom (F . m))) = [ [g1, g1], ( id ( cod g1))] by Th32;

          ( dom m) = (m `11 ) by Th31;

          then

           A73: ( id ( dom m)) = [ [(m `11 ), (m `11 )], ( id ( cod (m `11 )))] by Th32;

          then

           A74: (( id ( dom m)) `11 ) = (m `11 ) by MCART_1: 85;



           A75: (( id ( dom m)) `12 ) = (m `11 ) by A73, MCART_1: 85;

          (( id ( dom m)) `2 ) = ( id ( cod (m `11 ))) by A73;



          hence (F . ( id ( dom m))) = [ [g1, g1], ( id ( cod (m `11 )))] by A51, A74, A75

          .= ( id ( dom (F . m))) by A70, A72, CAT_1: 17;

          (F . m) = [ [g1, g2], (m `2 )] by A51;



          then ( cod (F . m)) = ( [ [g1, g2], (m `2 )] `12 ) by Th31

          .= g2 by MCART_1: 85;

          then

           A76: ( id ( cod (F . m))) = [ [g2, g2], ( id ( cod g2))] by Th32;

          ( cod m) = (m `12 ) by Th31;

          then

           A77: ( id ( cod m)) = [ [(m `12 ), (m `12 )], ( id ( cod (m `12 )))] by Th32;

          then

           A78: (( id ( cod m)) `11 ) = (m `12 ) by MCART_1: 85;



           A79: (( id ( cod m)) `12 ) = (m `12 ) by A77, MCART_1: 85;

          (( id ( cod m)) `2 ) = ( id ( cod (m `12 ))) by A77;



          hence (F . ( id ( cod m))) = [ [g2, g2], ( id ( cod (m `12 )))] by A51, A78, A79

          .= ( id ( cod (F . m))) by A71, A76, CAT_1: 17;

        end;

        now

          let f1,f2 be Morphism of C1;

          consider a1,b1 be Element of (( cod f) Hom ), g1 be Morphism of C such that

           A80: f1 = [ [a1, b1], g1] and ( dom g1) = ( cod a1) and (g1 (*) a1) = b1 by Def12;

          consider a2,b2 be Element of (( cod f) Hom ), g2 be Morphism of C such that

           A81: f2 = [ [a2, b2], g2] and ( dom g2) = ( cod a2) and (g2 (*) a2) = b2 by Def12;



           A82: ( dom f2) = (f2 `11 ) by Th2;



           A83: ( cod f1) = (f1 `12 ) by Th2;



           A84: ( dom f2) = a2 by A81, A82, MCART_1: 85;



           A85: ( cod f1) = b1 by A80, A83, MCART_1: 85;

          reconsider ha1 = (a1 (*) f), ha2 = (a2 (*) f), hb1 = (b1 (*) f), hb2 = (b2 (*) f) as Element of (( dom f) Hom ) by Th28;



           A86: (f1 `11 ) = a1 by A80, MCART_1: 85;



           A87: (f1 `12 ) = b1 by A80, MCART_1: 85;



           A88: (f1 `2 ) = g1 by A80;



           A89: (f2 `11 ) = a2 by A81, MCART_1: 85;



           A90: (f2 `12 ) = b2 by A81, MCART_1: 85;



           A91: (f2 `2 ) = g2 by A81;



           A92: (F . f1) = [ [ha1, hb1], g1] by A51, A86, A87, A88;



           A93: (F . f2) = [ [ha2, hb2], g2] by A51, A89, A90, A91;

          assume

           A94: ( dom f2) = ( cod f1);

          then

           A95: (f2 (*) f1) = [ [a1, b2], (g2 (*) g1)] by A80, A81, A84, A85, Def12;



           A96: ((F . f2) (*) (F . f1)) = [ [ha1, hb2], (g2 (*) g1)] by A84, A85, A92, A93, A94, Def12;



           A97: ((f2 (*) f1) `11 ) = a1 by A95, MCART_1: 85;



           A98: ((f2 (*) f1) `12 ) = b2 by A95, MCART_1: 85;

          ((f2 (*) f1) `2 ) = (g2 (*) g1) by A95;

          hence (F . (f2 (*) f1)) = ((F . f2) (*) (F . f1)) by A51, A96, A97, A98;

        end;

        then

        reconsider F as Functor of C1, C2 by A62, A69, CAT_1: 61;

        take F;

        thus thesis by A51;

      end;

      uniqueness

      proof

        let F1,F2 be Functor of (( cod f) -SliceCat C), (( dom f) -SliceCat C) such that

         A99: for m be Morphism of (( cod f) -SliceCat C) holds (F1 . m) = [ [((m `11 ) (*) f), ((m `12 ) (*) f)], (m `2 )] and

         A100: for m be Morphism of (( cod f) -SliceCat C) holds (F2 . m) = [ [((m `11 ) (*) f), ((m `12 ) (*) f)], (m `2 )];

        now

          let m be Morphism of (( cod f) -SliceCat C);



          thus (F1 . m) = [ [((m `11 ) (*) f), ((m `12 ) (*) f)], (m `2 )] by A99

          .= (F2 . m) by A100;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: CAT_5:33

    for C be Category, f,g be Morphism of C st ( dom g) = ( cod f) holds ( SliceFunctor (g (*) f)) = (( SliceFunctor g) * ( SliceFunctor f))

    proof

      let C be Category, f,g be Morphism of C;

      assume

       A1: ( dom g) = ( cod f);

      then

       A2: ( dom (g (*) f)) = ( dom f) by CAT_1: 17;

      set A1 = (C -SliceCat ( dom f)), A3 = (C -SliceCat ( cod g));

      set F = ( SliceFunctor f);

      reconsider G = ( SliceFunctor g) as Functor of (C -SliceCat ( cod f)), A3 by A1;

      reconsider GF = ( SliceFunctor (g (*) f)) as Functor of A1, A3 by A1, A2, CAT_1: 17;

      now

        let m be Morphism of A1;



         A3: (F . m) = [ [(f (*) (m `11 )), (f (*) (m `12 ))], (m `2 )] by Def13;

        then

         A4: ((F . m) `11 ) = (f (*) (m `11 )) by MCART_1: 85;



         A5: ((F . m) `12 ) = (f (*) (m `12 )) by A3, MCART_1: 85;



         A6: ((F . m) `2 ) = (m `2 ) by A3;



         A7: ( dom f) = ( cod (m `11 )) by Th23;



         A8: ( dom f) = ( cod (m `12 )) by Th23;



         A9: (g (*) (f (*) (m `11 ))) = ((g (*) f) (*) (m `11 )) by A1, A7, CAT_1: 18;



         A10: (g (*) (f (*) (m `12 ))) = ((g (*) f) (*) (m `12 )) by A1, A8, CAT_1: 18;



        thus ((G * F) . m) = (G . (F . m)) by FUNCT_2: 15

        .= [ [(g (*) (f (*) (m `11 ))), (g (*) (f (*) (m `12 )))], (m `2 )] by A1, A4, A5, A6, Def13

        .= (GF . m) by A2, A9, A10, Def13;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CAT_5:34

    for C be Category, f,g be Morphism of C st ( dom g) = ( cod f) holds ( SliceContraFunctor (g (*) f)) = (( SliceContraFunctor f) * ( SliceContraFunctor g))

    proof

      let C be Category, f,g be Morphism of C;

      assume

       A1: ( dom g) = ( cod f);

      then

       A2: ( cod (g (*) f)) = ( cod g) by CAT_1: 17;

      set A1 = (( dom f) -SliceCat C), A2 = (( cod f) -SliceCat C);

      set A3 = (( cod g) -SliceCat C);

      reconsider F = ( SliceContraFunctor f) as Functor of A2, A1;

      reconsider G = ( SliceContraFunctor g) as Functor of A3, A2 by A1;

      reconsider FG = ( SliceContraFunctor (g (*) f)) as Functor of A3, A1 by A1, A2, CAT_1: 17;

      now

        let m be Morphism of A3;



         A3: (G . m) = [ [((m `11 ) (*) g), ((m `12 ) (*) g)], (m `2 )] by Def14;

        then

         A4: ((G . m) `11 ) = ((m `11 ) (*) g) by MCART_1: 85;



         A5: ((G . m) `12 ) = ((m `12 ) (*) g) by A3, MCART_1: 85;



         A6: ((G . m) `2 ) = (m `2 ) by A3;



         A7: ( cod g) = ( dom (m `11 )) by Th24;



         A8: ( cod g) = ( dom (m `12 )) by Th24;



         A9: ((m `11 ) (*) (g (*) f)) = (((m `11 ) (*) g) (*) f) by A1, A7, CAT_1: 18;



         A10: ((m `12 ) (*) (g (*) f)) = (((m `12 ) (*) g) (*) f) by A1, A8, CAT_1: 18;



        thus ((F * G) . m) = (F . (G . m)) by FUNCT_2: 15

        .= [ [(((m `11 ) (*) g) (*) f), (((m `12 ) (*) g) (*) f)], (m `2 )] by A4, A5, A6, Def14

        .= (FG . m) by A2, A9, A10, Def14;

      end;

      hence thesis by FUNCT_2: 63;

    end;