isocat_2.miz



    begin

    definition

      let A,B,C be non empty set;

      let f be Function of A, ( Funcs (B,C));

      :: original: uncurry

      redefine

      func uncurry f -> Function of [:A, B:], C ;

      coherence

      proof

        

         A1: ( rng f) c= ( Funcs (B,C));

        ( dom ( uncurry f)) = [:( dom f), B:] by A1, FUNCT_5: 26

        .= [:A, B:] by FUNCT_2:def 1;

        hence thesis;

      end;

    end

    theorem :: ISOCAT_2:1

    

     Th1: for A,B,C be non empty set, f be Function of A, ( Funcs (B,C)) holds ( curry ( uncurry f)) = f

    proof

      let A,B,C be non empty set, f be Function of A, ( Funcs (B,C));

      ( rng f) c= ( Funcs (B,C));

      hence thesis by FUNCT_5: 48;

    end;

    theorem :: ISOCAT_2:2

    

     Th2: for A,B,C be non empty set, f be Function of A, ( Funcs (B,C)) holds for a be Element of A, b be Element of B holds (( uncurry f) . (a,b)) = ((f . a) . b)

    proof

      let A,B,C be non empty set, f be Function of A, ( Funcs (B,C));

      let a be Element of A, b be Element of B;

      ( dom f) = A & ( dom (f . a)) = B by FUNCT_2:def 1;

      hence thesis by FUNCT_5: 38;

    end;

    ::$Canceled

    reserve A,B,C for Category,

F,F1 for Functor of A, B;

    theorem :: ISOCAT_2:5

    

     Th3: for f be Morphism of A holds (( id ( cod f)) (*) f) = f

    proof

      let f be Morphism of A;

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

      

       A1: ( Hom (( dom f),( cod f))) <> {} by CAT_1: 2;

      ( Hom (( cod f),( cod f))) <> {} ;

      

      hence (( id ( cod f)) (*) f) = (( id ( cod f)) * f9) by A1, CAT_1:def 13

      .= f by A1, CAT_1: 28;

    end;

    theorem :: ISOCAT_2:6

    

     Th4: for f be Morphism of A holds (f (*) ( id ( dom f))) = f

    proof

      let f be Morphism of A;

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

      

       A1: ( Hom (( dom f),( cod f))) <> {} by CAT_1: 2;

      ( Hom (( dom f),( dom f))) <> {} ;

      

      hence (f (*) ( id ( dom f))) = (f9 * ( id ( dom f))) by A1, CAT_1:def 13

      .= f by A1, CAT_1: 29;

    end;

    reserve o,m for set;

    reserve t for natural_transformation of F, F1;

    theorem :: ISOCAT_2:7

    

     Th5: o is Object of ( Functors (A,B)) iff o is Functor of A, B

    proof

      the carrier of ( Functors (A,B)) = ( Funct (A,B)) by NATTRA_1:def 17;

      hence thesis by CAT_2:def 2;

    end;

    theorem :: ISOCAT_2:8

    

     Th6: for f be Morphism of ( Functors (A,B)) holds ex F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 st F1 is_naturally_transformable_to F2 & ( dom f) = F1 & ( cod f) = F2 & f = [ [F1, F2], t]

    proof

      let m be Morphism of ( Functors (A,B));

      ( Hom (( dom m),( cod m))) <> {} & m is Morphism of ( dom m), ( cod m) by CAT_1: 2, CAT_1: 4;

      then

      consider F, F1, t such that

       A1: ( dom m) = F & ( cod m) = F1 and

       A2: m = [ [F, F1], t] by NATTRA_1: 34;

      take F, F1, t;

      the carrier' of ( Functors (A,B)) = ( NatTrans (A,B)) by NATTRA_1:def 17;

      hence F is_naturally_transformable_to F1 by A2, NATTRA_1: 32;

      thus thesis by A1, A2;

    end;

    begin

    definition

      let A, B;

      let a be Object of A;

      :: ISOCAT_2:def1

      func a |-> B -> Functor of ( Functors (A,B)), B means

      : Def1: for F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 st F1 is_naturally_transformable_to F2 holds (it . [ [F1, F2], t]) = (t . a);

      existence

      proof

        defpred P[ set, set] means for F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 st $1 = [ [F1, F2], t] holds $2 = (t . a);

        

         A1: the carrier' of ( Functors (A,B)) = ( NatTrans (A,B)) by NATTRA_1:def 17;

         A2:

        now

          let x be Element of ( NatTrans (A,B));

          consider F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 such that

           A3: x = [ [F1, F2], t] and F1 is_naturally_transformable_to F2 by NATTRA_1:def 16;

          reconsider b = (t . a) as Morphism of B;

          take b;

          thus P[x, b]

          proof

            let F19,F29 be Functor of A, B, t9 be natural_transformation of F19, F29;

            assume

             A4: x = [ [F19, F29], t9];

            then [F1, F2] = [F19, F29] by A3, XTUPLE_0: 1;

            then F1 = F19 & F2 = F29 by XTUPLE_0: 1;

            hence thesis by A3, A4, XTUPLE_0: 1;

          end;

        end;

        consider f be Function of ( NatTrans (A,B)), the carrier' of B such that

         A5: for x be Element of ( NatTrans (A,B)) holds P[x, (f . x)] from FUNCT_2:sch 3( A2);

        

         A6: the carrier' of ( Functors (A,B)) = ( NatTrans (A,B)) by NATTRA_1:def 17;

        then

        reconsider ff = f as Function of the carrier' of ( Functors (A,B)), the carrier' of B;

         A7:

        now

          let c be Object of ( Functors (A,B));

          reconsider F = c as Functor of A, B by Th5;

          take d = (F . a);

          

           A8: [ [F, F], ( id F)] is Morphism of ( Functors (A,B)) by A6, NATTRA_1:def 16;

          

          thus (f . ( id c)) = (f . [ [F, F], ( id F)]) by NATTRA_1:def 17

          .= (( id F) . a) by A5, A6, A8

          .= ( id d) by NATTRA_1: 20;

        end;

         A9:

        now

          let m1,m2 be Morphism of ( Functors (A,B));

          assume

           A10: [m2, m1] in ( dom the Comp of ( Functors (A,B)));

          reconsider m19 = m1, m29 = m2 as Element of ( NatTrans (A,B)) by NATTRA_1:def 17;

          consider F, F1, t such that

           A11: F is_naturally_transformable_to F1 and ( dom m1) = F and ( cod m1) = F1 and

           A12: m1 = [ [F, F1], t] by Th6;

          

           A13: ( Hom ((F . a),(F1 . a))) <> {} by A11, ISOCAT_1: 25;

          

           A14: (f . m19) = (t . a) by A5, A12;

          consider F19,F2 be Functor of A, B, t9 be natural_transformation of F19, F2 such that

           A15: F19 is_naturally_transformable_to F2 and ( dom m2) = F19 and ( cod m2) = F2 and

           A16: m2 = [ [F19, F2], t9] by Th6;

          

           A17: F19 = ( dom m2) by A16, NATTRA_1: 33

          .= ( cod m1) by A10, CAT_1: 15

          .= F1 by A12, NATTRA_1: 33;

          then

          reconsider t9 as natural_transformation of F1, F2;

          

           A18: ( Hom ((F1 . a),(F2 . a))) <> {} by A15, A17, ISOCAT_1: 25;

          

           A19: (f . m29) = (t9 . a) by A5, A16, A17;

          

           A20: (m2 (*) m1) = [ [F, F2], (t9 `*` t)] by A12, A16, A17, NATTRA_1: 36;

          

          thus (ff . (m2 (*) m1)) = ((t9 `*` t) . a) by A5, A6, A20

          .= ((t9 . a) * (t . a)) by A11, A15, A17, NATTRA_1: 25

          .= ((t9 . a) (*) (t . a)) by A13, A18, CAT_1:def 13

          .= ((ff . m2) (*) (ff . m1)) by A14, A19;

        end;

        now

          let m be Morphism of ( Functors (A,B));

          reconsider m9 = m as Element of ( NatTrans (A,B)) by NATTRA_1:def 17;

          consider F, F1, t such that

           A21: F is_naturally_transformable_to F1 and

           A22: ( dom m) = F and

           A23: ( cod m) = F1 and

           A24: m = [ [F, F1], t] by Th6;

          

           A25: ( Hom ((F . a),(F1 . a))) <> {} by A21, ISOCAT_1: 25;

          

           A26: [ [F, F], ( id F)] is Morphism of ( Functors (A,B)) by A6, NATTRA_1:def 16;

          

          thus (f . ( id ( dom m))) = (f . [ [F, F], ( id F)]) by A22, NATTRA_1:def 17

          .= (( id F) . a) by A5, A6, A26

          .= ( id (F . a)) by NATTRA_1: 20

          .= ( id ( dom (t . a))) by A25, CAT_1: 5

          .= ( id ( dom (f . m9))) by A5, A24

          .= ( id ( dom (ff . m)));

          

           A27: [ [F1, F1], ( id F1)] is Morphism of ( Functors (A,B)) by A6, NATTRA_1:def 16;

          

          thus (f . ( id ( cod m))) = (f . [ [F1, F1], ( id F1)]) by A23, NATTRA_1:def 17

          .= (( id F1) . a) by A5, A6, A27

          .= ( id (F1 . a)) by NATTRA_1: 20

          .= ( id ( cod (t . a))) by A25, CAT_1: 5

          .= ( id ( cod (f . m9))) by A5, A24

          .= ( id ( cod (ff . m)));

        end;

        then

        reconsider f as Functor of ( Functors (A,B)), B by A7, A9, CAT_1:def 21;

        take f;

        let F1,F2 be Functor of A, B, t be natural_transformation of F1, F2;

        assume F1 is_naturally_transformable_to F2;

        then [ [F1, F2], t] is Morphism of ( Functors (A,B)) by A1, NATTRA_1: 32;

        hence thesis by A5, A1;

      end;

      uniqueness

      proof

        let f1,f2 be Functor of ( Functors (A,B)), B such that

         A28: for F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 st F1 is_naturally_transformable_to F2 holds (f1 . [ [F1, F2], t]) = (t . a) and

         A29: for F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 st F1 is_naturally_transformable_to F2 holds (f2 . [ [F1, F2], t]) = (t . a);

        now

          let c be Morphism of ( Functors (A,B));

          the carrier' of ( Functors (A,B)) = ( NatTrans (A,B)) by NATTRA_1:def 17;

          then

          consider F1,F2 be Functor of A, B, t be natural_transformation of F1, F2 such that

           A30: c = [ [F1, F2], t] & F1 is_naturally_transformable_to F2 by NATTRA_1:def 15;

          

          thus (f1 . c) = (t . a) by A28, A30

          .= (f2 . c) by A29, A30;

        end;

        hence f1 = f2 by FUNCT_2: 63;

      end;

    end

    theorem :: ISOCAT_2:9

    ( Functors (( 1Cat (o,m)),A)) ~= A

    proof

      reconsider a = o as Object of ( 1Cat (o,m)) by TARSKI:def 1;

      take F = (a |-> A);

      now

        let x,y be object;

        

         A1: the carrier' of ( Functors (( 1Cat (o,m)),A)) = ( NatTrans (( 1Cat (o,m)),A)) by NATTRA_1:def 17;

        assume x in the carrier' of ( Functors (( 1Cat (o,m)),A));

        then

        consider F1,F2 be Functor of ( 1Cat (o,m)), A, t be natural_transformation of F1, F2 such that

         A2: x = [ [F1, F2], t] and

         A3: F1 is_naturally_transformable_to F2 by A1, NATTRA_1:def 16;

        assume y in the carrier' of ( Functors (( 1Cat (o,m)),A));

        then

        consider F19,F29 be Functor of ( 1Cat (o,m)), A, t9 be natural_transformation of F19, F29 such that

         A4: y = [ [F19, F29], t9] and

         A5: F19 is_naturally_transformable_to F29 by A1, NATTRA_1:def 16;

        assume (F . x) = (F . y);

        

        then

         A6: (t . a) = (F . y) by A2, A3, Def1

        .= (t9 . a) by A4, A5, Def1;

        reconsider G1 = F1, G19 = F19, G2 = F2, G29 = F29 as Function of {m}, the carrier' of A;

        reconsider s = t, s9 = t9 as Function of {a}, the carrier' of A;

        

         A7: ( id a) = m by TARSKI:def 1;

        

         A8: F1 is_transformable_to F2 by A3;

        then

         A9: ( Hom ((F1 . a),(F2 . a))) <> {} ;

        

         A10: F19 is_transformable_to F29 by A5;

        then

         A11: ( Hom ((F19 . a),(F29 . a))) <> {} ;

        then (F1 . a) = (F19 . a) by A6, A9, CAT_1: 6;

        

        then (G1 . ( id a)) = ( id (F19 . a)) by CAT_1: 71

        .= (G19 . ( id a)) by CAT_1: 71;

        then

         A12: F1 = F19 by A7, FUNCT_2: 125;

        (F2 . a) = (F29 . a) by A6, A9, A11, CAT_1: 6;

        

        then (G2 . ( id a)) = ( id (F29 . a)) by CAT_1: 71

        .= (G29 . ( id a)) by CAT_1: 71;

        then

         A13: F2 = F29 by A7, FUNCT_2: 125;

        (s . a) = (t9 . a) by A8, A6, NATTRA_1:def 5

        .= (s9 . a) by A10, NATTRA_1:def 5;

        hence x = y by A2, A4, A12, A13, FUNCT_2: 125;

      end;

      hence F is one-to-one by FUNCT_2: 19;

      thus ( rng F) c= the carrier' of A;

      let x be object;

      assume x in the carrier' of A;

      then

      reconsider f = x as Morphism of A;

      reconsider F1 = ( {m} --> ( id ( dom f))), F2 = ( {m} --> ( id ( cod f))) as Function of the carrier' of ( 1Cat (o,m)), the carrier' of A;

       A14:

      now

        let g be Morphism of ( 1Cat (o,m));

        

        thus (F1 . ( id ( dom g))) = ( id ( dom f)) by FUNCOP_1: 7

        .= ( id ( dom ( id ( dom f))))

        .= ( id ( dom (F1 . g))) by FUNCOP_1: 7;

        

        thus (F1 . ( id ( cod g))) = ( id ( dom f)) by FUNCOP_1: 7

        .= ( id ( cod ( id ( dom f))))

        .= ( id ( cod (F1 . g))) by FUNCOP_1: 7;

      end;

       A15:

      now

        let h,g be Morphism of ( 1Cat (o,m)) such that ( dom g) = ( cod h);

        

         A16: ( Hom (( dom f),( dom f))) <> {} ;

        

        thus (F1 . (g (*) h)) = ( id ( dom f)) by FUNCOP_1: 7

        .= (( id ( dom f)) * ( id ( dom f)))

        .= (( id ( dom f)) (*) ( id ( dom f)) qua Morphism of A) by A16, CAT_1:def 13

        .= (( id ( dom f)) (*) (F1 . h)) by FUNCOP_1: 7

        .= ((F1 . g) (*) (F1 . h)) by FUNCOP_1: 7;

      end;

       A17:

      now

        let h,g be Morphism of ( 1Cat (o,m)) such that ( dom g) = ( cod h);

        

         A18: ( Hom (( cod f),( cod f))) <> {} ;

        

        thus (F2 . (g (*) h)) = ( id ( cod f)) by FUNCOP_1: 7

        .= (( id ( cod f)) * ( id ( cod f)))

        .= (( id ( cod f)) (*) ( id ( cod f)) qua Morphism of A) by A18, CAT_1:def 13

        .= (( id ( cod f)) (*) (F2 . h)) by FUNCOP_1: 7

        .= ((F2 . g) (*) (F2 . h)) by FUNCOP_1: 7;

      end;

       A19:

      now

        let g be Morphism of ( 1Cat (o,m));

        

        thus (F2 . ( id ( dom g))) = ( id ( cod f)) by FUNCOP_1: 7

        .= ( id ( dom ( id ( cod f))))

        .= ( id ( dom (F2 . g))) by FUNCOP_1: 7;

        

        thus (F2 . ( id ( cod g))) = ( id ( cod f)) by FUNCOP_1: 7

        .= ( id ( cod ( id ( cod f))))

        .= ( id ( cod (F2 . g))) by FUNCOP_1: 7;

      end;

      (for c be Object of ( 1Cat (o,m)) holds ex d be Object of A st (F1 . ( id c)) = ( id d)) & for c be Object of ( 1Cat (o,m)) holds ex d be Object of A st (F2 . ( id c)) = ( id d) by FUNCOP_1: 7;

      then

      reconsider F1, F2 as Functor of ( 1Cat (o,m)), A by A14, A15, A19, A17, CAT_1: 61;

      reconsider t = ( {a} --> f) as Function of the carrier of ( 1Cat (o,m)), the carrier' of A;

      

       A20: for b be Object of ( 1Cat (o,m)) holds (F1 . b) = ( dom f) & (F2 . b) = ( cod f)

      proof

        let b be Object of ( 1Cat (o,m));

        (F2 . ( id b) qua Morphism of ( 1Cat (o,m))) = ( id ( cod f)) by FUNCOP_1: 7;

        then

         A21: ( id (F2 . b)) = ( id ( cod f)) by CAT_1: 71;

        (F1 . ( id b) qua Morphism of ( 1Cat (o,m))) = ( id ( dom f)) by FUNCOP_1: 7;

        then ( id (F1 . b)) = ( id ( dom f)) by CAT_1: 71;

        hence thesis by A21, CAT_1: 59;

      end;

       A22:

      now

        let b be Object of ( 1Cat (o,m));

        

         A23: (F2 . b) = ( cod f) by A20;

        (t . b) = f & (F1 . b) = ( dom f) by A20, FUNCOP_1: 7;

        then (t . b) in ( Hom ((F1 . b),(F2 . b))) by A23;

        hence (t . b) is Morphism of (F1 . b), (F2 . b) by CAT_1:def 5;

      end;

       A24:

      now

        let b be Object of ( 1Cat (o,m));

        (F1 . b) = ( dom f) & (F2 . b) = ( cod f) by A20;

        hence ( Hom ((F1 . b),(F2 . b))) <> {} by CAT_1: 2;

      end;

      then

       A25: F1 is_transformable_to F2;

      then

      reconsider t as transformation of F1, F2 by A22, NATTRA_1:def 3;

      

       A26: for b be Object of ( 1Cat (o,m)) holds (t . b) = f

      proof

        let b be Object of ( 1Cat (o,m));

        

        thus f = (( {a} --> f) . b) by FUNCOP_1: 7

        .= (t . b) by A25, NATTRA_1:def 5;

      end;

       A27:

      now

        let b1,b2 be Object of ( 1Cat (o,m)) such that

         A28: ( Hom (b1,b2)) <> {} ;

        

         A29: ( Hom ((F2 . b1),(F2 . b2))) <> {} by A28, CAT_1: 82;

        let g be Morphism of b1, b2;

        

         A30: (t . b1) = f & ( Hom ((F1 . b1),(F2 . b1))) <> {} by A24, A26;

        

         A31: ( Hom ((F1 . b1),(F1 . b2))) <> {} by A28, CAT_1: 82;

        

         A32: m in {m} by TARSKI:def 1;

        

         A33: g = m by TARSKI:def 1;

        

        then

         A34: (F2 /. g) = (F2 . m) by A28, CAT_3:def 10

        .= ( id ( cod f)) by A32, FUNCOP_1: 7;

        

         A35: (F1 /. g) = (F1 . m) by A28, A33, CAT_3:def 10

        .= ( id ( dom f)) by A32, FUNCOP_1: 7;

        (t . b2) = f & ( Hom ((F1 . b2),(F2 . b2))) <> {} by A24, A26;

        

        hence ((t . b2) * (F1 /. g)) = (f (*) (F1 /. g)) by A31, CAT_1:def 13

        .= f by A35, CAT_1: 22

        .= ((F2 /. g) (*) f) by A34, CAT_1: 21

        .= ((F2 /. g) * (t . b1)) by A30, A29, CAT_1:def 13;

      end;

      F1 is_transformable_to F2 by A24;

      then

       A36: F1 is_naturally_transformable_to F2 by A27;

      then

      reconsider t as natural_transformation of F1, F2 by A27, NATTRA_1:def 8;

       [ [F1, F2], t] in ( NatTrans (( 1Cat (o,m)),A)) by A36, NATTRA_1:def 16;

      then

       A37: [ [F1, F2], t] in the carrier' of ( Functors (( 1Cat (o,m)),A)) by NATTRA_1:def 17;

      (F . [ [F1, F2], t]) = (t . a) by A36, Def1

      .= f by A26;

      hence thesis by A37, FUNCT_2: 4;

    end;

    begin

    theorem :: ISOCAT_2:10

    

     Th8: for F be Functor of [:A, B:], C, a be Object of A, b be Object of B holds ((F ?- a) . b) = (F . [a, b])

    proof

      let F be Functor of [:A, B:], C, a be Object of A, b be Object of B;

      

      thus ((F ?- a) . b) = (( Obj F) . (a,b)) by CAT_2: 37

      .= (F . [a, b]);

    end;

    theorem :: ISOCAT_2:11

    

     Th9: for a1,a2 be Object of A, b1,b2 be Object of B holds ( Hom (a1,a2)) <> {} & ( Hom (b1,b2)) <> {} iff ( Hom ( [a1, b1], [a2, b2])) <> {}

    proof

      let a1,a2 be Object of A, b1,b2 be Object of B;

      ( Hom ( [a1, b1], [a2, b2])) = [:( Hom (a1,a2)), ( Hom (b1,b2)):] by CAT_2: 32;

      hence thesis by ZFMISC_1: 90;

    end;

    theorem :: ISOCAT_2:12

    

     Th10: for a1,a2 be Object of A, b1,b2 be Object of B st ( Hom ( [a1, b1], [a2, b2])) <> {} holds for f be Morphism of A, g be Morphism of B holds [f, g] is Morphism of [a1, b1], [a2, b2] iff f is Morphism of a1, a2 & g is Morphism of b1, b2

    proof

      let a1,a2 be Object of A, b1,b2 be Object of B;

      assume

       A1: ( Hom ( [a1, b1], [a2, b2])) <> {} ;

      let f be Morphism of A;

      let g be Morphism of B;

      thus [f, g] is Morphism of [a1, b1], [a2, b2] implies f is Morphism of a1, a2 & g is Morphism of b1, b2

      proof

        assume [f, g] is Morphism of [a1, b1], [a2, b2];

        then

         A2: [f, g] in ( Hom ( [a1, b1], [a2, b2])) by A1, CAT_1:def 5;

        ( Hom ( [a1, b1], [a2, b2])) = [:( Hom (a1,a2)), ( Hom (b1,b2)):] by CAT_2: 32;

        then f in ( Hom (a1,a2)) & g in ( Hom (b1,b2)) by A2, ZFMISC_1: 87;

        hence thesis by CAT_1:def 5;

      end;

      ( Hom (a1,a2)) <> {} & ( Hom (b1,b2)) <> {} by A1, Th9;

      hence thesis by CAT_2: 33;

    end;

    theorem :: ISOCAT_2:13

    

     Th11: for F1,F2 be Functor of [:A, B:], C st F1 is_naturally_transformable_to F2 holds for t be natural_transformation of F1, F2, a be Object of A holds (F1 ?- a) is_naturally_transformable_to (F2 ?- a) & (( curry t) . a) is natural_transformation of (F1 ?- a), (F2 ?- a)

    proof

      let F1,F2 be Functor of [:A, B:], C;

      assume

       A1: F1 is_naturally_transformable_to F2;

      then

       A2: F1 is_transformable_to F2;

      let u be natural_transformation of F1, F2, a be Object of A;

      reconsider t = u as Function of [:the carrier of A, the carrier of B:], the carrier' of C;

      

       A3: (F1 ?- a) is_transformable_to (F2 ?- a)

      proof

        let b be Object of B;

        ((F1 ?- a) . b) = (F1 . [a, b]) & ((F2 ?- a) . b) = (F2 . [a, b]) by Th8;

        hence thesis by A2;

      end;

       A4:

      now

        let b be Object of B;

        

         A5: ((F1 ?- a) . b) = (F1 . [a, b]) & ((F2 ?- a) . b) = (F2 . [a, b]) by Th8;

        

         A6: ( Hom (((F1 ?- a) . b),((F2 ?- a) . b))) <> {} by A3;

        ((( curry t) . a) . b) = (t . (a,b)) by FUNCT_5: 69

        .= (u . [a, b]) by A2, NATTRA_1:def 5;

        hence ((( curry t) . a) . b) in ( Hom (((F1 ?- a) . b),((F2 ?- a) . b))) by A5, A6, CAT_1:def 5;

      end;

      now

        let b be Object of B;

        ((( curry t) . a) . b) in ( Hom (((F1 ?- a) . b),((F2 ?- a) . b))) by A4;

        hence ((( curry t) . a) . b) is Morphism of ((F1 ?- a) . b), ((F2 ?- a) . b) by CAT_1:def 5;

      end;

      then

      reconsider s = (( curry t) . a) as transformation of (F1 ?- a), (F2 ?- a) by A3, NATTRA_1:def 3;

       A7:

      now

        let b1,b2 be Object of B such that

         A8: ( Hom (b1,b2)) <> {} ;

        

         A9: ( Hom (((F1 ?- a) . b1),((F1 ?- a) . b2))) <> {} by A8, CAT_1: 84;

        let f be Morphism of b1, b2;

        

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

        then

        reconsider g = [( id a), f] as Morphism of [a, b1], [a, b2] by A8, CAT_2: 33;

        

         A11: ( Hom ( [a, b1], [a, b2])) <> {} by A8, A10, Th9;

        then

         A12: ( Hom ((F1 . [a, b1]),(F1 . [a, b2]))) <> {} by CAT_1: 84;

        

         A13: (s . b1) = ((( curry t) . a) . b1) by A3, NATTRA_1:def 5

        .= (t . (a,b1)) by FUNCT_5: 69

        .= (u . [a, b1]) by A2, NATTRA_1:def 5;

        

         A14: ( Hom ((F1 . [a, b2]),(F2 . [a, b2]))) <> {} by A2;

        

         A15: ( Hom (((F2 ?- a) . b1),((F2 ?- a) . b2))) <> {} by A8, CAT_1: 84;

        

         A16: ((F1 ?- a) . b1) = (F1 . [a, b1]) & ((F2 ?- a) . b1) = (F2 . [a, b1]) by Th8;

        

         A17: ((F1 ?- a) . b2) = (F1 . [a, b2]) & ((F2 ?- a) . b2) = (F2 . [a, b2]) by Th8;

        

         A18: ( Hom ((F1 . [a, b1]),(F2 . [a, b1]))) <> {} by A2;

        

         A19: ( Hom ((F2 . [a, b1]),(F2 . [a, b2]))) <> {} by A11, CAT_1: 84;

        (s . b2) = ((( curry t) . a) . b2) by A3, NATTRA_1:def 5

        .= (t . (a,b2)) by FUNCT_5: 69

        .= (u . [a, b2]) by A2, NATTRA_1:def 5;

        

        hence ((s . b2) * ((F1 ?- a) /. f)) = ((u . [a, b2]) (*) ((F1 ?- a) /. f)) by A14, A9, A17, CAT_1:def 13

        .= ((u . [a, b2]) (*) ((F1 ?- a) . f qua Morphism of B)) by A8, CAT_3:def 10

        .= ((u . [a, b2]) (*) (F1 . (( id a),f))) by CAT_2: 36

        .= ((u . [a, b2]) (*) (F1 /. g) qua Morphism of C) by A11, CAT_3:def 10

        .= ((u . [a, b2]) * (F1 /. g)) by A12, A14, CAT_1:def 13

        .= ((F2 /. g) * (u . [a, b1])) by A1, A11, NATTRA_1:def 8

        .= ((F2 /. g) qua Morphism of C (*) (u . [a, b1])) by A18, A19, CAT_1:def 13

        .= ((F2 . (( id a),f)) (*) (u . [a, b1])) by A11, CAT_3:def 10

        .= (((F2 ?- a) . f qua Morphism of B) (*) (u . [a, b1])) by CAT_2: 36

        .= (((F2 ?- a) /. f) qua Morphism of C (*) (s . b1)) by A8, A13, CAT_3:def 10

        .= (((F2 ?- a) /. f) * (s . b1)) by A18, A15, A16, CAT_1:def 13;

      end;

      hence (F1 ?- a) is_naturally_transformable_to (F2 ?- a) by A3;

      hence thesis by A7, NATTRA_1:def 8;

    end;

    definition

      let A, B, C;

      let F be Functor of [:A, B:], C;

      let f be Morphism of A;

      :: ISOCAT_2:def2

      func curry (F,f) -> Function of the carrier' of B, the carrier' of C equals (( curry F) . f);

      coherence

      proof

        reconsider F as Function of [:the carrier' of A, the carrier' of B:], the carrier' of C;

        (( curry F) . f) is Function of the carrier' of B, the carrier' of C;

        hence thesis;

      end;

    end

    theorem :: ISOCAT_2:14

    

     Th12: for a1,a2 be Object of A, b1,b2 be Object of B, f be Morphism of A, g be Morphism of B st f in ( Hom (a1,a2)) & g in ( Hom (b1,b2)) holds [f, g] in ( Hom ( [a1, b1], [a2, b2]))

    proof

      let a1,a2 be Object of A, b1,b2 be Object of B, f be Morphism of A, g be Morphism of B;

      assume f in ( Hom (a1,a2)) & g in ( Hom (b1,b2));

      then [f, g] in [:( Hom (a1,a2)), ( Hom (b1,b2)):] by ZFMISC_1: 87;

      hence thesis by CAT_2: 32;

    end;

    theorem :: ISOCAT_2:15

    

     Th13: for F be Functor of [:A, B:], C holds for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds (F ?- a) is_naturally_transformable_to (F ?- b) & (( curry (F,f)) * ( IdMap B)) is natural_transformation of (F ?- a), (F ?- b)

    proof

      let F be Functor of [:A, B:], C;

      let a1,a2 be Object of A such that

       A1: ( Hom (a1,a2)) <> {} ;

      reconsider G = F as Function of [:the carrier' of A, the carrier' of B:], the carrier' of C;

      let f be Morphism of a1, a2;

      reconsider Ff = (( curry G) . f qua Morphism of A) as Function of the carrier' of B, the carrier' of C;

       A2:

      now

        let b be Object of B;

        f in ( Hom (a1,a2)) & ( id b) in ( Hom (b,b)) by A1, CAT_1:def 5;

        then [f, ( id b)] in ( Hom ( [a1, b], [a2, b])) by Th12;

        then

         A3: (F . (f,( id b))) in ( Hom ((F . [a1, b]),(F . [a2, b]))) by CAT_1: 81;

        

         A4: ( id b) = (( IdMap B) . b) by ISOCAT_1:def 12;

        ((F ?- a1) . b) = (F . [a1, b]) & ((F ?- a2) . b) = (F . [a2, b]) by Th8;

        then (Ff . ( id b) qua Morphism of B) in ( Hom (((F ?- a1) . b),((F ?- a2) . b))) by A3, FUNCT_5: 69;

        hence ((( curry (F,f)) * ( IdMap B)) . b) in ( Hom (((F ?- a1) . b),((F ?- a2) . b))) by A4, FUNCT_2: 15;

      end;

      

       A5: (F ?- a1) is_transformable_to (F ?- a2) by A2;

      reconsider FfI = (( curry (F,f)) * ( IdMap B)) as Function of the carrier of B, the carrier' of C;

      now

        let b be Object of B;

        ((( curry (F,f)) * ( IdMap B)) . b) in ( Hom (((F ?- a1) . b),((F ?- a2) . b))) by A2;

        hence (FfI . b) is Morphism of ((F ?- a1) . b), ((F ?- a2) . b) by CAT_1:def 5;

      end;

      then

      reconsider t = (( curry (F,f)) * ( IdMap B)) as transformation of (F ?- a1), (F ?- a2) by A5, NATTRA_1:def 3;

       A6:

      now

        reconsider ida1 = ( id a1), ida2 = ( id a2) as Morphism of A;

        

         A7: ( Hom (a1,a1)) <> {} ;

        

         A8: ( Hom (a2,a2)) <> {} ;

        let b1,b2 be Object of B such that

         A9: ( Hom (b1,b2)) <> {} ;

        

         A10: ( Hom (((F ?- a2) . b1),((F ?- a2) . b2))) <> {} by A9, CAT_1: 84;

        let g be Morphism of b1, b2;

        reconsider idb1 = ( id b1), idb2 = ( id b2) as Morphism of B;

        

         A11: ( Hom (b1,b1)) <> {} ;

        

         A12: ( dom ( id b2)) = b2

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

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

        

        then

         A13: [(f (*) ida1), (idb2 (*) g)] = [(f (*) ida1), (( id b2) * g)] by A9, CAT_1:def 13

        .= [(f (*) ida1), g] by A9, CAT_1: 28

        .= [(f * ( id a1)), g] by A1, A7, CAT_1:def 13

        .= [f, g] by A1, CAT_1: 29

        .= [(( id a2) * f), g] by A1, CAT_1: 28

        .= [(ida2 (*) f), g] by A1, A8, CAT_1:def 13

        .= [(ida2 (*) f), (g * ( id b1))] by A9, CAT_1: 29

        .= [(ida2 (*) f), (g (*) idb1)] by A9, A11, CAT_1:def 13;

        

         A14: ( Hom (((F ?- a1) . b2),((F ?- a2) . b2))) <> {} & (t . b2) = (FfI . b2) by A5, NATTRA_1:def 5;

        

         A15: ( cod ( id a1)) = a1

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

        

        then

         A16: ( cod [( id a1), g]) = [( dom f), ( cod g)] by CAT_2: 28

        .= ( dom [f, ( id b2)]) by A12, CAT_2: 28;

        

         A17: ( Hom (((F ?- a1) . b1),((F ?- a2) . b1))) <> {} & (t . b1) = (FfI . b1) by A5, NATTRA_1:def 5;

        

         A18: ( dom g) = b1 by A9, CAT_1: 5

        .= ( cod ( id b1));

        

         A19: ( dom ( id a2)) = a2

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

        

        then

         A20: ( dom [( id a2), g]) = [( cod f), ( dom g)] by CAT_2: 28

        .= ( cod [f, ( id b1)]) by A18, CAT_2: 28;

        

         A21: ( id b2) = (( IdMap B) . b2) by ISOCAT_1:def 12;

        

         A22: ( id b1) = (( IdMap B) . b1) by ISOCAT_1:def 12;

        ( Hom (((F ?- a1) . b1),((F ?- a1) . b2))) <> {} by A9, CAT_1: 84;

        

        hence ((t . b2) * ((F ?- a1) /. g)) = ((FfI . b2) (*) ((F ?- a1) /. g)) by A14, CAT_1:def 13

        .= ((Ff . ( id b2) qua Morphism of B) (*) ((F ?- a1) /. g)) by A21, FUNCT_2: 15

        .= ((F . (f,( id b2))) (*) ((F ?- a1) /. g)) by FUNCT_5: 69

        .= ((F . [f, ( id b2)]) (*) ((F ?- a1) . g qua Morphism of B)) by A9, CAT_3:def 10

        .= ((F . (f,( id b2))) (*) (F . (( id a1),g))) by CAT_2: 36

        .= (F . ( [f, ( id b2)] (*) [( id a1), g])) by A16, CAT_1: 64

        .= (F . [(f (*) ida1), (idb2 (*) g)]) by A15, A12, CAT_2: 29

        .= (F . ( [ida2, g] (*) [f, idb1])) by A19, A18, A13, CAT_2: 29

        .= ((F . (( id a2),g)) (*) (F . [f, ( id b1)])) by A20, CAT_1: 64

        .= (((F ?- a2) . g qua Morphism of B) (*) (F . [f, ( id b1)])) by CAT_2: 36

        .= (((F ?- a2) /. g) (*) (F . (f,( id b1)))) by A9, CAT_3:def 10

        .= (((F ?- a2) /. g) (*) (Ff . ( id b1) qua Morphism of B)) by FUNCT_5: 69

        .= (((F ?- a2) /. g) (*) (FfI . b1)) by A22, FUNCT_2: 15

        .= (((F ?- a2) /. g) * (t . b1)) by A10, A17, CAT_1:def 13;

      end;

      hence (F ?- a1) is_naturally_transformable_to (F ?- a2) by A5;

      hence thesis by A6, NATTRA_1:def 8;

    end;

    definition

      let A, B, C;

      let F be Functor of [:A, B:], C;

      let f be Morphism of A;

      :: ISOCAT_2:def3

      func F ?- f -> natural_transformation of (F ?- ( dom f)), (F ?- ( cod f)) equals (( curry (F,f)) * ( IdMap B));

      coherence

      proof

        ( Hom (( dom f),( cod f))) <> {} & f is Morphism of ( dom f), ( cod f) by CAT_1: 2, CAT_1: 4;

        hence thesis by Th13;

      end;

      correctness ;

    end

    theorem :: ISOCAT_2:16

    

     Th14: for F be Functor of [:A, B:], C, g be Morphism of A holds (F ?- ( dom g)) is_naturally_transformable_to (F ?- ( cod g))

    proof

      let F be Functor of [:A, B:], C, g be Morphism of A;

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

      hence thesis by Th13;

    end;

    theorem :: ISOCAT_2:17

    

     Th15: for F be Functor of [:A, B:], C, f be Morphism of A, b be Object of B holds ((F ?- f) . b) = (F . (f,( id b)))

    proof

      let F be Functor of [:A, B:], C, f be Morphism of A, b be Object of B;

      reconsider G = F as Function of [:the carrier' of A, the carrier' of B:], the carrier' of C;

      reconsider Ff = (( curry G) . f) as Function of the carrier' of B, the carrier' of C;

      

       A1: ( id b) = (( IdMap B) . b) by ISOCAT_1:def 12;

      (F ?- ( dom f)) is_naturally_transformable_to (F ?- ( cod f)) by Th14;

      then (F ?- ( dom f)) is_transformable_to (F ?- ( cod f));

      

      hence ((F ?- f) . b) = ((( curry (F,f)) * ( IdMap B)) . b) by NATTRA_1:def 5

      .= (Ff . ( id b) qua Morphism of B) by A1, FUNCT_2: 15

      .= (F . (f,( id b))) by FUNCT_5: 69;

    end;

    theorem :: ISOCAT_2:18

    

     Th16: for F be Functor of [:A, B:], C, a be Object of A holds ( id (F ?- a)) = (F ?- ( id a))

    proof

      let F be Functor of [:A, B:], C, a be Object of A;

      reconsider G = F as Function of [:the carrier' of A, the carrier' of B:], the carrier' of C;

      reconsider Ff = (( curry G) . ( id a) qua Morphism of A) as Function of the carrier' of B, the carrier' of C;

      reconsider I = (F ?- ( id a)) as transformation of (F ?- a), (F ?- a);

      now

        let b be Object of B;

        

         A1: ( id b) = (( IdMap B) . b) by ISOCAT_1:def 12;

        

        thus (I qua Function of the carrier of B, the carrier' of C . b) = (Ff . ( id b) qua Morphism of B) by A1, FUNCT_2: 15

        .= (F . (( id a),( id b))) by FUNCT_5: 69

        .= (F . ( id [a, b]) qua Morphism of [:A, B:]) by CAT_2: 31

        .= ( id (F . [a, b])) by CAT_1: 71

        .= ( id ((F ?- a) . b)) by Th8;

      end;

      hence thesis by NATTRA_1:def 4;

    end;

    theorem :: ISOCAT_2:19

    

     Th17: for F be Functor of [:A, B:], C, g,f be Morphism of A st ( dom g) = ( cod f) holds for t be natural_transformation of (F ?- ( dom f)), (F ?- ( dom g)) st t = (F ?- f) holds (F ?- (g (*) f)) = ((F ?- g) `*` t)

    proof

      let F be Functor of [:A, B:], C, g,f be Morphism of A such that

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

      

       A2: (F ?- ( dom f)) is_naturally_transformable_to (F ?- ( dom g)) by A1, Th14;

      then

       A3: (F ?- ( dom f)) is_transformable_to (F ?- ( dom g));

      reconsider G = F as Function of [:the carrier' of A, the carrier' of B:], the carrier' of C;

      reconsider Fgf = (( curry G) . (g (*) f)), Ff = (( curry G) . f), Fg = (( curry G) . g) as Function of the carrier' of B, the carrier' of C;

      let t be natural_transformation of (F ?- ( dom f)), (F ?- ( dom g)) such that

       A4: t = (F ?- f);

      reconsider s = t as transformation of (F ?- ( dom f)), (F ?- ( dom g));

      

       A5: (F ?- ( dom g)) is_naturally_transformable_to (F ?- ( cod g)) by Th14;

      then

       A6: (F ?- ( dom g)) is_transformable_to (F ?- ( cod g));

      (F ?- ( dom (g (*) f))) is_naturally_transformable_to (F ?- ( cod (g (*) f))) by Th14;

      then

       A7: (F ?- ( dom (g (*) f))) is_transformable_to (F ?- ( cod (g (*) f)));

       A8:

      now

        let b be Object of B;

        

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

        

         A10: ( id b) = (( IdMap B) . b) by ISOCAT_1:def 12;

        

         A11: ((F ?- g) . b) = ((( curry (F,g)) * ( IdMap B)) . b) by A6, NATTRA_1:def 5

        .= (Fg . ( id b) qua Morphism of B) by A10, FUNCT_2: 15

        .= (F . (g,( id b))) by FUNCT_5: 69;

        ( dom ( id b)) = b

        .= ( cod ( id b));

        

        then

         A12: ( dom [g, ( id b)]) = [( cod f), ( cod ( id b))] by A1, CAT_2: 28

        .= ( cod [f, ( id b)]) by CAT_2: 28;

        

         A13: ( Hom (((F ?- ( dom g)) . b),((F ?- ( cod g)) . b))) <> {} & ( Hom (((F ?- ( dom f)) . b),((F ?- ( dom g)) . b))) <> {} by A3, A6;

        

         A14: ((F ?- f) . b) = ((( curry (F,f)) * ( IdMap B)) . b) by A1, A3, NATTRA_1:def 5

        .= (Ff . ( id b) qua Morphism of B) by A10, FUNCT_2: 15

        .= (F . (f,( id b))) by FUNCT_5: 69;

        

        thus ((F ?- (g (*) f)) . b) = ((( curry (F,(g (*) f))) * ( IdMap B)) . b) by A7, NATTRA_1:def 5

        .= (Fgf . ( id b) qua Morphism of B) by A10, FUNCT_2: 15

        .= (F . ((g (*) f),( id b))) by FUNCT_5: 69

        .= (F . [(g (*) f), (( id b) * ( id b))])

        .= (F . [(g (*) f), (( id b) (*) ( id b) qua Morphism of B)]) by A9, CAT_1:def 13

        .= (F . ( [g, ( id b)] (*) [f, ( id b)])) by A12, CAT_2: 30

        .= (((F ?- g) . b) (*) (s . b) qua Morphism of C) by A1, A4, A11, A14, A12, CAT_1: 64

        .= (((F ?- g) . b) * (s . b)) by A13, CAT_1:def 13

        .= (((F ?- g) `*` s) . b) by A3, A6, NATTRA_1:def 6;

      end;

      ( cod (g (*) f)) = ( cod g) & ( dom (g (*) f)) = ( dom f) by A1, CAT_1: 17;

      then (F ?- (g (*) f)) = ((F ?- g) `*` s) by A3, A6, A8, NATTRA_1: 18, NATTRA_1: 19;

      hence thesis by A2, A5, NATTRA_1:def 9;

    end;

    definition

      let A, B, C;

      let F be Functor of [:A, B:], C;

      :: ISOCAT_2:def4

      func export F -> Functor of A, ( Functors (B,C)) means

      : Def4: for f be Morphism of A holds (it . f) = [ [(F ?- ( dom f)), (F ?- ( cod f))], (F ?- f)];

      existence

      proof

        defpred P[ object, object] means for f be Morphism of A st $1 = f holds $2 = [ [(F ?- ( dom f)), (F ?- ( cod f))], (F ?- f)];

         A1:

        now

          let m be object;

          assume m in the carrier' of A;

          then

          reconsider g = m as Morphism of A;

          reconsider o = [ [(F ?- ( dom g)), (F ?- ( cod g))], (F ?- g)] as object;

          take o;

          (F ?- ( dom g)) is_naturally_transformable_to (F ?- ( cod g)) by Th14;

          then o in ( NatTrans (B,C)) by NATTRA_1: 32;

          hence o in the carrier' of ( Functors (B,C)) by NATTRA_1:def 17;

          thus P[m, o];

        end;

        consider G be Function of the carrier' of A, the carrier' of ( Functors (B,C)) such that

         A2: for m be object st m in the carrier' of A holds P[m, (G . m)] from FUNCT_2:sch 1( A1);

        G is Functor of A, ( Functors (B,C))

        proof

          thus for c be Object of A holds ex d be Object of ( Functors (B,C)) st (G . ( id c)) = ( id d)

          proof

            let c be Object of A;

            reconsider d = (F ?- c) as Object of ( Functors (B,C)) by Th5;

            take d;

            

            thus (G . ( id c)) = [ [(F ?- c), (F ?- c)], (F ?- ( id c))] by A2

            .= [ [(F ?- c), (F ?- c)], ( id (F ?- c))] by Th16

            .= ( id d) by NATTRA_1:def 17;

          end;

          thus for f be Morphism of A holds (G . ( id ( dom f))) = ( id ( dom (G . f))) & (G . ( id ( cod f))) = ( id ( cod (G . f)))

          proof

            let f be Element of the carrier' of A;

            reconsider d = (F ?- ( dom f)), c = (F ?- ( cod f)) as Object of ( Functors (B,C)) by Th5;

            

             A3: (G . f) = [ [(F ?- ( dom f)), (F ?- ( cod f))], (F ?- f)] by A2;

            

            thus (G . ( id ( dom f))) = [ [(F ?- ( dom f)), (F ?- ( dom f))], (F ?- ( id ( dom f)))] by A2

            .= [ [(F ?- ( dom f)), (F ?- ( dom f))], ( id (F ?- ( dom f)))] by Th16

            .= ( id d) by NATTRA_1:def 17

            .= ( id ( dom (G . f))) by A3, NATTRA_1: 33;

            

            thus (G . ( id ( cod f))) = [ [(F ?- ( cod f)), (F ?- ( cod f))], (F ?- ( id ( cod f)))] by A2

            .= [ [(F ?- ( cod f)), (F ?- ( cod f))], ( id (F ?- ( cod f)))] by Th16

            .= ( id c) by NATTRA_1:def 17

            .= ( id ( cod (G . f))) by A3, NATTRA_1: 33;

          end;

          let f,g be Morphism of A;

          assume

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

          then

          reconsider t = (F ?- f) as natural_transformation of (F ?- ( dom f)), (F ?- ( dom g));

          

           A5: ( cod (g (*) f)) = ( cod g) & ( dom (g (*) f)) = ( dom f) by A4, CAT_1: 17;

          

           A6: (F ?- ( dom g)) is_naturally_transformable_to (F ?- ( cod g)) by Th14;

          the carrier' of ( Functors (B,C)) = ( NatTrans (B,C)) & (F ?- ( dom f)) is_naturally_transformable_to (F ?- ( cod f)) by Th14, NATTRA_1:def 17;

          then

          reconsider gg = [ [(F ?- ( dom g)), (F ?- ( cod g))], (F ?- g)], ff = [ [(F ?- ( dom f)), (F ?- ( cod f))], (F ?- f)] as Morphism of ( Functors (B,C)) by A6, NATTRA_1: 32;

          

           A7: (G . f) = ff by A2;

          

          thus (G . (g (*) f)) = [ [(F ?- ( dom (g (*) f))), (F ?- ( cod (g (*) f)))], (F ?- (g (*) f))] by A2

          .= [ [(F ?- ( dom (g (*) f))), (F ?- ( cod (g (*) f)))], ((F ?- g) `*` t)] by A4, Th17

          .= (gg (*) ff) by A4, A5, NATTRA_1: 36

          .= ((G . g) (*) (G . f)) by A2, A7;

        end;

        then

        reconsider G as Functor of A, ( Functors (B,C));

        take G;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let G1,G2 be Functor of A, ( Functors (B,C)) such that

         A8: for f be Morphism of A holds (G1 . f) = [ [(F ?- ( dom f)), (F ?- ( cod f))], (F ?- f)] and

         A9: for f be Morphism of A holds (G2 . f) = [ [(F ?- ( dom f)), (F ?- ( cod f))], (F ?- f)];

        now

          let f be Morphism of A;

          

          thus (G1 . f) = [ [(F ?- ( dom f)), (F ?- ( cod f))], (F ?- f)] by A8

          .= (G2 . f) by A9;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    

     Lm1: for F1,F2 be Functor of A, B st F1 is_transformable_to F2 holds for t be transformation of F1, F2, a be Object of A holds (t . a) in ( Hom ((F1 . a),(F2 . a)))

    proof

      let F1,F2 be Functor of A, B such that

       A1: F1 is_transformable_to F2;

      let t be transformation of F1, F2, a be Object of A;

      ( Hom ((F1 . a),(F2 . a))) <> {} by A1;

      hence thesis by CAT_1:def 5;

    end;

    theorem :: ISOCAT_2:20

    

     Th18: for F be Functor of [:A, B:], C, a be Object of A holds (( export F) . a) = (F ?- a)

    proof

      let F be Functor of [:A, B:], C, a be Object of A;

      reconsider o = (F ?- a) as Object of ( Functors (B,C)) by Th5;

      reconsider i = ( id a) as Morphism of A;

      (( export F) . i) = [ [(F ?- a), (F ?- a)], (F ?- ( id a))] by Def4

      .= [ [(F ?- a), (F ?- a)], ( id (F ?- a))] by Th16

      .= ( id o) by NATTRA_1:def 17;

      hence thesis by CAT_1: 67;

    end;

    theorem :: ISOCAT_2:21

    

     Th19: for F be Functor of [:A, B:], C, a be Object of A holds (( export F) . a) is Functor of B, C

    proof

      let F be Functor of [:A, B:], C, a be Object of A;

      (( export F) . a) = (F ?- a) by Th18;

      hence thesis;

    end;

    theorem :: ISOCAT_2:22

    

     Th20: for F1,F2 be Functor of [:A, B:], C holds ( export F1) = ( export F2) implies F1 = F2

    proof

      let F1,F2 be Functor of [:A, B:], C such that

       A1: ( export F1) = ( export F2);

      now

        let fg be Morphism of [:A, B:];

        consider f be Morphism of A, g be Morphism of B such that

         A2: fg = [f, g] by CAT_2: 27;

        

         A3: ( dom ( id ( cod f))) = ( cod f) & ( dom g) = ( cod ( id ( dom g)));

        

         A4: fg = [(( id ( cod f)) (*) f), g] by A2, Th3

        .= [(( id ( cod f)) (*) f), (g (*) ( id ( dom g)))] by Th4

        .= ( [( id ( cod f)), g] (*) [f, ( id ( dom g))]) by A3, CAT_2: 29;

        

         A5: [ [(F1 ?- ( dom f)), (F1 ?- ( cod f))], (F1 ?- f)] = (( export F2) . f) by A1, Def4

        .= [ [(F2 ?- ( dom f)), (F2 ?- ( cod f))], (F2 ?- f)] by Def4;

        then

         A6: [(F1 ?- ( dom f)), (F1 ?- ( cod f))] = [(F2 ?- ( dom f)), (F2 ?- ( cod f))] by XTUPLE_0: 1;

        then

         A7: (F1 ?- ( dom f)) = (F2 ?- ( dom f)) by XTUPLE_0: 1;

        

         A8: (F1 ?- ( cod f)) = (F2 ?- ( cod f)) by A6, XTUPLE_0: 1;

        

        then

         A9: (F1 . (( id ( cod f)),g)) = ((F2 ?- ( cod f)) . g) by CAT_2: 36

        .= (F2 . (( id ( cod f)),g)) by CAT_2: 36;

        

         A10: ( cod [f, ( id ( dom g))]) = [( cod f), ( cod ( id ( dom g)))] by CAT_2: 28

        .= [( cod f), ( dom g)]

        .= [( dom ( id ( cod f))), ( dom g)]

        .= ( dom [( id ( cod f)), g]) by CAT_2: 28;

        (F1 . (f,( id ( dom g)))) = ((F1 ?- f) . ( dom g)) by Th15

        .= ((F2 ?- f) . ( dom g)) by A5, A7, A8, XTUPLE_0: 1

        .= (F2 . (f,( id ( dom g)))) by Th15;

        

        hence (F1 . fg) = ((F2 . [( id ( cod f)), g]) (*) (F2 . [f, ( id ( dom g))])) by A4, A9, A10, CAT_1: 64

        .= (F2 . fg) by A4, A10, CAT_1: 64;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ISOCAT_2:23

    

     Th21: for F1,F2 be Functor of [:A, B:], C st F1 is_naturally_transformable_to F2 holds for t be natural_transformation of F1, F2 holds ( export F1) is_naturally_transformable_to ( export F2) & ex G be natural_transformation of ( export F1), ( export F2) st for s be Function of [:the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a be Object of A holds (G . a) = [ [(( export F1) . a), (( export F2) . a)], (( curry s) . a)]

    proof

      let F1,F2 be Functor of [:A, B:], C;

      assume

       A1: F1 is_naturally_transformable_to F2;

      then

       A2: F1 is_transformable_to F2;

      let t be natural_transformation of F1, F2;

      reconsider s = t as Function of [:the carrier of A, the carrier of B:], the carrier' of C;

       A3:

      now

        let a be Object of A;

        let S1,S2 be Functor of B, C such that

         A4: S1 = (( export F1) . a) and

         A5: S2 = (( export F2) . a);

        let b be Object of B;

        

         A6: (S2 . b) = ((F2 ?- a) . b) by A5, Th18

        .= (F2 . [a, b]) by Th8;

        

         A7: ((( curry s) . a) . b) = (s . (a,b)) by FUNCT_5: 69

        .= (t . [a, b]) by A2, NATTRA_1:def 5;

        (S1 . b) = ((F1 ?- a) . b) by A4, Th18

        .= (F1 . [a, b]) by Th8;

        hence ((( curry s) . a) . b) in ( Hom ((S1 . b),(S2 . b))) by A2, A6, A7, Lm1;

      end;

      

       A8: for a be Object of A, S1,S2 be Functor of B, C st S1 = (( export F1) . a) & S2 = (( export F2) . a) holds S1 is_transformable_to S2 by A3;

       A9:

      now

        let a be Object of A;

        let S1,S2 be Functor of B, C, T be transformation of S1, S2;

        assume that

         A10: S1 = (( export F1) . a) and

         A11: S2 = (( export F2) . a) and

         A12: T = (( curry s) . a);

        let b1,b2 be Object of B such that

         A13: ( Hom (b1,b2)) <> {} ;

        

         A14: ( Hom ((S1 . b1),(S1 . b2))) <> {} by A13, CAT_1: 84;

        

         A15: (T . b2) = (T qua Function of the carrier of B, the carrier' of C . b2) by A8, A10, A11, NATTRA_1:def 5

        .= (s . (a,b2)) by A12, FUNCT_5: 69

        .= (t . [a, b2]) by A2, NATTRA_1:def 5;

        

         A16: ( Hom ((F1 . [a, b2]),(F2 . [a, b2]))) <> {} by A2;

        let f be Morphism of b1, b2;

        

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

        then

        reconsider g = [( id a), f] as Morphism of [a, b1], [a, b2] by A13, CAT_2: 33;

        

         A18: ( Hom ( [a, b1], [a, b2])) <> {} by A13, A17, Th9;

        then

         A19: ( Hom ((F1 . [a, b1]),(F1 . [a, b2]))) <> {} by CAT_1: 84;

        

         A20: S1 is_transformable_to S2 by A8, A10, A11;

        then

         A21: ( Hom ((S1 . b1),(S2 . b1))) <> {} ;

        

         A22: (T . b1) = (T qua Function of the carrier of B, the carrier' of C . b1) by A8, A10, A11, NATTRA_1:def 5

        .= (s . (a,b1)) by A12, FUNCT_5: 69

        .= (t . [a, b1]) by A2, NATTRA_1:def 5;

        

         A23: ( Hom ((F1 . [a, b1]),(F2 . [a, b1]))) <> {} by A2;

        

         A24: ( Hom ((S1 . b2),(S2 . b2))) <> {} by A20;

        

         A25: ( Hom ((S2 . b1),(S2 . b2))) <> {} by A13, CAT_1: 84;

        

         A26: (S2 /. f) = ((F2 ?- a) /. f) by A11, Th18

        .= ((F2 ?- a) /. f qua Morphism of B) by A13, CAT_3:def 10

        .= (F2 . (( id a),f)) by CAT_2: 36

        .= (F2 /. g) by A18, CAT_3:def 10;

        

         A27: ( Hom ((F2 . [a, b1]),(F2 . [a, b2]))) <> {} by A18, CAT_1: 84;

        

         A28: (S1 /. f) = ((F1 ?- a) /. f) by A10, Th18

        .= ((F1 ?- a) /. f qua Morphism of B) by A13, CAT_3:def 10

        .= (F1 . (( id a),f)) by CAT_2: 36

        .= (F1 /. g) by A18, CAT_3:def 10;

        

        thus ((T . b2) * (S1 /. f)) = ((T . b2) (*) (S1 /. f)) by A14, A24, CAT_1:def 13

        .= ((t . [a, b2]) * (F1 /. g)) by A19, A16, A15, A28, CAT_1:def 13

        .= ((F2 /. g) * (t . [a, b1])) by A1, A18, NATTRA_1:def 8

        .= ((S2 /. f) qua Morphism of C (*) (T . b1)) by A27, A23, A22, A26, CAT_1:def 13

        .= ((S2 /. f) * (T . b1)) by A25, A21, CAT_1:def 13;

      end;

      defpred P[ object, object] means for f be Object of A, s be Function of [:the carrier of A, the carrier of B:], the carrier' of C st t = s & $1 = f holds $2 = [ [(( export F1) . f), (( export F2) . f)], (( curry s) . f)];

       A29:

      now

        let a be Object of A;

        let S1,S2 be Functor of B, C such that

         A30: S1 = (( export F1) . a) & S2 = (( export F2) . a);

        thus (( curry s) . a) is transformation of S1, S2

        proof

          thus S1 is_transformable_to S2 by A8, A30;

          let b be Object of B;

          ((( curry s) . a) . b) in ( Hom ((S1 . b),(S2 . b))) by A3, A30;

          hence thesis by CAT_1:def 5;

        end;

      end;

       A31:

      now

        let m be object;

        assume m in the carrier of A;

        then

        reconsider a = m as Object of A;

        reconsider S1 = (( export F1) . a), S2 = (( export F2) . a) as Functor of B, C by Th19;

        reconsider o = [ [(( export F1) . a), (( export F2) . a)], (( curry s) . a)] as object;

        take o;

        reconsider T = (( curry s) . a) as transformation of S1, S2 by A29;

        

         A32: S1 is_naturally_transformable_to S2

        proof

          thus S1 is_transformable_to S2 by A8;

          take T;

          thus thesis by A9;

        end;

        for a,b be Object of B st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((T . b) * (S1 /. f)) = ((S2 /. f) * (T . a)) by A9;

        then T is natural_transformation of S1, S2 by A32, NATTRA_1:def 8;

        then o in ( NatTrans (B,C)) by A32, NATTRA_1: 32;

        hence o in the carrier' of ( Functors (B,C)) by NATTRA_1:def 17;

        thus P[m, o];

      end;

      consider G be Function of the carrier of A, the carrier' of ( Functors (B,C)) such that

       A33: for m be object st m in the carrier of A holds P[m, (G . m)] from FUNCT_2:sch 1( A31);

       A34:

      now

        let a be Object of A;

        reconsider S1 = (( export F1) . a), S2 = (( export F2) . a) as Functor of B, C by Th19;

        reconsider T = (( curry s) . a) as transformation of S1, S2 by A29;

        

         A35: (G . a) = [ [S1, S2], T] by A33;

        

         A36: S1 is_naturally_transformable_to S2

        proof

          thus S1 is_transformable_to S2 by A8;

          take T;

          thus thesis by A9;

        end;

        for a,b be Object of B st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ((T . b) * (S1 /. f)) = ((S2 /. f) * (T . a)) by A9;

        then T is natural_transformation of S1, S2 by A36, NATTRA_1:def 8;

        then ( dom (G . a)) = S1 & ( cod (G . a)) = S2 by A35, NATTRA_1: 33;

        hence (G . a) in ( Hom ((( export F1) . a),(( export F2) . a)));

      end;

      then

       A37: for a be Object of A holds ( Hom ((( export F1) . a),(( export F2) . a))) <> {} ;

      G is transformation of ( export F1), ( export F2)

      proof

        thus ( export F1) is_transformable_to ( export F2) by A37;

        let a be Object of A;

        (G . a) in ( Hom ((( export F1) . a),(( export F2) . a))) by A34;

        hence thesis by CAT_1:def 5;

      end;

      then

      reconsider G as transformation of ( export F1), ( export F2);

      

       A38: ( export F1) is_transformable_to ( export F2) by A37;

       A39:

      now

        let a,b be Object of A such that

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

        

         A41: ( Hom ((( export F2) . a),(( export F2) . b))) <> {} by A40, CAT_1: 84;

        reconsider S1 = (( export F1) . a), S2 = (( export F2) . a), S3 = (( export F1) . b), S4 = (( export F2) . b) as Functor of B, C by Th19;

        let f be Morphism of a, b;

        

         A42: (F2 ?- a) = (( export F2) . a) by Th18;

        

         A43: (F1 ?- a) = (( export F1) . a) by Th18;

        then

        reconsider T12 = (( curry s) . a) as natural_transformation of S1, S2 by A1, A42, Th11;

        

         A44: (F2 ?- b) = (( export F2) . b) by Th18;

        then

         A45: (F2 ?- ( cod f)) = (( export F2) . b) by A40, CAT_1: 5;

        then

        reconsider T24 = (F2 ?- f) as natural_transformation of S2, S4 by A40, A42, CAT_1: 5;

        

         A46: (G . a) = (G . a qua set) by A38, NATTRA_1:def 5

        .= [ [S1, S2], T12] by A33;

        

         A47: (F1 ?- b) = (( export F1) . b) by Th18;

        then

        reconsider T34 = (( curry s) . b) as natural_transformation of S3, S4 by A1, A44, Th11;

        

         A48: S3 is_naturally_transformable_to S4 by A1, A47, A44, Th11;

        then

         A49: S3 is_transformable_to S4;

        

         A50: (F1 ?- ( cod f)) = (( export F1) . b) by A40, A47, CAT_1: 5;

        then

        reconsider T13 = (F1 ?- f) as natural_transformation of S1, S3 by A40, A43, CAT_1: 5;

        

         A51: (G . b) = (G . b qua set) by A38, NATTRA_1:def 5

        .= [ [S3, S4], T34] by A33;

        

         A52: S1 is_naturally_transformable_to S2 by A1, A42, A43, Th11;

        then

         A53: S1 is_transformable_to S2;

        reconsider g = f as Morphism of A;

        

         A54: ( Hom ((( export F1) . a),(( export F2) . a))) <> {} by A34;

        (F2 ?- ( dom f)) = (( export F2) . a) by A40, A42, CAT_1: 5;

        then

         A55: (( export F2) . g) = [ [S2, S4], T24] by A45, Def4;

        

         A56: ( Hom ((( export F1) . a),(( export F1) . b))) <> {} by A40, CAT_1: 84;

        

         A57: S2 is_naturally_transformable_to S4 by A40, A42, A44, Th13;

        then

         A58: S2 is_transformable_to S4;

        

         A59: S1 is_naturally_transformable_to S3 by A40, A47, A43, Th13;

        then

         A60: S1 is_transformable_to S3;

        now

          reconsider FF1 = F1, FF2 = F2 as Function of [:the carrier' of A, the carrier' of B:], the carrier' of C;

          let c be Object of B;

          

           A61: ( Hom ((F1 . [a, c]),(F2 . [a, c]))) <> {} by A2;

          

           A62: ( Hom ((F1 . [b, c]),(F2 . [b, c]))) <> {} by A2;

          

           A63: ( Hom ((S3 . c),(S4 . c))) <> {} & ( Hom ((S1 . c),(S3 . c))) <> {} by A60, A49;

          

           A64: ( Hom ((S2 . c),(S4 . c))) <> {} & ( Hom ((S1 . c),(S2 . c))) <> {} by A53, A58;

          

           A65: (t . [b, c]) = (s . (b,c)) by A2, NATTRA_1:def 5

          .= ((( curry s) . b) . c) by FUNCT_5: 69

          .= (T34 . c) by A49, NATTRA_1:def 5;

          

           A66: (t . [a, c]) = (s . (a,c)) by A2, NATTRA_1:def 5

          .= ((( curry s) . a) . c) by FUNCT_5: 69

          .= (T12 . c) by A53, NATTRA_1:def 5;

          

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

          then

          reconsider fi = [f, ( id c)] as Morphism of [a, c], [b, c] by A40, CAT_2: 33;

          

           A68: ( Hom ( [a, c], [b, c])) <> {} by A40, A67, Th9;

          then

           A69: ( Hom ((F2 . [a, c]),(F2 . [b, c]))) <> {} by CAT_1: 84;

          

           A70: ( id c) = (( IdMap B) . c) by ISOCAT_1:def 12;

          

           A71: (F1 /. fi) = (FF1 . (f,( id c))) by A68, CAT_3:def 10

          .= (( curry (F1,f)) . ( id c)) by FUNCT_5: 69

          .= ((F1 ?- f) qua Function of the carrier of B, the carrier' of C . c) by A70, FUNCT_2: 15

          .= (T13 . c) by A60, NATTRA_1:def 5;

          

           A72: (F2 /. fi) = (FF2 . (f,( id c))) by A68, CAT_3:def 10

          .= (( curry (F2,f)) . ( id c)) by FUNCT_5: 69

          .= ((F2 ?- f) qua Function of the carrier of B, the carrier' of C . c) by A70, FUNCT_2: 15

          .= (T24 . c) by A58, NATTRA_1:def 5;

          

           A73: ( Hom ((F1 . [a, c]),(F1 . [b, c]))) <> {} by A68, CAT_1: 84;

          

          thus ((T34 `*` T13) . c) = ((T34 . c) * (T13 . c)) by A59, A48, NATTRA_1: 25

          .= ((t . [b, c]) qua Morphism of C (*) (F1 /. fi)) by A63, A71, A65, CAT_1:def 13

          .= ((t . [b, c]) * (F1 /. fi)) by A62, A73, CAT_1:def 13

          .= ((F2 /. fi) * (t . [a, c])) by A1, A68, NATTRA_1:def 8

          .= ((F2 /. fi) (*) (t . [a, c]) qua Morphism of C) by A61, A69, CAT_1:def 13

          .= ((T24 . c) * (T12 . c)) by A64, A72, A66, CAT_1:def 13

          .= ((T24 `*` T12) . c) by A52, A57, NATTRA_1: 25;

        end;

        then

         A74: (T34 `*` T13) = (T24 `*` T12) by A53, A58, NATTRA_1: 18, NATTRA_1: 19;

        (F1 ?- ( dom f)) = (( export F1) . a) by A40, A43, CAT_1: 5;

        then

         A75: (( export F1) . g) = [ [S1, S3], T13] by A50, Def4;

        ( Hom ((( export F1) . b),(( export F2) . b))) <> {} by A34;

        

        hence ((G . b) * (( export F1) /. f)) = ((G . b) (*) (( export F1) /. f) qua Morphism of ( Functors (B,C))) by A56, CAT_1:def 13

        .= ((G . b) (*) (( export F1) . g)) by A40, CAT_3:def 10

        .= [ [S1, S4], (T34 `*` T13)] by A75, A51, NATTRA_1: 36

        .= ((( export F2) /. g) (*) (G . a)) by A55, A46, A74, NATTRA_1: 36

        .= ((( export F2) /. f) qua Morphism of ( Functors (B,C)) (*) (G . a)) by A40, CAT_3:def 10

        .= ((( export F2) /. f) * (G . a)) by A54, A41, CAT_1:def 13;

      end;

      

       A76: ( export F1) is_transformable_to ( export F2) by A37;

      hence ( export F1) is_naturally_transformable_to ( export F2) by A39;

      ( export F1) is_naturally_transformable_to ( export F2) by A39, A76;

      then

      reconsider G as natural_transformation of ( export F1), ( export F2) by A39, NATTRA_1:def 8;

      take G;

      let s be Function of [:the carrier of A, the carrier of B:], the carrier' of C;

      assume

       A77: t = s;

      let a be Object of A;

      

      thus (G . a) = (G . a qua set) by A38, NATTRA_1:def 5

      .= [ [(( export F1) . a), (( export F2) . a)], (( curry s) . a)] by A33, A77;

    end;

    definition

      let A, B, C;

      let F1,F2 be Functor of [:A, B:], C;

      let t be natural_transformation of F1, F2;

      :: ISOCAT_2:def5

      func export t -> natural_transformation of ( export F1), ( export F2) means

      : Def5: for s be Function of [:the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a be Object of A holds (it . a) = [ [(( export F1) . a), (( export F2) . a)], (( curry s) . a)];

      existence by A1, Th21;

      uniqueness

      proof

        reconsider s = t as Function of [:the carrier of A, the carrier of B:], the carrier' of C;

        let T1,T2 be natural_transformation of ( export F1), ( export F2) such that

         A2: for s be Function of [:the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a be Object of A holds (T1 . a) = [ [(( export F1) . a), (( export F2) . a)], (( curry s) . a)] and

         A3: for s be Function of [:the carrier of A, the carrier of B:], the carrier' of C st t = s holds for a be Object of A holds (T2 . a) = [ [(( export F1) . a), (( export F2) . a)], (( curry s) . a)];

         A4:

        now

          let a be Object of A;

          (T1 . a) = [ [(( export F1) . a), (( export F2) . a)], (( curry s) . a)] by A2;

          hence (T1 . a) = (T2 . a) by A3;

        end;

        ( export F1) is_naturally_transformable_to ( export F2) by A1, Th21;

        then ( export F1) is_transformable_to ( export F2);

        hence T1 = T2 by A4, NATTRA_1: 19;

      end;

    end

    theorem :: ISOCAT_2:24

    

     Th22: for F be Functor of [:A, B:], C holds ( id ( export F)) = ( export ( id F))

    proof

      let F be Functor of [:A, B:], C;

      reconsider s = ( id F) as Function of [:the carrier of A, the carrier of B:], the carrier' of C;

      now

        let a be Object of A;

        reconsider ff = (( export F) . a) as Functor of B, C by Th5;

         A1:

        now

          let b be Object of B;

          

          thus (( id ff) qua Function of the carrier of B, the carrier' of C . b) = (( id ff) . b) by NATTRA_1:def 5

          .= ( id (ff . b)) by NATTRA_1: 20

          .= (ff qua Function of the carrier' of B, the carrier' of C . ( id b)) by CAT_1: 71

          .= ((F ?- a) . ( id b)) by Th18

          .= (F . (( id a),( id b))) by CAT_2: 36

          .= (F . ( id [a, b]) qua Morphism of [:A, B:]) by CAT_2: 31

          .= ( id (F . [a, b])) by CAT_1: 71

          .= (( id F) . [a, b]) by NATTRA_1: 20

          .= (( id F) qua Function of the carrier of [:A, B:], the carrier' of C . (a,b)) by NATTRA_1:def 5

          .= ((( curry s) . a) . b) by FUNCT_5: 69;

        end;

        

        thus (( id ( export F)) . a) = ( id (( export F) . a)) by NATTRA_1: 20

        .= [ [ff, ff], ( id ff)] by NATTRA_1:def 17

        .= [ [(( export F) . a), (( export F) . a)], (( curry s) . a)] by A1, FUNCT_2: 63

        .= (( export ( id F)) . a) by Def5;

      end;

      hence thesis by NATTRA_1: 19;

    end;

    theorem :: ISOCAT_2:25

    

     Th23: for F1,F2,F3 be Functor of [:A, B:], C st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds for t1 be natural_transformation of F1, F2, t2 be natural_transformation of F2, F3 holds ( export (t2 `*` t1)) = (( export t2) `*` ( export t1))

    proof

      let F1,F2,F3 be Functor of [:A, B:], C such that

       A1: F1 is_naturally_transformable_to F2 and

       A2: F2 is_naturally_transformable_to F3;

      

       A3: F2 is_transformable_to F3 by A2;

      let t1 be natural_transformation of F1, F2, t2 be natural_transformation of F2, F3;

      

       A4: F1 is_transformable_to F2 by A1;

      

       A5: ( export F1) is_naturally_transformable_to ( export F2) by A1, Th21;

      then

       A6: ( export F1) is_transformable_to ( export F2);

      

       A7: ( export F2) is_naturally_transformable_to ( export F3) by A2, Th21;

      then

       A8: ( export F2) is_transformable_to ( export F3);

      

       A9: F1 is_naturally_transformable_to F3 by A1, A2, NATTRA_1: 23;

      then

       A10: F1 is_transformable_to F3;

      now

        let a be Object of A;

        reconsider S1 = (( export F1) . a), S2 = (( export F2) . a), S3 = (( export F3) . a) as Functor of B, C by Th5;

        reconsider s1 = t1, s2 = t2, s3 = (t2 `*` t1) as Function of [:the carrier of A, the carrier of B:], the carrier' of C;

        

         A11: S2 = (F2 ?- a) by Th18;

        

         A12: S3 = (F3 ?- a) by Th18;

        then

        reconsider T2 = (( curry s2) . a) as natural_transformation of S2, S3 by A2, A11, Th11;

        

         A13: S2 is_naturally_transformable_to S3 by A2, A11, A12, Th11;

        then

         A14: S2 is_transformable_to S3;

        

         A15: S1 = (F1 ?- a) by Th18;

        then

        reconsider T1 = (( curry s1) . a) as natural_transformation of S1, S2 by A1, A11, Th11;

        

         A16: (( export t2) . a) = [ [S2, S3], T2] & (( export t1) . a) = [ [S1, S2], T1] by A1, A2, Def5;

        

         A17: S1 is_naturally_transformable_to S2 by A1, A15, A11, Th11;

        then S1 is_naturally_transformable_to S3 by A13, NATTRA_1: 23;

        then

         A18: S1 is_transformable_to S3;

        reconsider T3 = (( curry s3) . a) as natural_transformation of S1, S3 by A9, A15, A12, Th11;

        

         A19: ( Hom ((( export F1) . a),(( export F2) . a))) <> {} & ( Hom ((( export F2) . a),(( export F3) . a))) <> {} by A6, A8;

        

         A20: S1 is_transformable_to S2 by A17;

        now

          let b be Object of B;

          

           A21: ( Hom ((F1 . [a, b]),(F2 . [a, b]))) <> {} & ( Hom ((F2 . [a, b]),(F3 . [a, b]))) <> {} by A4, A3;

          

           A22: ( Hom ((S1 . b),(S2 . b))) <> {} & ( Hom ((S2 . b),(S3 . b))) <> {} by A20, A14;

          

           A23: (T1 . b) = (T1 qua Function of the carrier of B, the carrier' of C . b) by A20, NATTRA_1:def 5

          .= (s1 . (a,b)) by FUNCT_5: 69

          .= (t1 . [a, b]) by A4, NATTRA_1:def 5;

          

           A24: (T2 . b) = (T2 qua Function of the carrier of B, the carrier' of C . b) by A14, NATTRA_1:def 5

          .= (s2 . (a,b)) by FUNCT_5: 69

          .= (t2 . [a, b]) by A3, NATTRA_1:def 5;

          

          thus (T3 . b) = (T3 qua Function of the carrier of B, the carrier' of C . b) by A18, NATTRA_1:def 5

          .= (s3 . (a,b)) by FUNCT_5: 69

          .= ((t2 `*` t1) . [a, b]) by A10, NATTRA_1:def 5

          .= ((t2 . [a, b]) * (t1 . [a, b])) by A1, A2, NATTRA_1: 25

          .= ((T2 . b) (*) (T1 . b) qua Morphism of C) by A21, A24, A23, CAT_1:def 13

          .= ((T2 . b) * (T1 . b)) by A22, CAT_1:def 13

          .= ((T2 `*` T1) . b) by A17, A13, NATTRA_1: 25;

        end;

        then

         A25: T3 = (T2 `*` T1) by A18, NATTRA_1: 19;

        

        thus (( export (t2 `*` t1)) . a) = [ [S1, S3], T3] by A9, Def5

        .= ((( export t2) . a) (*) (( export t1) . a) qua Morphism of ( Functors (B,C))) by A16, A25, NATTRA_1: 36

        .= ((( export t2) . a) * (( export t1) . a)) by A19, CAT_1:def 13

        .= ((( export t2) `*` ( export t1)) . a) by A5, A7, NATTRA_1: 25;

      end;

      hence thesis by A6, A8, NATTRA_1: 18, NATTRA_1: 19;

    end;

    theorem :: ISOCAT_2:26

    

     Th24: for F1,F2 be Functor of [:A, B:], C st F1 is_naturally_transformable_to F2 holds for t1,t2 be natural_transformation of F1, F2 holds ( export t1) = ( export t2) implies t1 = t2

    proof

      let F1,F2 be Functor of [:A, B:], C;

      assume

       A1: F1 is_naturally_transformable_to F2;

      then

       A2: F1 is_transformable_to F2;

      let t1,t2 be natural_transformation of F1, F2 such that

       A3: ( export t1) = ( export t2);

      now

        reconsider s1 = t1, s2 = t2 as Function of [:the carrier of A, the carrier of B:], the carrier' of C;

        let ab be Object of [:A, B:];

        consider a be Object of A, b be Object of B such that

         A4: ab = [a, b] by DOMAIN_1: 1;

         [ [(( export F1) . a), (( export F2) . a)], (( curry s1) . a)] = (( export t1) . a) by A1, Def5

        .= [ [(( export F1) . a), (( export F2) . a)], (( curry s2) . a)] by A1, A3, Def5;

        then

         A5: (( curry s1) . a) = (( curry s2) . a) by XTUPLE_0: 1;

        

        thus (t1 . ab) = (s1 . (a,b)) by A2, A4, NATTRA_1:def 5

        .= ((( curry s2) . a) . b) by A5, FUNCT_5: 69

        .= (s2 . (a,b)) by FUNCT_5: 69

        .= (t2 . ab) by A2, A4, NATTRA_1:def 5;

      end;

      hence thesis by A1, ISOCAT_1: 26;

    end;

    theorem :: ISOCAT_2:27

    

     Th25: for G be Functor of A, ( Functors (B,C)) holds ex F be Functor of [:A, B:], C st G = ( export F)

    proof

      let G be Functor of A, ( Functors (B,C));

      defpred P[ object, object] means for f be Morphism of A, g be Morphism of B st $1 = [f, g] holds for f1,f2 be Functor of B, C, t be natural_transformation of f1, f2 st (G . f) = [ [f1, f2], t] holds $2 = ((t . ( cod g)) (*) (f1 . g));

       A1:

      now

        let m be object;

        assume m in the carrier' of [:A, B:];

        then

        consider m1 be Morphism of A, m2 be Morphism of B such that

         A2: m = [m1, m2] by CAT_2: 27;

        consider F1,F2 be Functor of B, C, t1 be natural_transformation of F1, F2 such that F1 is_naturally_transformable_to F2 and ( dom (G . m1)) = F1 and ( cod (G . m1)) = F2 and

         A3: (G . m1) = [ [F1, F2], t1] by Th6;

        reconsider o = ((t1 . ( cod m2)) (*) (F1 . m2)) as object;

        take o;

        thus o in the carrier' of C;

        thus P[m, o]

        proof

          let f be Morphism of A, g be Morphism of B;

          assume

           A4: m = [f, g];

          then

           A5: g = m2 by A2, XTUPLE_0: 1;

          let f1,f2 be Functor of B, C, t be natural_transformation of f1, f2;

          assume

           A6: (G . f) = [ [f1, f2], t];

          

           A7: f = m1 by A2, A4, XTUPLE_0: 1;

          then [F1, F2] = [f1, f2] by A3, A6, XTUPLE_0: 1;

          then F1 = f1 & F2 = f2 by XTUPLE_0: 1;

          hence thesis by A3, A7, A5, A6, XTUPLE_0: 1;

        end;

      end;

      consider F be Function of the carrier' of [:A, B:], the carrier' of C such that

       A8: for m be object st m in the carrier' of [:A, B:] holds P[m, (F . m)] from FUNCT_2:sch 1( A1);

      F is Functor of [:A, B:], C

      proof

        thus for ab be Object of [:A, B:] holds ex c be Object of C st (F . ( id ab)) = ( id c)

        proof

          let ab be Object of [:A, B:];

          consider a be Object of A, b be Object of B such that

           A9: ab = [a, b] by CAT_2: 25;

          reconsider H = (G . a) as Functor of B, C by Th5;

          take (H . b);

          

           A10: ( Hom ((H . b),(H . b))) <> {} ;

          

           A11: (G . ( id a) qua Morphism of A) = ( id (G . a)) by CAT_1: 71

          .= [ [H, H], ( id H)] by NATTRA_1:def 17;

          ( id ab) = [( id a), ( id b)] by A9, CAT_2: 31;

          

          hence (F . ( id ab)) = ((( id H) . ( cod ( id b))) (*) (H . ( id b) qua Morphism of B)) by A8, A11

          .= ((( id H) . ( cod ( id b))) (*) ( id (H . b))) by CAT_1: 71

          .= ((( id H) . b) (*) ( id (H . b)) qua Morphism of C)

          .= (( id (H . b)) (*) ( id (H . b)) qua Morphism of C) by NATTRA_1: 20

          .= (( id (H . b)) * ( id (H . b))) by A10, CAT_1:def 13

          .= ( id (H . b));

        end;

        thus for f be Morphism of [:A, B:] holds (F . ( id ( dom f))) = ( id ( dom (F . f))) & (F . ( id ( cod f))) = ( id ( cod (F . f)))

        proof

          let f be Morphism of [:A, B:];

          consider f1 be Morphism of A, f2 be Morphism of B such that

           A12: f = [f1, f2] by CAT_2: 27;

          reconsider H = (G . ( dom f1)) as Functor of B, C by Th5;

          

           A13: ( Hom (( dom (H . f2)),( dom (H . f2)))) <> {} ;

          

           A14: ( id (G . ( dom f1))) = [ [H, H], ( id H)] & (G . ( id ( dom f1)) qua Morphism of A) = ( id (G . ( dom f1))) by CAT_1: 71, NATTRA_1:def 17;

          consider F1,F2 be Functor of B, C, t be natural_transformation of F1, F2 such that

           A15: F1 is_naturally_transformable_to F2 and

           A16: ( dom (G . f1)) = F1 and

           A17: ( cod (G . f1)) = F2 and

           A18: (G . f1) = [ [F1, F2], t] by Th6;

          

           A19: (F1 . ( cod f2)) = ( cod (F1 . f2)) by CAT_1: 72;

          ( Hom ((F1 . ( cod f2)),(F2 . ( cod f2)))) <> {} by A15, ISOCAT_1: 25;

          then

           A20: ( dom (t . ( cod f2))) = ( cod (F1 . f2)) by A19, CAT_1: 5;

          

           A21: F1 = H by A16, CAT_1: 72;

          ( id ( dom f)) = ( id [( dom f1), ( dom f2)]) by A12, CAT_2: 28

          .= [( id ( dom f1)), ( id ( dom f2))] by CAT_2: 31;

          

          hence (F . ( id ( dom f))) = ((( id H) . ( cod ( id ( dom f2)))) (*) (H . ( id ( dom f2)) qua Morphism of B)) by A8, A14

          .= ((( id H) . ( cod ( id ( dom f2)))) (*) ( id (H . ( dom f2)))) by CAT_1: 71

          .= ((( id H) . ( cod ( id ( dom f2)))) (*) ( id ( dom (H . f2)))) by CAT_1: 72

          .= ((( id H) . ( dom f2)) (*) ( id ( dom (H . f2))))

          .= (( id (H . ( dom f2))) (*) ( id ( dom (H . f2)))) by NATTRA_1: 20

          .= (( id ( dom (H . f2))) qua Morphism of C (*) ( id ( dom (H . f2)))) by CAT_1: 72

          .= (( id ( dom (H . f2))) * ( id ( dom (H . f2)))) by A13, CAT_1:def 13

          .= ( id ( dom (F1 . f2))) by A21

          .= ( id ( dom ((t . ( cod f2)) (*) (F1 . f2)))) by A20, CAT_1: 17

          .= ( id ( dom (F . f))) by A8, A12, A18;

          reconsider H = (G . ( cod f1)) as Functor of B, C by Th5;

          

           A22: F2 = H by A17, CAT_1: 72;

          

           A23: ( Hom (( cod (H . f2)),( cod (H . f2)))) <> {} ;

          

           A24: ( id ( cod f)) = ( id [( cod f1), ( cod f2)]) by A12, CAT_2: 28

          .= [( id ( cod f1)), ( id ( cod f2))] by CAT_2: 31;

          

           A25: ( Hom ((F1 . ( cod f2)),(F2 . ( cod f2)))) <> {} by A15, ISOCAT_1: 25;

          (F1 . ( cod f2)) = ( cod (F1 . f2)) by CAT_1: 72;

          then

           A26: ( dom (t . ( cod f2))) = ( cod (F1 . f2)) by A25, CAT_1: 5;

          ( id (G . ( cod f1))) = [ [H, H], ( id H)] & (G . ( id ( cod f1)) qua Morphism of A) = ( id (G . ( cod f1))) by CAT_1: 71, NATTRA_1:def 17;

          

          hence (F . ( id ( cod f))) = ((( id H) . ( cod ( id ( cod f2)))) (*) (H . ( id ( cod f2)) qua Morphism of B)) by A8, A24

          .= ((( id H) . ( cod ( id ( cod f2)))) (*) ( id (H . ( cod f2)))) by CAT_1: 71

          .= ((( id H) . ( cod ( id ( cod f2)))) (*) ( id ( cod (H . f2)))) by CAT_1: 72

          .= ((( id H) . ( cod f2)) (*) ( id ( cod (H . f2))))

          .= (( id (H . ( cod f2))) (*) ( id ( cod (H . f2)))) by NATTRA_1: 20

          .= (( id ( cod (H . f2))) qua Morphism of C (*) ( id ( cod (H . f2)))) by CAT_1: 72

          .= (( id ( cod (H . f2))) * ( id ( cod (H . f2)))) by A23, CAT_1:def 13

          .= ( id ( cod (H . f2)))

          .= ( id (F2 . ( cod f2))) by A22, CAT_1: 72

          .= ( id ( cod (t . ( cod f2)))) by A25, CAT_1: 5

          .= ( id ( cod ((t . ( cod f2)) (*) (F1 . f2)))) by A26, CAT_1: 17

          .= ( id ( cod (F . f))) by A8, A12, A18;

        end;

        let f,g be Morphism of [:A, B:] such that

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

        consider g1 be Morphism of A, g2 be Morphism of B such that

         A28: g = [g1, g2] by CAT_2: 27;

        reconsider g29 = g2 as Morphism of ( dom g2), ( cod g2) by CAT_1: 4;

        consider f1 be Morphism of A, f2 be Morphism of B such that

         A29: f = [f1, f2] by CAT_2: 27;

        

         A30: [( cod f1), ( cod f2)] = ( cod f) by A29, CAT_2: 28;

        consider G1,G2 be Functor of B, C, s be natural_transformation of G1, G2 such that

         A31: G1 is_naturally_transformable_to G2 and

         A32: ( dom (G . g1)) = G1 and ( cod (G . g1)) = G2 and

         A33: (G . g1) = [ [G1, G2], s] by Th6;

        consider F1,F2 be Functor of B, C, t be natural_transformation of F1, F2 such that

         A34: F1 is_naturally_transformable_to F2 and ( dom (G . f1)) = F1 and

         A35: ( cod (G . f1)) = F2 and

         A36: (G . f1) = [ [F1, F2], t] by Th6;

        

         A37: (F . f) = ((t . ( cod f2)) (*) (F1 . f2)) by A8, A29, A36;

        

         A38: [( dom g1), ( dom g2)] = ( dom g) by A28, CAT_2: 28;

        then

         A39: ( cod f1) = ( dom g1) by A27, A30, XTUPLE_0: 1;

        then

        reconsider s as natural_transformation of F2, G2 by A35, A32, CAT_1: 64;

        

         A40: ( cod f2) = ( dom g2) by A27, A30, A38, XTUPLE_0: 1;

        then

         A41: (g (*) f) = [(g1 (*) f1), (g2 (*) f2)] by A29, A28, A39, CAT_2: 29;

        reconsider f29 = f2 as Morphism of ( dom f2), ( dom g2) by A40, CAT_1: 4;

        

         A42: ( cod (g2 (*) f2)) = ( cod g2) by A40, CAT_1: 17;

        

         A43: ( Hom (( dom f2),( dom g2))) <> {} by A40, CAT_1: 2;

        then

         A44: ( Hom ((F1 . ( dom f2)),(F1 . ( dom g2)))) <> {} by CAT_1: 84;

        

         A45: ( Hom ((F1 . ( dom g2)),(F2 . ( dom g2)))) <> {} by A34, ISOCAT_1: 25;

        then

         A46: ( Hom ((F1 . ( dom f2)),(F2 . ( dom g2)))) <> {} by A44, CAT_1: 24;

        

         A47: ( Hom (( dom g2),( cod g2))) <> {} by CAT_1: 2;

        then

         A48: (F1 /. g2) = (F1 /. g29) by CAT_3:def 10;

        

         A49: F2 = G1 by A35, A32, A39, CAT_1: 64;

        then

         A50: ( Hom ((F2 . ( cod g2)),(G2 . ( cod g2)))) <> {} by A31, ISOCAT_1: 25;

        

         A51: (G1 /. g2) = (F2 /. g29) by A49, A47, CAT_3:def 10;

        

         A52: ( Hom ((F2 . ( dom g2)),(F2 . ( cod g2)))) <> {} by A47, CAT_1: 84;

        then

         A53: ( Hom ((F2 . ( dom g2)),(G2 . ( cod g2)))) <> {} by A50, CAT_1: 24;

        

         A54: ( Hom ((F1 . ( dom g2)),(F1 . ( cod g2)))) <> {} by A47, CAT_1: 84;

        then

         A55: ( Hom ((F1 . ( dom f2)),(F1 . ( cod g2)))) <> {} by A44, CAT_1: 24;

        

         A56: ( Hom ((F1 . ( cod g2)),(F2 . ( cod g2)))) <> {} by A34, ISOCAT_1: 25;

        then

         A57: ( Hom ((F1 . ( cod g2)),(G2 . ( cod g2)))) <> {} by A50, CAT_1: 24;

        

         A58: (F1 /. f2) = (F1 /. f29) by A43, CAT_3:def 10;

        (G . (g1 (*) f1)) = ((G . g1) (*) (G . f1)) by A39, CAT_1: 64

        .= [ [F1, G2], (s `*` t)] by A36, A33, A49, NATTRA_1: 36;

        

        hence (F . (g (*) f)) = (((s `*` t) . ( cod (g2 (*) f2))) (*) (F1 . (g2 (*) f2))) by A8, A41

        .= (((s . ( cod g2)) * (t . ( cod g2))) (*) (F1 . (g2 (*) f2))) by A34, A31, A49, A42, NATTRA_1: 25

        .= (((s . ( cod g2)) * (t . ( cod g2))) (*) ((F1 /. g2) (*) (F1 /. f2))) by A40, CAT_1: 64

        .= (((s . ( cod g2)) * (t . ( cod g2))) (*) ((F1 /. g29) * (F1 /. f29)) qua Morphism of C) by A44, A54, A48, A58, CAT_1:def 13

        .= (((s . ( cod g2)) * (t . ( cod g2))) * ((F1 /. g29) * (F1 /. f29))) by A55, A57, CAT_1:def 13

        .= ((s . ( cod g2)) * ((t . ( cod g2)) * ((F1 /. g29) * (F1 /. f29)))) by A50, A56, A55, CAT_1: 25

        .= ((s . ( cod g2)) * (((t . ( cod g2)) * (F1 /. g29)) * (F1 /. f29))) by A56, A44, A54, CAT_1: 25

        .= ((s . ( cod g2)) * (((F2 /. g29) * (t . ( dom g2))) * (F1 /. f29))) by A34, A47, NATTRA_1:def 8

        .= ((s . ( cod g2)) * ((F2 /. g29) * ((t . ( dom g2)) * (F1 /. f29)))) by A44, A52, A45, CAT_1: 25

        .= (((s . ( cod g2)) * (F2 /. g29)) * ((t . ( dom g2)) * (F1 /. f29))) by A50, A52, A46, CAT_1: 25

        .= (((s . ( cod g2)) * (F2 /. g29)) (*) ((t . ( dom g2)) * (F1 /. f29)) qua Morphism of C) by A46, A53, CAT_1:def 13

        .= (((s . ( cod g2)) * (F2 /. g29)) (*) ((t . ( cod f2)) (*) (F1 . f2))) by A40, A44, A45, A58, CAT_1:def 13

        .= (((s . ( cod g2)) (*) (G1 /. g2)) (*) ((t . ( cod f2)) (*) (F1 . f2))) by A50, A52, A51, CAT_1:def 13

        .= ((F . g) (*) (F . f)) by A8, A28, A33, A49, A37;

      end;

      then

      reconsider F as Functor of [:A, B:], C;

      take F;

      now

        let f be Morphism of A;

        consider f1,f2 be Functor of B, C, t be natural_transformation of f1, f2 such that

         A59: f1 is_naturally_transformable_to f2 and

         A60: ( dom (G . f)) = f1 and

         A61: ( cod (G . f)) = f2 and

         A62: (G . f) = [ [f1, f2], t] by Th6;

        now

          let g be Morphism of B;

          

           A63: ( dom ( id ( cod g))) = ( cod g);

          

           A64: f1 = (G . ( dom f)) by A60, CAT_1: 72;

          

           A65: (G . ( id ( dom f)) qua Morphism of A) = ( id (G . ( dom f))) by CAT_1: 71

          .= [ [f1, f1], ( id f1)] by A64, NATTRA_1:def 17;

          

          thus ((F ?- ( dom f)) . g) = (F . (( id ( dom f)),g)) by CAT_2: 36

          .= (F . [( id ( dom f)), g])

          .= ((( id f1) . ( cod g)) (*) (f1 . g)) by A8, A65

          .= (( id (f1 . ( cod g)) qua Object of C) (*) (f1 . g)) by NATTRA_1: 20

          .= ((f1 . ( id ( cod g)) qua Morphism of B) (*) (f1 . g)) by CAT_1: 71

          .= (f1 . (( id ( cod g)) qua Morphism of B (*) g)) by A63, CAT_1: 64

          .= (f1 . g) by CAT_1: 21;

        end;

        then

         A66: f1 = (F ?- ( dom f)) by FUNCT_2: 63;

        now

          let g be Morphism of B;

          

           A67: ( dom ( id ( cod g))) = ( cod g);

          

           A68: f2 = (G . ( cod f)) by A61, CAT_1: 72;

          

           A69: (G . ( id ( cod f)) qua Morphism of A) = ( id (G . ( cod f))) by CAT_1: 71

          .= [ [f2, f2], ( id f2)] by A68, NATTRA_1:def 17;

          

          thus ((F ?- ( cod f)) . g) = (F . (( id ( cod f)),g)) by CAT_2: 36

          .= (F . [( id ( cod f)), g])

          .= ((( id f2) . ( cod g)) (*) (f2 . g)) by A8, A69

          .= (( id (f2 . ( cod g)) qua Object of C) (*) (f2 . g)) by NATTRA_1: 20

          .= ((f2 . ( id ( cod g)) qua Morphism of B) (*) (f2 . g)) by CAT_1: 71

          .= (f2 . (( id ( cod g)) qua Morphism of B (*) g)) by A67, CAT_1: 64

          .= (f2 . g) by CAT_1: 21;

        end;

        then

         A70: f2 = (F ?- ( cod f)) by FUNCT_2: 63;

        now

          let b be Object of B;

          

           A71: ( Hom ((f1 . b),(f1 . b))) <> {} ;

          

           A72: ( Hom ((f1 . b),(f2 . b))) <> {} by A59, ISOCAT_1: 25;

          

          thus ((F ?- f) . b) = (F . (f,( id b))) by Th15

          .= (F . [f, ( id b)])

          .= ((t . ( cod ( id b))) (*) (f1 . ( id b) qua Morphism of B)) by A8, A62

          .= ((t . ( cod ( id b))) (*) ( id (f1 . b))) by CAT_1: 71

          .= ((t . b) (*) ( id (f1 . b)) qua Morphism of C)

          .= ((t . b) * ( id (f1 . b))) by A72, A71, CAT_1:def 13

          .= (t . b) by A72, CAT_1: 29;

        end;

        hence (G . f) = [ [(F ?- ( dom f)), (F ?- ( cod f))], (F ?- f)] by A59, A62, A66, A70, ISOCAT_1: 26;

      end;

      hence thesis by Def4;

    end;

    theorem :: ISOCAT_2:28

    

     Th26: for F1,F2 be Functor of [:A, B:], C st ( export F1) is_naturally_transformable_to ( export F2) holds for t be natural_transformation of ( export F1), ( export F2) holds F1 is_naturally_transformable_to F2 & ex u be natural_transformation of F1, F2 st t = ( export u)

    proof

      let F1,F2 be Functor of [:A, B:], C such that

       A1: ( export F1) is_naturally_transformable_to ( export F2);

      let t be natural_transformation of ( export F1), ( export F2);

      defpred P[ object, object] means for a be Object of A st $1 = a holds (t . a) = [ [(( export F1) . a), (( export F2) . a)], $2];

       A2:

      now

        let o be object;

        assume o in the carrier of A;

        then

        reconsider a9 = o as Object of A;

        consider f1,f2 be Functor of B, C, tau be natural_transformation of f1, f2 such that f1 is_naturally_transformable_to f2 and

         A3: ( dom (t . a9)) = f1 and

         A4: ( cod (t . a9)) = f2 & (t . a9) = [ [f1, f2], tau] by Th6;

        reconsider m = tau as object;

        take m;

        thus m in ( Funcs (the carrier of B,the carrier' of C)) by FUNCT_2: 8;

        thus P[o, m]

        proof

          let a be Object of A such that

           A5: o = a;

          ( export F1) is_transformable_to ( export F2) by A1;

          then

           A6: ( Hom ((( export F1) . a),(( export F2) . a))) <> {} ;

          then (( export F1) . a) = f1 by A3, A5, CAT_1: 5;

          hence thesis by A4, A5, A6, CAT_1: 5;

        end;

      end;

      consider t9 be Function of the carrier of A, ( Funcs (the carrier of B,the carrier' of C)) such that

       A7: for o be object st o in the carrier of A holds P[o, (t9 . o)] from FUNCT_2:sch 1( A2);

      reconsider u9 = ( uncurry t9) as Function of the carrier of [:A, B:], the carrier' of C;

       A8:

      now

        let ab be Object of [:A, B:];

        consider a be Object of A, b be Object of B such that

         A9: ab = [a, b] by DOMAIN_1: 1;

        (( export F1) . a) = (F1 ?- a) & (( export F2) . a) = (F2 ?- a) by Th18;

        then (t . a) = [ [(F1 ?- a), (F2 ?- a)], (t9 . a)] by A7;

        then [ [(F1 ?- a), (F2 ?- a)], (t9 . a)] in the carrier' of ( Functors (B,C));

        then [ [(F1 ?- a), (F2 ?- a)], (t9 . a)] in ( NatTrans (B,C)) by NATTRA_1:def 17;

        then

        consider G1,G2 be Functor of B, C, t99 be natural_transformation of G1, G2 such that

         A10: [ [(F1 ?- a), (F2 ?- a)], (t9 . a)] = [ [G1, G2], t99] and

         A11: G1 is_naturally_transformable_to G2 by NATTRA_1:def 15;

        

         A12: G1 is_transformable_to G2 by A11;

        

         A13: [(F1 ?- a), (F2 ?- a)] = [G1, G2] by A10, XTUPLE_0: 1;

        

         A14: (F1 . [a, b]) = ((F1 ?- a) . b) by Th8

        .= (G1 . b) by A13, XTUPLE_0: 1;

        

         A15: ( Hom ((G1 . b),(G2 . b))) <> {} by A11, ISOCAT_1: 25;

        

         A16: (F2 . [a, b]) = ((F2 ?- a) . b) by Th8

        .= (G2 . b) by A13, XTUPLE_0: 1;

        (u9 . (a,b)) = ((t9 . a) . b) by Th2

        .= (t99 qua Function of the carrier of B, the carrier' of C . b) by A10, XTUPLE_0: 1

        .= (t99 . b) by A12, NATTRA_1:def 5;

        hence (u9 . ab) in ( Hom ((F1 . ab),(F2 . ab))) by A9, A14, A16, A15, CAT_1:def 5;

      end;

      

       A17: F1 is_transformable_to F2 by A8;

      u9 is transformation of F1, F2

      proof

        thus F1 is_transformable_to F2 by A17;

        let a be Object of [:A, B:];

        (u9 . a) in ( Hom ((F1 . a),(F2 . a))) by A8;

        hence thesis by CAT_1:def 5;

      end;

      then

      reconsider u = u9 as transformation of F1, F2;

       A18:

      now

        reconsider FF1 = F1, FF2 = F2 as Function of [:the carrier' of A, the carrier' of B:], the carrier' of C;

        let ab1,ab2 be Object of [:A, B:] such that

         A19: ( Hom (ab1,ab2)) <> {} ;

        

         A20: ( Hom ((F2 . ab1),(F2 . ab2))) <> {} by A19, CAT_1: 84;

        consider a2 be Object of A, b2 be Object of B such that

         A21: ab2 = [a2, b2] by DOMAIN_1: 1;

        (( export F1) . a2) = (F1 ?- a2) & (( export F2) . a2) = (F2 ?- a2) by Th18;

        then (t . a2) = [ [(F1 ?- a2), (F2 ?- a2)], (t9 . a2)] by A7;

        then [ [(F1 ?- a2), (F2 ?- a2)], (t9 . a2)] in the carrier' of ( Functors (B,C));

        then [ [(F1 ?- a2), (F2 ?- a2)], (t9 . a2)] in ( NatTrans (B,C)) by NATTRA_1:def 17;

        then

        consider G2,H2 be Functor of B, C, t2 be natural_transformation of G2, H2 such that

         A22: [ [(F1 ?- a2), (F2 ?- a2)], (t9 . a2)] = [ [G2, H2], t2] and

         A23: G2 is_naturally_transformable_to H2 by NATTRA_1:def 15;

        

         A24: (t9 . a2) = t2 & G2 is_transformable_to H2 by A22, A23, XTUPLE_0: 1;

        consider a1 be Object of A, b1 be Object of B such that

         A25: ab1 = [a1, b1] by DOMAIN_1: 1;

        (( export F1) . a1) = (F1 ?- a1) & (( export F2) . a1) = (F2 ?- a1) by Th18;

        then (t . a1) = [ [(F1 ?- a1), (F2 ?- a1)], (t9 . a1)] by A7;

        then [ [(F1 ?- a1), (F2 ?- a1)], (t9 . a1)] in the carrier' of ( Functors (B,C));

        then [ [(F1 ?- a1), (F2 ?- a1)], (t9 . a1)] in ( NatTrans (B,C)) by NATTRA_1:def 17;

        then

        consider G1,H1 be Functor of B, C, t1 be natural_transformation of G1, H1 such that

         A26: [ [(F1 ?- a1), (F2 ?- a1)], (t9 . a1)] = [ [G1, H1], t1] and

         A27: G1 is_naturally_transformable_to H1 by NATTRA_1:def 15;

        

         A28: (t9 . a1) = t1 & G1 is_transformable_to H1 by A26, A27, XTUPLE_0: 1;

        

         A29: (u . ab1) = (u9 . (a1,b1)) by A17, A25, NATTRA_1:def 5

        .= ((t9 . a1) . b1) by Th2

        .= (t1 . b1) by A28, NATTRA_1:def 5;

        

         A30: ( Hom ((G1 . b2),(H1 . b2))) <> {} by A27, ISOCAT_1: 25;

        

         A31: ( Hom ((F1 . ab1),(F1 . ab2))) <> {} by A19, CAT_1: 84;

        

         A32: ( Hom ((F1 . ab2),(F2 . ab2))) <> {} by A17;

        (( export F2) . a1) = (F2 ?- a1) & (( export F1) . a1) = (F1 ?- a1) by Th18;

        then

         A33: (t . a1) = [ [G1, H1], t1] by A7, A26;

        

         A34: ( Hom ((G1 . b1),(H1 . b1))) <> {} by A27, ISOCAT_1: 25;

        (( export F1) . a2) = (F1 ?- a2) & (( export F2) . a2) = (F2 ?- a2) by Th18;

        then

         A35: (t . a2) = [ [G2, H2], t2] by A7, A22;

        

         A36: ( Hom ((( export F1) . a2),(( export F2) . a2))) <> {} by A1, ISOCAT_1: 25;

        

         A37: ( Hom ((( export F1) . a1),(( export F2) . a1))) <> {} by A1, ISOCAT_1: 25;

        let f be Morphism of ab1, ab2;

        consider g be Morphism of A, h be Morphism of B such that

         A38: f = [g, h] by DOMAIN_1: 1;

        reconsider g as Morphism of a1, a2 by A19, A25, A21, A38, Th10;

        

         A39: ( Hom (a1,a2)) <> {} by A19, A25, A21, Th9;

        then

         A40: ( dom g) = a1 & ( cod g) = a2 by CAT_1: 5;

        reconsider h as Morphism of b1, b2 by A19, A25, A21, A38, Th10;

        reconsider g9 = g as Morphism of A;

        reconsider h9 = h as Morphism of B;

        reconsider f9 = f as Morphism of [:A, B:];

        

         A41: ( dom ( id b2)) = b2;

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

        

        then

         A42: (g9 (*) ( id a1)) = (g * ( id a1)) by A39, CAT_1:def 13

        .= g by A39, CAT_1: 29;

        

         A43: ( dom g) = a1 by A39, CAT_1: 5;

        

         A44: ( Hom ((( export F2) . a1),(( export F2) . a2))) <> {} by A39, CAT_1: 84;

        reconsider e1 = (( export F1) /. g), e2 = (( export F2) /. g) as Morphism of ( Functors (B,C));

        

         A45: ( Hom ((F1 . ab1),(F2 . ab1))) <> {} by A17;

        

         A46: ( Hom (b1,b2)) <> {} by A19, A25, A21, Th9;

        then

         A47: ( Hom ((G1 . b1),(G1 . b2))) <> {} by CAT_1: 84;

        

         A48: [(F1 ?- a1), (F2 ?- a1)] = [G1, H1] by A26, XTUPLE_0: 1;

        then

         A49: (F2 ?- a1) = H1 by XTUPLE_0: 1;

        

        then

         A50: (H1 /. h) = ((F2 ?- a1) /. h qua Morphism of B) by A46, CAT_3:def 10

        .= (F2 . (( id a1),h)) by CAT_2: 36;

        

         A51: [(F1 ?- a2), (F2 ?- a2)] = [G2, H2] by A22, XTUPLE_0: 1;

        then

         A52: (F2 ?- a2) = H2 by XTUPLE_0: 1;

        then

         A53: ( Hom ((H1 . b2),(H2 . b2))) <> {} by A49, A40, Th14, ISOCAT_1: 25;

        

         A54: (F1 ?- a2) = G2 by A51, XTUPLE_0: 1;

        then

        reconsider v1 = (F1 ?- g) as natural_transformation of G1, G2 by A48, A40, XTUPLE_0: 1;

        

         A55: ( Hom ((( export F1) . a1),(( export F1) . a2))) <> {} by A39, CAT_1: 84;

        ( cod ( id a1)) = a1 & ( cod h) = b2 by A46, CAT_1: 5;

        

        then

         A56: ( cod [( id a1), h]) = [a1, b2] by CAT_2: 28

        .= ( dom [g, ( id b2)]) by A43, A41, CAT_2: 28;

        reconsider v2 = (F2 ?- g) as natural_transformation of H1, H2 by A48, A52, A40, XTUPLE_0: 1;

        

         A57: (( export F2) . g9) = [ [H1, H2], v2] by A49, A52, A40, Def4;

        

         A58: ( id b2) = (( IdMap B) . b2) by ISOCAT_1:def 12;

        

         A59: H1 is_naturally_transformable_to H2 by A49, A52, A40, Th14;

        then H1 is_transformable_to H2;

        

        then

         A60: (v2 . b2) = ((( curry (F2,g)) * ( IdMap B)) . b2) by NATTRA_1:def 5

        .= (( curry (F2,g)) . (( IdMap B) . b2)) by FUNCT_2: 15

        .= (F2 . (g,( id b2))) by A58, FUNCT_5: 69;

        

         A61: (F1 ?- a1) = G1 by A48, XTUPLE_0: 1;

        

        then

         A62: (G1 /. h) = ((F1 ?- a1) /. h qua Morphism of B) by A46, CAT_3:def 10

        .= (F1 . (( id a1),h)) by CAT_2: 36;

        (( export F1) . g9) = [ [G1, G2], v1] by A61, A54, A40, Def4;

        

        then [ [G1, H2], (t2 `*` v1)] = ((t . a2) (*) (( export F1) . g9)) by A35, NATTRA_1: 36

        .= ((t . a2) (*) e1) by A39, CAT_3:def 10

        .= ((t . a2) * (( export F1) /. g)) by A55, A36, CAT_1:def 13

        .= ((( export F2) /. g) * (t . a1)) by A1, A39, NATTRA_1:def 8

        .= (e2 (*) (t . a1)) by A44, A37, CAT_1:def 13

        .= ((( export F2) . g9) (*) (t . a1)) by A39, CAT_3:def 10

        .= [ [G1, H2], (v2 `*` t1)] by A57, A33, NATTRA_1: 36;

        then

         A63: (t2 `*` v1) = (v2 `*` t1) by XTUPLE_0: 1;

        

         A64: ( id b2) = (( IdMap B) . b2) by ISOCAT_1:def 12;

        

         A65: G1 is_naturally_transformable_to G2 by A61, A54, A40, Th14;

        then G1 is_transformable_to G2;

        

        then

         A66: (v1 . b2) = ((( curry (F1,g)) * ( IdMap B)) . b2) by NATTRA_1:def 5

        .= (( curry (F1,g)) . (( IdMap B) . b2)) by FUNCT_2: 15

        .= (F1 . (g,( id b2))) by A64, FUNCT_5: 69;

        

         A67: (u . ab2) = (u9 . (a2,b2)) by A17, A21, NATTRA_1:def 5

        .= ((t9 . a2) . b2) by Th2

        .= (t2 . b2) by A24, NATTRA_1:def 5;

        

         A68: ( Hom ((G2 . b2),(H2 . b2))) <> {} by A23, ISOCAT_1: 25;

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

        

        then (( id b2) (*) h9) = (( id b2) * h) by A46, CAT_1:def 13

        .= h by A46, CAT_1: 28;

        then

         A69: f = ( [g, ( id b2)] (*) [( id a1), h]) by A38, A42, A56, CAT_2: 30;

        

         A70: ( Hom ((H1 . b1),(H1 . b2))) <> {} by A46, CAT_1: 84;

        then

         A71: ( Hom ((H1 . b1),(H2 . b2))) <> {} by A53, CAT_1: 24;

        

         A72: (F2 /. f) = (F2 /. f9) by A19, CAT_3:def 10

        .= ((v2 . b2) (*) (H1 /. h) qua Morphism of C) by A56, A69, A60, A50, CAT_1: 64

        .= ((v2 . b2) * (H1 /. h)) by A53, A70, CAT_1:def 13;

        

         A73: ( Hom ((G1 . b2),(G2 . b2))) <> {} by A61, A54, A40, Th14, ISOCAT_1: 25;

        then

         A74: ( Hom ((G1 . b1),(G2 . b2))) <> {} by A47, CAT_1: 24;

        (F1 /. f) = (F1 /. f9) by A19, CAT_3:def 10

        .= ((v1 . b2) (*) (G1 /. h) qua Morphism of C) by A56, A69, A66, A62, CAT_1: 64

        .= ((v1 . b2) * (G1 /. h)) by A73, A47, CAT_1:def 13;

        

        hence ((u . ab2) * (F1 /. f)) = ((t2 . b2) (*) ((v1 . b2) * (G1 /. h)) qua Morphism of C) by A31, A32, A67, CAT_1:def 13

        .= ((t2 . b2) * ((v1 . b2) * (G1 /. h))) by A68, A74, CAT_1:def 13

        .= (((t2 . b2) * (v1 . b2)) * (G1 /. h)) by A68, A73, A47, CAT_1: 25

        .= (((v2 `*` t1) . b2) * (G1 /. h)) by A23, A65, A63, NATTRA_1: 25

        .= (((v2 . b2) * (t1 . b2)) * (G1 /. h)) by A27, A59, NATTRA_1: 25

        .= ((v2 . b2) * ((t1 . b2) * (G1 /. h))) by A47, A53, A30, CAT_1: 25

        .= ((v2 . b2) * ((H1 /. h) * (t1 . b1))) by A27, A46, NATTRA_1:def 8

        .= (((v2 . b2) * (H1 /. h)) * (t1 . b1)) by A53, A70, A34, CAT_1: 25

        .= ((F2 /. f) (*) (u . ab1) qua Morphism of C) by A34, A71, A29, A72, CAT_1:def 13

        .= ((F2 /. f) * (u . ab1)) by A45, A20, CAT_1:def 13;

      end;

      hence

       A75: F1 is_naturally_transformable_to F2 by A17;

      then

      reconsider u as natural_transformation of F1, F2 by A18, NATTRA_1:def 8;

      take u;

      now

        let s be Function of [:the carrier of A, the carrier of B:], the carrier' of C such that

         A76: u = s;

        let a be Object of A;

        t9 = ( curry u9) by Th1;

        hence (t . a) = [ [(( export F1) . a), (( export F2) . a)], (( curry s) . a)] by A7, A76;

      end;

      hence thesis by A75, Def5;

    end;

    definition

      let A, B, C;

      :: ISOCAT_2:def6

      func export (A,B,C) -> Functor of ( Functors ( [:A, B:],C)), ( Functors (A,( Functors (B,C)))) means

      : Def6: for F1,F2 be Functor of [:A, B:], C st F1 is_naturally_transformable_to F2 holds for t be natural_transformation of F1, F2 holds (it . [ [F1, F2], t]) = [ [( export F1), ( export F2)], ( export t)];

      existence

      proof

        defpred P[ object, object] means for F1,F2 be Functor of [:A, B:], C, t be natural_transformation of F1, F2 st $1 = [ [F1, F2], t] holds $2 = [ [( export F1), ( export F2)], ( export t)];

         A1:

        now

          let o be object;

          assume o in the carrier' of ( Functors ( [:A, B:],C));

          then o in ( NatTrans ( [:A, B:],C)) by NATTRA_1:def 17;

          then

          consider F1,F2 be Functor of [:A, B:], C, t be natural_transformation of F1, F2 such that

           A2: o = [ [F1, F2], t] and

           A3: F1 is_naturally_transformable_to F2 by NATTRA_1:def 16;

          reconsider m = [ [( export F1), ( export F2)], ( export t)] as object;

          take m;

          ( export F1) is_naturally_transformable_to ( export F2) by A3, Th21;

          then m in ( NatTrans (A,( Functors (B,C)))) by NATTRA_1:def 16;

          hence m in the carrier' of ( Functors (A,( Functors (B,C)))) by NATTRA_1:def 17;

          thus P[o, m]

          proof

            let F19,F29 be Functor of [:A, B:], C, t9 be natural_transformation of F19, F29;

            assume

             A4: o = [ [F19, F29], t9];

            then [F1, F2] = [F19, F29] by A2, XTUPLE_0: 1;

            then F1 = F19 & F2 = F29 by XTUPLE_0: 1;

            hence thesis by A2, A4, XTUPLE_0: 1;

          end;

        end;

        consider FF be Function of the carrier' of ( Functors ( [:A, B:],C)), the carrier' of ( Functors (A,( Functors (B,C)))) such that

         A5: for o be object st o in the carrier' of ( Functors ( [:A, B:],C)) holds P[o, (FF . o)] from FUNCT_2:sch 1( A1);

        FF is Functor of ( Functors ( [:A, B:],C)), ( Functors (A,( Functors (B,C))))

        proof

          thus for c be Object of ( Functors ( [:A, B:],C)) holds ex d be Object of ( Functors (A,( Functors (B,C)))) st (FF . ( id c)) = ( id d)

          proof

            let c be Object of ( Functors ( [:A, B:],C));

            reconsider F = c as Functor of [:A, B:], C by Th5;

            reconsider d = ( export F) as Object of ( Functors (A,( Functors (B,C)))) by Th5;

            take d;

            

             A6: ( id ( export F)) = ( export ( id F)) by Th22;

            ( id c) = [ [F, F], ( id F)] by NATTRA_1:def 17;

            

            hence (FF . ( id c)) = [ [( export F), ( export F)], ( export ( id F))] by A5

            .= ( id d) by A6, NATTRA_1:def 17;

          end;

          thus for f be Morphism of ( Functors ( [:A, B:],C)) holds (FF . ( id ( dom f))) = ( id ( dom (FF . f))) & (FF . ( id ( cod f))) = ( id ( cod (FF . f)))

          proof

            let f be Morphism of ( Functors ( [:A, B:],C));

            consider F1,F2 be Functor of [:A, B:], C, t be natural_transformation of F1, F2 such that F1 is_naturally_transformable_to F2 and

             A7: ( dom f) = F1 and

             A8: ( cod f) = F2 and

             A9: f = [ [F1, F2], t] by Th6;

            

             A10: (FF . f) = [ [( export F1), ( export F2)], ( export t)] by A5, A9;

            then

             A11: ( dom (FF . f)) = ( export F1) by NATTRA_1: 33;

            ( id ( dom f)) = [ [F1, F1], ( id F1)] by A7, NATTRA_1:def 17;

            

            hence (FF . ( id ( dom f))) = [ [( export F1), ( export F1)], ( export ( id F1))] by A5

            .= [ [( export F1), ( export F1)], ( id ( export F1))] by Th22

            .= ( id ( dom (FF . f))) by A11, NATTRA_1:def 17;

            

             A12: ( cod (FF . f)) = ( export F2) by A10, NATTRA_1: 33;

            ( id ( cod f)) = [ [F2, F2], ( id F2)] by A8, NATTRA_1:def 17;

            

            hence (FF . ( id ( cod f))) = [ [( export F2), ( export F2)], ( export ( id F2))] by A5

            .= [ [( export F2), ( export F2)], ( id ( export F2))] by Th22

            .= ( id ( cod (FF . f))) by A12, NATTRA_1:def 17;

          end;

          let f,g be Morphism of ( Functors ( [:A, B:],C));

          consider F1,F2 be Functor of [:A, B:], C, t be natural_transformation of F1, F2 such that

           A13: F1 is_naturally_transformable_to F2 and ( dom f) = F1 and

           A14: ( cod f) = F2 and

           A15: f = [ [F1, F2], t] by Th6;

          

           A16: (FF . f) = [ [( export F1), ( export F2)], ( export t)] by A5, A15;

          consider G1,G2 be Functor of [:A, B:], C, u be natural_transformation of G1, G2 such that

           A17: G1 is_naturally_transformable_to G2 and

           A18: ( dom g) = G1 and ( cod g) = G2 and

           A19: g = [ [G1, G2], u] by Th6;

          assume

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

          then

          reconsider u as natural_transformation of F2, G2 by A14, A18;

          (g (*) f) = [ [F1, G2], (u `*` t)] by A14, A15, A18, A19, A20, NATTRA_1: 36;

          then

           A21: (FF . (g (*) f)) = [ [( export F1), ( export G2)], ( export (u `*` t))] by A5;

          (FF . g) = [ [( export F2), ( export G2)], ( export u)] & (( export u) `*` ( export t)) = ( export (u `*` t)) by A5, A13, A14, A17, A18, A19, A20, Th23;

          hence thesis by A16, A21, NATTRA_1: 36;

        end;

        then

        reconsider FF as Functor of ( Functors ( [:A, B:],C)), ( Functors (A,( Functors (B,C))));

        take FF;

        let F1,F2 be Functor of [:A, B:], C such that

         A22: F1 is_naturally_transformable_to F2;

        let t be natural_transformation of F1, F2;

         [ [F1, F2], t] in ( NatTrans ( [:A, B:],C)) by A22, NATTRA_1: 32;

        then [ [F1, F2], t] in the carrier' of ( Functors ( [:A, B:],C)) by NATTRA_1:def 17;

        hence thesis by A5;

      end;

      uniqueness

      proof

        let IT1,IT2 be Functor of ( Functors ( [:A, B:],C)), ( Functors (A,( Functors (B,C)))) such that

         A23: for F1,F2 be Functor of [:A, B:], C st F1 is_naturally_transformable_to F2 holds for t be natural_transformation of F1, F2 holds (IT1 . [ [F1, F2], t]) = [ [( export F1), ( export F2)], ( export t)] and

         A24: for F1,F2 be Functor of [:A, B:], C st F1 is_naturally_transformable_to F2 holds for t be natural_transformation of F1, F2 holds (IT2 . [ [F1, F2], t]) = [ [( export F1), ( export F2)], ( export t)];

        now

          let f be Morphism of ( Functors ( [:A, B:],C));

          consider F1,F2 be Functor of [:A, B:], C, t be natural_transformation of F1, F2 such that

           A25: F1 is_naturally_transformable_to F2 and ( dom f) = F1 and ( cod f) = F2 and

           A26: f = [ [F1, F2], t] by Th6;

          

          thus (IT1 qua Function of the carrier' of ( Functors ( [:A, B:],C)), the carrier' of ( Functors (A,( Functors (B,C)))) . f) = [ [( export F1), ( export F2)], ( export t)] by A23, A25, A26

          .= (IT2 qua Function of the carrier' of ( Functors ( [:A, B:],C)), the carrier' of ( Functors (A,( Functors (B,C)))) . f) by A24, A25, A26;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    registration

      let A, B, C;

      cluster ( export (A,B,C)) -> isomorphic;

      coherence

      proof

        thus ( export (A,B,C)) is one-to-one

        proof

          let x1,x2 be object;

          assume x1 in ( dom ( export (A,B,C)));

          then

          reconsider f1 = x1 as Morphism of ( Functors ( [:A, B:],C));

          consider F1,F2 be Functor of [:A, B:], C, t be natural_transformation of F1, F2 such that

           A1: F1 is_naturally_transformable_to F2 and ( dom f1) = F1 and ( cod f1) = F2 and

           A2: f1 = [ [F1, F2], t] by Th6;

          assume x2 in ( dom ( export (A,B,C)));

          then

          reconsider f2 = x2 as Morphism of ( Functors ( [:A, B:],C));

          consider G1,G2 be Functor of [:A, B:], C, u be natural_transformation of G1, G2 such that

           A3: G1 is_naturally_transformable_to G2 and ( dom f2) = G1 and ( cod f2) = G2 and

           A4: f2 = [ [G1, G2], u] by Th6;

          assume (( export (A,B,C)) . x1) = (( export (A,B,C)) . x2);

          

          then

           A5: [ [( export F1), ( export F2)], ( export t)] = (( export (A,B,C)) . [ [G1, G2], u]) by A1, A2, A4, Def6

          .= [ [( export G1), ( export G2)], ( export u)] by A3, Def6;

          then

           A6: [( export F1), ( export F2)] = [( export G1), ( export G2)] by XTUPLE_0: 1;

          then ( export F1) = ( export G1) by XTUPLE_0: 1;

          then

           A7: F1 = G1 by Th20;

          ( export F2) = ( export G2) by A6, XTUPLE_0: 1;

          then

           A8: F2 = G2 by Th20;

          ( export u) = ( export t) by A5, XTUPLE_0: 1;

          hence thesis by A1, A2, A4, A7, A8, Th24;

        end;

        thus ( rng ( export (A,B,C))) c= the carrier' of ( Functors (A,( Functors (B,C))));

        let m be object;

        assume m in the carrier' of ( Functors (A,( Functors (B,C))));

        then

        reconsider f = m as Morphism of ( Functors (A,( Functors (B,C))));

        consider F1,F2 be Functor of A, ( Functors (B,C)), t be natural_transformation of F1, F2 such that

         A9: F1 is_naturally_transformable_to F2 and ( dom f) = F1 and ( cod f) = F2 and

         A10: f = [ [F1, F2], t] by Th6;

        consider G1 be Functor of [:A, B:], C such that

         A11: F1 = ( export G1) by Th25;

        consider G2 be Functor of [:A, B:], C such that

         A12: F2 = ( export G2) by Th25;

        consider u be natural_transformation of G1, G2 such that

         A13: t = ( export u) by A9, A11, A12, Th26;

        

         A14: G1 is_naturally_transformable_to G2 by A9, A11, A12, Th26;

        then ( dom ( export (A,B,C))) = the carrier' of ( Functors ( [:A, B:],C)) & [ [G1, G2], u] in ( NatTrans ( [:A, B:],C)) by FUNCT_2:def 1, NATTRA_1: 32;

        then

         A15: [ [G1, G2], u] in ( dom ( export (A,B,C))) by NATTRA_1:def 17;

        (( export (A,B,C)) . [ [G1, G2], u]) = f by A10, A11, A12, A14, A13, Def6;

        hence thesis by A15, FUNCT_1:def 3;

      end;

    end

    theorem :: ISOCAT_2:29

    ( Functors ( [:A, B:],C)) ~= ( Functors (A,( Functors (B,C))))

    proof

      take ( export (A,B,C));

      thus thesis;

    end;

    begin

    theorem :: ISOCAT_2:30

    

     Th28: for F1,F2 be Functor of A, B, G be Functor of B, C st F1 is_naturally_transformable_to F2 holds for t be natural_transformation of F1, F2 holds (G * t) = (G * t qua Function)

    proof

      let F1,F2 be Functor of A, B, G be Functor of B, C;

      assume

       A1: F1 is_naturally_transformable_to F2;

      then

       A2: F1 is_transformable_to F2;

      let t be natural_transformation of F1, F2;

      

      thus (G * t) = (G * t qua transformation of F1, F2) by A1, ISOCAT_1:def 7

      .= (G * t qua Function) by A2, ISOCAT_1:def 5;

    end;

    definition

      let A, B, C;

      let F be Functor of A, B, G be Functor of A, C;

      :: original: <:

      redefine

      func <:F,G:> -> Functor of A, [:B, C:] ;

      coherence

      proof

        thus <:F, G:> is Functor of A, [:B, C:];

      end;

    end

    definition

      let A, B, C;

      let F be Functor of A, [:B, C:];

      :: ISOCAT_2:def7

      func Pr1 F -> Functor of A, B equals (( pr1 (B,C)) * F);

      correctness ;

      :: ISOCAT_2:def8

      func Pr2 F -> Functor of A, C equals (( pr2 (B,C)) * F);

      correctness ;

    end

    theorem :: ISOCAT_2:31

    

     Th29: for F be Functor of A, B, G be Functor of A, C holds ( Pr1 <:F, G:>) = F & ( Pr2 <:F, G:>) = G by FUNCT_3: 62;

    theorem :: ISOCAT_2:32

    

     Th30: for F,G be Functor of A, [:B, C:] st ( Pr1 F) = ( Pr1 G) & ( Pr2 F) = ( Pr2 G) holds F = G by FUNCT_3: 80;

    definition

      let A, B, C;

      let F1,F2 be Functor of A, [:B, C:];

      let t be natural_transformation of F1, F2;

      :: ISOCAT_2:def9

      func Pr1 t -> natural_transformation of ( Pr1 F1), ( Pr1 F2) equals (( pr1 (B,C)) * t);

      coherence ;

      :: ISOCAT_2:def10

      func Pr2 t -> natural_transformation of ( Pr2 F1), ( Pr2 F2) equals (( pr2 (B,C)) * t);

      coherence ;

    end

    theorem :: ISOCAT_2:33

    

     Th31: for F1,F2,G1,G2 be Functor of A, [:B, C:] st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds for s be natural_transformation of F1, F2, t be natural_transformation of G1, G2 st ( Pr1 s) = ( Pr1 t) & ( Pr2 s) = ( Pr2 t) holds s = t

    proof

      let F1,F2,G1,G2 be Functor of A, [:B, C:] such that

       A1: F1 is_naturally_transformable_to F2 and

       A2: G1 is_naturally_transformable_to G2;

      let s be natural_transformation of F1, F2, t be natural_transformation of G1, G2 such that

       A3: ( Pr1 s) = ( Pr1 t) and

       A4: ( Pr2 s) = ( Pr2 t);

      reconsider S = s, T = t as Function of the carrier of A, [:the carrier' of B, the carrier' of C:];

      

       A5: (( pr2 (the carrier' of B,the carrier' of C)) * S) = (( pr2 (B,C)) * S)

      .= ( Pr2 s) by A1, Th28

      .= (( pr2 (B,C)) * T) by A2, A4, Th28

      .= (( pr2 (the carrier' of B,the carrier' of C)) * T);

      (( pr1 (the carrier' of B,the carrier' of C)) * S) = (( pr1 (B,C)) * S)

      .= ( Pr1 s) by A1, Th28

      .= (( pr1 (B,C)) * T) by A2, A3, Th28

      .= (( pr1 (the carrier' of B,the carrier' of C)) * T);

      hence thesis by A5, FUNCT_3: 80;

    end;

    

     Lm2: for F1,G1 be Functor of A, B, F2,G2 be Functor of A, C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds for t1 be transformation of F1, G1, t2 be transformation of F2, G2 holds for a be Object of A holds ( <:t1, t2:> . a) = [(t1 . a), (t2 . a)]

    proof

      let F1,G1 be Functor of A, B, F2,G2 be Functor of A, C such that

       A1: F1 is_transformable_to G1 and

       A2: F2 is_transformable_to G2;

      let t1 be transformation of F1, G1, t2 be transformation of F2, G2;

      let a be Object of A;

      reconsider s1 = t1 as Function of the carrier of A, the carrier' of B;

      reconsider s2 = t2 as Function of the carrier of A, the carrier' of C;

      

      thus ( <:t1, t2:> . a) = [(s1 . a), (s2 . a)] by FUNCT_3: 59

      .= [(t1 . a), (s2 . a)] by A1, NATTRA_1:def 5

      .= [(t1 . a), (t2 . a)] by A2, NATTRA_1:def 5;

    end;

    theorem :: ISOCAT_2:34

    

     Th32: for F be Functor of A, B, G be Functor of A, C holds for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds ( <:F, G:> . f) = [(F . f), (G . f)] by FUNCT_3: 59;

    theorem :: ISOCAT_2:35

    

     Th33: for F be Functor of A, B, G be Functor of A, C holds for a be Object of A holds ( <:F, G:> . a) = [(F . a), (G . a)]

    proof

      let F be Functor of A, B, G be Functor of A, C;

      let a be Object of A;

      ( <:F, G:> . ( id a) qua Morphism of A) = [(F . ( id a) qua Morphism of A), (G . ( id a) qua Morphism of A)] by FUNCT_3: 59

      .= [( id (F . a)), (G . ( id a) qua Morphism of A)] by CAT_1: 71

      .= [( id (F . a)), ( id (G . a))] by CAT_1: 71

      .= ( id [(F . a), (G . a)]) by CAT_2: 31;

      hence thesis by CAT_1: 70;

    end;

    

     Lm3: for F1,G1 be Functor of A, B, F2,G2 be Functor of A, C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds for t1 be transformation of F1, G1, t2 be transformation of F2, G2 holds for a be Object of A holds ( <:t1, t2:> . a) in ( Hom (( <:F1, F2:> . a),( <:G1, G2:> . a)))

    proof

      let F1,G1 be Functor of A, B, F2,G2 be Functor of A, C such that

       A1: F1 is_transformable_to G1 & F2 is_transformable_to G2;

      let t1 be transformation of F1, G1, t2 be transformation of F2, G2;

      let a be Object of A;

      

       A2: (t1 . a) in ( Hom ((F1 . a),(G1 . a))) & (t2 . a) in ( Hom ((F2 . a),(G2 . a))) by A1, ISOCAT_1: 4;

      

       A3: [(F1 . a), (F2 . a)] = ( <:F1, F2:> . a) & [(G1 . a), (G2 . a)] = ( <:G1, G2:> . a) by Th33;

       [(t1 . a), (t2 . a)] = ( <:t1, t2:> . a) by A1, Lm2;

      hence thesis by A2, A3, Th12;

    end;

    theorem :: ISOCAT_2:36

    

     Th34: for F1,G1 be Functor of A, B, F2,G2 be Functor of A, C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds <:F1, F2:> is_transformable_to <:G1, G2:> by Lm3;

    definition

      let A, B, C;

      let F1,G1 be Functor of A, B, F2,G2 be Functor of A, C;

      let t1 be transformation of F1, G1, t2 be transformation of F2, G2;

      :: ISOCAT_2:def11

      func <:t1,t2:> -> transformation of <:F1, F2:>, <:G1, G2:> equals

      : Def11: <:t1, t2:>;

      coherence

      proof

        reconsider t = <:t1, t2:> as Function of the carrier of A, the carrier' of [:B, C:];

        t is transformation of <:F1, F2:>, <:G1, G2:>

        proof

          thus <:F1, F2:> is_transformable_to <:G1, G2:> by A1, Th34;

          let a be Object of A;

          (t . a) in ( Hom (( <:F1, F2:> . a),( <:G1, G2:> . a))) by A1, Lm3;

          hence thesis by CAT_1:def 5;

        end;

        hence thesis;

      end;

    end

    theorem :: ISOCAT_2:37

    

     Th35: for F1,G1 be Functor of A, B, F2,G2 be Functor of A, C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds for t1 be transformation of F1, G1, t2 be transformation of F2, G2 holds for a be Object of A holds ( <:t1, t2:> . a) = [(t1 . a), (t2 . a)]

    proof

      let F1,G1 be Functor of A, B, F2,G2 be Functor of A, C such that

       A1: F1 is_transformable_to G1 & F2 is_transformable_to G2;

      let t1 be transformation of F1, G1, t2 be transformation of F2, G2;

      let a be Object of A;

      reconsider s1 = t1 as Function of the carrier of A, the carrier' of B;

      reconsider s2 = t2 as Function of the carrier of A, the carrier' of C;

      

      thus ( <:t1, t2:> . a) = ( <:t1, t2:> qua Function of the carrier of A, the carrier' of [:B, C:] . a) by A1, Th34, NATTRA_1:def 5

      .= ( <:s1, s2:> . a) by A1, Def11

      .= [(t1 . a), (t2 . a)] by A1, Lm2;

    end;

    

     Lm4: for F1,G1 be Functor of A, B, F2,G2 be Functor of A, C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds for t1 be natural_transformation of F1, G1, t2 be natural_transformation of F2, G2 holds for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds (( <:t1, t2:> . b) * ( <:F1, F2:> /. f)) = (( <:G1, G2:> /. f) * ( <:t1, t2:> . a))

    proof

      let F1,G1 be Functor of A, B, F2,G2 be Functor of A, C such that

       A1: F1 is_naturally_transformable_to G1 and

       A2: F2 is_naturally_transformable_to G2;

      let t1 be natural_transformation of F1, G1, t2 be natural_transformation of F2, G2;

      let a,b be Object of A such that

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

      

       A4: ( Hom ((F1 . a),(F1 . b))) <> {} by A3, CAT_1: 84;

      let f be Morphism of a, b;

      

       A5: ((t1 . b) * (F1 /. f)) = ((G1 /. f) * (t1 . a)) & ((t2 . b) * (F2 /. f)) = ((G2 /. f) * (t2 . a)) by A1, A2, A3, NATTRA_1:def 8;

      

       A6: (G1 /. f) = (G1 . f) & (G2 /. f) = (G2 . f) by A3, CAT_3:def 10;

      

       A7: ( <:G1, G2:> /. f) = ( <:G1, G2:> . f) by A3, CAT_3:def 10

      .= [(G1 /. f), (G2 /. f)] by A6, A3, Th32;

      

       A8: (F1 /. f) = (F1 . f) & (F2 /. f) = (F2 . f) by A3, CAT_3:def 10;

      

       A9: ( <:F1, F2:> /. f) = ( <:F1, F2:> . f) by A3, CAT_3:def 10

      .= [(F1 /. f), (F2 /. f)] by A3, Th32, A8;

      

       A10: F2 is_transformable_to G2 by A2;

      then

       A11: ( Hom ((F2 . b),(G2 . b))) <> {} ;

      

       A12: F1 is_transformable_to G1 by A1;

      then

       A13: ( <:t1, t2:> . b) = [(t1 . b), (t2 . b)] by A10, Th35;

      

       A14: ( <:t1, t2:> . a) = [(t1 . a), (t2 . a)] by A12, A10, Th35;

      

       A15: ( Hom ((G2 . a),(G2 . b))) <> {} by A3, CAT_1: 84;

      

       A16: <:F1, F2:> is_transformable_to <:G1, G2:> by A12, A10, Th34;

      then

       A17: ( Hom (( <:F1, F2:> . a),( <:G1, G2:> . a))) <> {} ;

      

       A18: ( Hom (( <:G1, G2:> . a),( <:G1, G2:> . b))) <> {} by A3, CAT_1: 84;

      

       A19: ( Hom ((G1 . a),(G1 . b))) <> {} by A3, CAT_1: 84;

      

       A20: ( Hom ((F2 . a),(F2 . b))) <> {} by A3, CAT_1: 84;

      then

       A21: ((t2 . b) * (F2 /. f)) = ((t2 . b) (*) (F2 /. f) qua Morphism of C) by A11, CAT_1:def 13;

      

       A22: ( Hom ((F2 . a),(G2 . a))) <> {} by A10;

      then

       A23: ((G2 /. f) * (t2 . a)) = ((G2 /. f) (*) (t2 . a) qua Morphism of C) by A15, CAT_1:def 13;

      

       A24: ( cod (t2 . a)) = (G2 . a) by A22, CAT_1: 5

      .= ( dom (G2 /. f)) by A15, CAT_1: 5;

      

       A25: ( Hom ((F1 . b),(G1 . b))) <> {} by A12;

      

      then

       A26: ( dom (t1 . b)) = (F1 . b) by CAT_1: 5

      .= ( cod (F1 /. f)) by A4, CAT_1: 5;

      

       A27: ( Hom ((F1 . a),(G1 . a))) <> {} by A12;

      then

       A28: ((G1 /. f) * (t1 . a)) = ((G1 /. f) (*) (t1 . a) qua Morphism of B) by A19, CAT_1:def 13;

      

       A29: ( cod (t1 . a)) = (G1 . a) by A27, CAT_1: 5

      .= ( dom (G1 /. f)) by A19, CAT_1: 5;

      

       A30: ( dom (t2 . b)) = (F2 . b) by A11, CAT_1: 5

      .= ( cod (F2 /. f)) by A20, CAT_1: 5;

      

       A31: ((t1 . b) * (F1 /. f)) = ((t1 . b) (*) (F1 /. f) qua Morphism of B) by A25, A4, CAT_1:def 13;

      

       A32: ( Hom (( <:F1, F2:> . b),( <:G1, G2:> . b))) <> {} by A16;

      ( Hom (( <:F1, F2:> . a),( <:F1, F2:> . b))) <> {} by A3, CAT_1: 84;

      

      hence (( <:t1, t2:> . b) * ( <:F1, F2:> /. f)) = (( <:t1, t2:> . b) (*) ( <:F1, F2:> /. f) qua Morphism of [:B, C:]) by A32, CAT_1:def 13

      .= [((G1 /. f) * (t1 . a)), ((G2 /. f) * (t2 . a))] by A5, A13, A9, A26, A30, A31, A21, CAT_2: 29

      .= (( <:G1, G2:> /. f) (*) ( <:t1, t2:> . a) qua Morphism of [:B, C:]) by A28, A23, A29, A24, A7, A14, CAT_2: 29

      .= (( <:G1, G2:> /. f) * ( <:t1, t2:> . a)) by A17, A18, CAT_1:def 13;

    end;

    theorem :: ISOCAT_2:38

    

     Th36: for F1,G1 be Functor of A, B, F2,G2 be Functor of A, C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds <:F1, F2:> is_naturally_transformable_to <:G1, G2:>

    proof

      let F1,G1 be Functor of A, B, F2,G2 be Functor of A, C such that

       A1: F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2;

      F1 is_transformable_to G1 & F2 is_transformable_to G2 by A1;

      hence <:F1, F2:> is_transformable_to <:G1, G2:> by Th34;

      set t1 = the natural_transformation of F1, G1, t2 = the natural_transformation of F2, G2;

      take <:t1, t2:>;

      thus thesis by A1, Lm4;

    end;

    definition

      let A, B, C;

      let F1,G1 be Functor of A, B, F2,G2 be Functor of A, C;

      let t1 be natural_transformation of F1, G1, t2 be natural_transformation of F2, G2;

      :: ISOCAT_2:def12

      func <:t1,t2:> -> natural_transformation of <:F1, F2:>, <:G1, G2:> equals

      : Def12: <:t1, t2:>;

      coherence

      proof

         <:F1, F2:> is_naturally_transformable_to <:G1, G2:> & for a,b be Object of A st ( Hom (a,b)) <> {} holds for f be Morphism of a, b holds (( <:t1, t2:> . b) * ( <:F1, F2:> /. f)) = (( <:G1, G2:> /. f) * ( <:t1, t2:> . a)) by A1, Lm4, Th36;

        hence thesis by NATTRA_1:def 8;

      end;

    end

    theorem :: ISOCAT_2:39

    

     Th37: for F1,G1 be Functor of A, B, F2,G2 be Functor of A, C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds for t1 be natural_transformation of F1, G1, t2 be natural_transformation of F2, G2 holds ( Pr1 <:t1, t2:>) = t1 & ( Pr2 <:t1, t2:>) = t2

    proof

      let F1,G1 be Functor of A, B, F2,G2 be Functor of A, C such that

       A1: F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2;

      

       A2: F1 is_transformable_to G1 & F2 is_transformable_to G2 by A1;

      let t1 be natural_transformation of F1, G1, t2 be natural_transformation of F2, G2;

      reconsider s = t1 as Function of the carrier of A, the carrier' of B;

       <:F1, F2:> is_naturally_transformable_to <:G1, G2:> by A1, Th36;

      then

       A3: <:F1, F2:> is_transformable_to <:G1, G2:>;

      

      thus ( Pr1 <:t1, t2:>) = (( pr1 (B,C)) * <:t1, t2:> qua transformation of <:F1, F2:>, <:G1, G2:>) by A1, Th36, ISOCAT_1:def 7

      .= (( pr1 (B,C)) * <:t1, t2:> qua Function of the carrier of A, the carrier' of [:B, C:]) by A3, ISOCAT_1:def 5

      .= (( pr1 (B,C)) * <:t1 qua transformation of F1, G1, t2:> qua Function of the carrier of A, the carrier' of [:B, C:]) by A1, Def12

      .= (( pr1 (B,C)) * <:s, t2:>) by A2, Def11

      .= (( pr1 (the carrier' of B,the carrier' of C)) * <:s, t2:>)

      .= t1 by FUNCT_3: 62;

      

      thus ( Pr2 <:t1, t2:>) = (( pr2 (B,C)) * <:t1, t2:> qua transformation of <:F1, F2:>, <:G1, G2:>) by A1, Th36, ISOCAT_1:def 7

      .= (( pr2 (B,C)) * <:t1, t2:> qua Function of the carrier of A, the carrier' of [:B, C:]) by A3, ISOCAT_1:def 5

      .= (( pr2 (B,C)) * <:t1 qua transformation of F1, G1, t2:> qua Function of the carrier of A, the carrier' of [:B, C:]) by A1, Def12

      .= (( pr2 (B,C)) * <:s, t2:>) by A2, Def11

      .= (( pr2 (the carrier' of B,the carrier' of C)) * <:s, t2:>)

      .= t2 by FUNCT_3: 62;

    end;

    definition

      let A, B, C;

      :: ISOCAT_2:def13

      func distribute (A,B,C) -> Functor of ( Functors (A, [:B, C:])), [:( Functors (A,B)), ( Functors (A,C)):] means

      : Def13: for F1,F2 be Functor of A, [:B, C:] st F1 is_naturally_transformable_to F2 holds for t be natural_transformation of F1, F2 holds (it . [ [F1, F2], t]) = [ [ [( Pr1 F1), ( Pr1 F2)], ( Pr1 t)], [ [( Pr2 F1), ( Pr2 F2)], ( Pr2 t)]];

      existence

      proof

        defpred P[ set, set] means for F1,F2 be Functor of A, [:B, C:], t be natural_transformation of F1, F2 st $1 = [ [F1, F2], t] holds $2 = [ [ [( Pr1 F1), ( Pr1 F2)], ( Pr1 t)], [ [( Pr2 F1), ( Pr2 F2)], ( Pr2 t)]];

         A1:

        now

          let f be Morphism of ( Functors (A, [:B, C:]));

          consider F1,F2 be Functor of A, [:B, C:], s be natural_transformation of F1, F2 such that

           A2: F1 is_naturally_transformable_to F2 and ( dom f) = F1 and ( cod f) = F2 and

           A3: f = [ [F1, F2], s] by Th6;

          the carrier' of ( Functors (A,C)) = ( NatTrans (A,C)) & ( Pr2 F1) is_naturally_transformable_to ( Pr2 F2) by A2, ISOCAT_1: 22, NATTRA_1:def 17;

          then

          reconsider PPr2 = [ [( Pr2 F1), ( Pr2 F2)], ( Pr2 s)] as Morphism of ( Functors (A,C)) by NATTRA_1: 32;

          the carrier' of ( Functors (A,B)) = ( NatTrans (A,B)) & ( Pr1 F1) is_naturally_transformable_to ( Pr1 F2) by A2, ISOCAT_1: 22, NATTRA_1:def 17;

          then

          reconsider PPr1 = [ [( Pr1 F1), ( Pr1 F2)], ( Pr1 s)] as Morphism of ( Functors (A,B)) by NATTRA_1: 32;

          take g = [PPr1, PPr2];

          thus P[f, g]

          proof

            let G1,G2 be Functor of A, [:B, C:], t be natural_transformation of G1, G2;

            assume

             A4: f = [ [G1, G2], t];

            then [G1, G2] = [F1, F2] by A3, XTUPLE_0: 1;

            then

             A5: G1 = F1 & G2 = F2 by XTUPLE_0: 1;

            t = s by A3, A4, XTUPLE_0: 1;

            hence thesis by A5;

          end;

        end;

        consider IT be Function of the carrier' of ( Functors (A, [:B, C:])), the carrier' of [:( Functors (A,B)), ( Functors (A,C)):] such that

         A6: for f be Morphism of ( Functors (A, [:B, C:])) holds P[f, (IT . f)] from FUNCT_2:sch 3( A1);

        IT is Functor of ( Functors (A, [:B, C:])), [:( Functors (A,B)), ( Functors (A,C)):]

        proof

          thus for c be Object of ( Functors (A, [:B, C:])) holds ex d be Object of [:( Functors (A,B)), ( Functors (A,C)):] st (IT . ( id c)) = ( id d)

          proof

            let c be Object of ( Functors (A, [:B, C:]));

            reconsider F = c as Functor of A, [:B, C:] by Th5;

            reconsider d2 = ( Pr2 F) as Object of ( Functors (A,C)) by Th5;

            reconsider d1 = ( Pr1 F) as Object of ( Functors (A,B)) by Th5;

            take [d1, d2];

            ( Pr1 ( id F)) = ( id ( Pr1 F)) by ISOCAT_1: 33;

            then

             A7: ( id d1) = [ [( Pr1 F), ( Pr1 F)], ( Pr1 ( id F))] by NATTRA_1:def 17;

            ( Pr2 ( id F)) = ( id ( Pr2 F)) by ISOCAT_1: 33;

            then

             A8: ( id d2) = [ [( Pr2 F), ( Pr2 F)], ( Pr2 ( id F))] by NATTRA_1:def 17;

            ( id c) = [ [F, F], ( id F)] by NATTRA_1:def 17;

            

            hence (IT . ( id c)) = [( id d1), ( id d2)] by A6, A7, A8

            .= ( id [d1, d2]) by CAT_2: 31;

          end;

          

           A9: the carrier' of ( Functors (A,C)) = ( NatTrans (A,C)) by NATTRA_1:def 17;

          

           A10: the carrier' of ( Functors (A,B)) = ( NatTrans (A,B)) by NATTRA_1:def 17;

          thus for f be Morphism of ( Functors (A, [:B, C:])) holds (IT . ( id ( dom f))) = ( id ( dom (IT . f))) & (IT . ( id ( cod f))) = ( id ( cod (IT . f)))

          proof

            let f be Morphism of ( Functors (A, [:B, C:]));

            consider F1,F2 be Functor of A, [:B, C:], s be natural_transformation of F1, F2 such that

             A11: F1 is_naturally_transformable_to F2 and

             A12: ( dom f) = F1 and

             A13: ( cod f) = F2 and

             A14: f = [ [F1, F2], s] by Th6;

            ( Pr1 F1) is_naturally_transformable_to ( Pr1 F2) by A11, ISOCAT_1: 22;

            then

            reconsider f1 = [ [( Pr1 F1), ( Pr1 F2)], ( Pr1 s)] as Morphism of ( Functors (A,B)) by A10, NATTRA_1: 32;

            ( dom f1) = ( Pr1 F1) & ( Pr1 ( id F1)) = ( id ( Pr1 F1)) by ISOCAT_1: 33, NATTRA_1: 33;

            then

             A15: ( id ( dom f1)) = [ [( Pr1 F1), ( Pr1 F1)], ( Pr1 ( id F1))] by NATTRA_1:def 17;

            ( Pr2 F1) is_naturally_transformable_to ( Pr2 F2) by A11, ISOCAT_1: 22;

            then

            reconsider f2 = [ [( Pr2 F1), ( Pr2 F2)], ( Pr2 s)] as Morphism of ( Functors (A,C)) by A9, NATTRA_1: 32;

            ( dom f2) = ( Pr2 F1) & ( Pr2 ( id F1)) = ( id ( Pr2 F1)) by ISOCAT_1: 33, NATTRA_1: 33;

            then

             A16: ( id ( dom f2)) = [ [( Pr2 F1), ( Pr2 F1)], ( Pr2 ( id F1))] by NATTRA_1:def 17;

            ( id ( dom f)) = [ [F1, F1], ( id F1)] by A12, NATTRA_1:def 17;

            

            hence (IT . ( id ( dom f))) = [( id ( dom f1)), ( id ( dom f2))] by A6, A15, A16

            .= ( id [( dom f1), ( dom f2)]) by CAT_2: 31

            .= ( id ( dom [f1, f2])) by CAT_2: 28

            .= ( id ( dom (IT . f))) by A6, A14;

            ( cod f1) = ( Pr1 F2) & ( Pr1 ( id F2)) = ( id ( Pr1 F2)) by ISOCAT_1: 33, NATTRA_1: 33;

            then

             A17: ( id ( cod f1)) = [ [( Pr1 F2), ( Pr1 F2)], ( Pr1 ( id F2))] by NATTRA_1:def 17;

            ( cod f2) = ( Pr2 F2) & ( Pr2 ( id F2)) = ( id ( Pr2 F2)) by ISOCAT_1: 33, NATTRA_1: 33;

            then

             A18: ( id ( cod f2)) = [ [( Pr2 F2), ( Pr2 F2)], ( Pr2 ( id F2))] by NATTRA_1:def 17;

            ( id ( cod f)) = [ [F2, F2], ( id F2)] by A13, NATTRA_1:def 17;

            

            hence (IT . ( id ( cod f))) = [( id ( cod f1)), ( id ( cod f2))] by A6, A17, A18

            .= ( id [( cod f1), ( cod f2)]) by CAT_2: 31

            .= ( id ( cod [f1, f2])) by CAT_2: 28

            .= ( id ( cod (IT . f))) by A6, A14;

          end;

          let f,g be Morphism of ( Functors (A, [:B, C:])) such that

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

          consider F1,F2 be Functor of A, [:B, C:], s be natural_transformation of F1, F2 such that

           A20: F1 is_naturally_transformable_to F2 and ( dom f) = F1 and

           A21: ( cod f) = F2 and

           A22: f = [ [F1, F2], s] by Th6;

          consider G1,G2 be Functor of A, [:B, C:], t be natural_transformation of G1, G2 such that

           A23: G1 is_naturally_transformable_to G2 and

           A24: ( dom g) = G1 and ( cod g) = G2 and

           A25: g = [ [G1, G2], t] by Th6;

          reconsider t as natural_transformation of F2, G2 by A19, A21, A24;

          

           A26: (g (*) f) = [ [F1, G2], (t `*` s)] by A19, A21, A22, A24, A25, NATTRA_1: 36;

          

           A27: ( Pr2 F1) is_naturally_transformable_to ( Pr2 F2) by A20, ISOCAT_1: 22;

          ( Pr2 F2) is_naturally_transformable_to ( Pr2 G2) by A19, A21, A23, A24, ISOCAT_1: 22;

          then

          reconsider g2 = [ [( Pr2 F2), ( Pr2 G2)], ( Pr2 t)], f2 = [ [( Pr2 F1), ( Pr2 F2)], ( Pr2 s)] as Morphism of ( Functors (A,C)) by A9, A27, NATTRA_1: 32;

          

           A28: (g2 (*) f2) = [ [( Pr2 F1), ( Pr2 G2)], (( Pr2 t) `*` ( Pr2 s))] by NATTRA_1: 36

          .= [ [( Pr2 F1), ( Pr2 G2)], ( Pr2 (t `*` s))] by A19, A20, A21, A23, A24, ISOCAT_1: 27;

          

           A29: ( dom g2) = ( Pr2 F2) by NATTRA_1: 33

          .= ( cod f2) by NATTRA_1: 33;

          

           A30: ( Pr1 F1) is_naturally_transformable_to ( Pr1 F2) by A20, ISOCAT_1: 22;

          ( Pr1 F2) is_naturally_transformable_to ( Pr1 G2) by A19, A21, A23, A24, ISOCAT_1: 22;

          then

          reconsider g1 = [ [( Pr1 F2), ( Pr1 G2)], ( Pr1 t)], f1 = [ [( Pr1 F1), ( Pr1 F2)], ( Pr1 s)] as Morphism of ( Functors (A,B)) by A10, A30, NATTRA_1: 32;

          

           A31: ( dom g1) = ( Pr1 F2) by NATTRA_1: 33

          .= ( cod f1) by NATTRA_1: 33;

          

           A32: (IT . f) = [ [ [( Pr1 F1), ( Pr1 F2)], ( Pr1 s)], [ [( Pr2 F1), ( Pr2 F2)], ( Pr2 s)]] by A6, A22;

          (g1 (*) f1) = [ [( Pr1 F1), ( Pr1 G2)], (( Pr1 t) `*` ( Pr1 s))] by NATTRA_1: 36

          .= [ [( Pr1 F1), ( Pr1 G2)], ( Pr1 (t `*` s))] by A19, A20, A21, A23, A24, ISOCAT_1: 27;

          

          hence (IT . (g (*) f)) = [(g1 (*) f1), (g2 (*) f2)] by A6, A28, A26

          .= ( [g1, g2] (*) [f1, f2]) by A31, A29, CAT_2: 29

          .= ((IT . g) (*) (IT . f)) by A6, A19, A21, A24, A25, A32;

        end;

        then

        reconsider IT as Functor of ( Functors (A, [:B, C:])), [:( Functors (A,B)), ( Functors (A,C)):];

        take IT;

        let F1,F2 be Functor of A, [:B, C:] such that

         A33: F1 is_naturally_transformable_to F2;

        let t be natural_transformation of F1, F2;

        set f = [ [F1, F2], t];

        f in ( NatTrans (A, [:B, C:])) by A33, NATTRA_1: 32;

        then

        reconsider f as Morphism of ( Functors (A, [:B, C:])) by NATTRA_1:def 17;

        

        thus (IT . [ [F1, F2], t]) = (IT . f)

        .= [ [ [( Pr1 F1), ( Pr1 F2)], ( Pr1 t)], [ [( Pr2 F1), ( Pr2 F2)], ( Pr2 t)]] by A6;

      end;

      uniqueness

      proof

        let IT1,IT2 be Functor of ( Functors (A, [:B, C:])), [:( Functors (A,B)), ( Functors (A,C)):] such that

         A34: for F1,F2 be Functor of A, [:B, C:] st F1 is_naturally_transformable_to F2 holds for t be natural_transformation of F1, F2 holds (IT1 . [ [F1, F2], t]) = [ [ [( Pr1 F1), ( Pr1 F2)], ( Pr1 t)], [ [( Pr2 F1), ( Pr2 F2)], ( Pr2 t)]] and

         A35: for F1,F2 be Functor of A, [:B, C:] st F1 is_naturally_transformable_to F2 holds for t be natural_transformation of F1, F2 holds (IT2 . [ [F1, F2], t]) = [ [ [( Pr1 F1), ( Pr1 F2)], ( Pr1 t)], [ [( Pr2 F1), ( Pr2 F2)], ( Pr2 t)]];

        now

          let f be Morphism of ( Functors (A, [:B, C:]));

          consider F1,F2 be Functor of A, [:B, C:], s be natural_transformation of F1, F2 such that

           A36: F1 is_naturally_transformable_to F2 and ( dom f) = F1 and ( cod f) = F2 and

           A37: f = [ [F1, F2], s] by Th6;

          

          thus (IT1 . f) = [ [ [( Pr1 F1), ( Pr1 F2)], ( Pr1 s)], [ [( Pr2 F1), ( Pr2 F2)], ( Pr2 s)]] by A34, A36, A37

          .= (IT2 . f) by A35, A36, A37;

        end;

        hence IT1 = IT2 by FUNCT_2: 63;

      end;

    end

    registration

      let A, B, C;

      cluster ( distribute (A,B,C)) -> isomorphic;

      coherence

      proof

        thus ( distribute (A,B,C)) is one-to-one

        proof

          let x1,x2 be object;

          assume x1 in ( dom ( distribute (A,B,C)));

          then

          reconsider f1 = x1 as Morphism of ( Functors (A, [:B, C:]));

          consider F1,F2 be Functor of A, [:B, C:], s be natural_transformation of F1, F2 such that

           A1: F1 is_naturally_transformable_to F2 and ( dom f1) = F1 and ( cod f1) = F2 and

           A2: f1 = [ [F1, F2], s] by Th6;

          assume x2 in ( dom ( distribute (A,B,C)));

          then

          reconsider f2 = x2 as Morphism of ( Functors (A, [:B, C:]));

          consider G1,G2 be Functor of A, [:B, C:], t be natural_transformation of G1, G2 such that

           A3: G1 is_naturally_transformable_to G2 and ( dom f2) = G1 and ( cod f2) = G2 and

           A4: f2 = [ [G1, G2], t] by Th6;

          assume (( distribute (A,B,C)) . x1) = (( distribute (A,B,C)) . x2);

          

          then

           A5: [ [ [( Pr1 F1), ( Pr1 F2)], ( Pr1 s)], [ [( Pr2 F1), ( Pr2 F2)], ( Pr2 s)]] = (( distribute (A,B,C)) . [ [G1, G2], t]) by A1, A2, A4, Def13

          .= [ [ [( Pr1 G1), ( Pr1 G2)], ( Pr1 t)], [ [( Pr2 G1), ( Pr2 G2)], ( Pr2 t)]] by A3, Def13;

          then

           A6: [ [( Pr1 F1), ( Pr1 F2)], ( Pr1 s)] = [ [( Pr1 G1), ( Pr1 G2)], ( Pr1 t)] by XTUPLE_0: 1;

          

           A7: [ [( Pr2 F1), ( Pr2 F2)], ( Pr2 s)] = [ [( Pr2 G1), ( Pr2 G2)], ( Pr2 t)] by A5, XTUPLE_0: 1;

          then

           A8: ( Pr2 s) = ( Pr2 t) by XTUPLE_0: 1;

          

           A9: [( Pr2 F1), ( Pr2 F2)] = [( Pr2 G1), ( Pr2 G2)] by A7, XTUPLE_0: 1;

          then

           A10: ( Pr2 F1) = ( Pr2 G1) by XTUPLE_0: 1;

          

           A11: [( Pr1 F1), ( Pr1 F2)] = [( Pr1 G1), ( Pr1 G2)] by A6, XTUPLE_0: 1;

          then ( Pr1 F1) = ( Pr1 G1) by XTUPLE_0: 1;

          then

           A12: F1 = G1 by A10, Th30;

          ( Pr1 s) = ( Pr1 t) by A6, XTUPLE_0: 1;

          then

           A13: s = t by A1, A3, A8, Th31;

          

           A14: ( Pr2 F2) = ( Pr2 G2) by A9, XTUPLE_0: 1;

          ( Pr1 F2) = ( Pr1 G2) by A11, XTUPLE_0: 1;

          hence thesis by A2, A4, A14, A13, A12, Th30;

        end;

        thus ( rng ( distribute (A,B,C))) c= the carrier' of [:( Functors (A,B)), ( Functors (A,C)):];

        let o be object;

        assume o in the carrier' of [:( Functors (A,B)), ( Functors (A,C)):];

        then

        consider o1 be Morphism of ( Functors (A,B)), o2 be Morphism of ( Functors (A,C)) such that

         A15: o = [o1, o2] by CAT_2: 27;

        consider G1,G2 be Functor of A, C, t be natural_transformation of G1, G2 such that

         A16: G1 is_naturally_transformable_to G2 and ( dom o2) = G1 and ( cod o2) = G2 and

         A17: o2 = [ [G1, G2], t] by Th6;

        consider F1,F2 be Functor of A, B, s be natural_transformation of F1, F2 such that

         A18: F1 is_naturally_transformable_to F2 and ( dom o1) = F1 and ( cod o1) = F2 and

         A19: o1 = [ [F1, F2], s] by Th6;

        set f = [ [ <:F1, G1:>, <:F2, G2:>], <:s, t:>];

        

         A20: <:F1, G1:> is_naturally_transformable_to <:F2, G2:> by A18, A16, Th36;

        then f in ( NatTrans (A, [:B, C:])) by NATTRA_1: 32;

        then

        reconsider f as Morphism of ( Functors (A, [:B, C:])) by NATTRA_1:def 17;

        

         A21: ( Pr1 <:F1, G1:>) = F1 & ( Pr1 <:F2, G2:>) = F2 by Th29;

        

         A22: ( Pr2 <:F1, G1:>) = G1 & ( Pr2 <:F2, G2:>) = G2 by Th29;

        ( Pr1 <:s, t:>) = s & ( Pr2 <:s, t:>) = t by A18, A16, Th37;

        then (( distribute (A,B,C)) . f) = o by A15, A19, A17, A20, A21, A22, Def13;

        hence thesis by FUNCT_2: 112;

      end;

    end

    theorem :: ISOCAT_2:40

    ( Functors (A, [:B, C:])) ~= [:( Functors (A,B)), ( Functors (A,C)):]

    proof

      take ( distribute (A,B,C));

      thus thesis;

    end;