functor2.miz



    begin

    registration

      let A be transitive with_units non empty AltCatStr, B be with_units non empty AltCatStr;

      cluster -> feasible id-preserving for Functor of A, B;

      coherence by FUNCTOR0:def 25;

    end

    registration

      let A be transitive with_units non empty AltCatStr, B be with_units non empty AltCatStr;

      cluster covariant -> Covariant comp-preserving for Functor of A, B;

      coherence by FUNCTOR0:def 26;

      cluster Covariant comp-preserving -> covariant for Functor of A, B;

      coherence by FUNCTOR0:def 26;

      cluster contravariant -> Contravariant comp-reversing for Functor of A, B;

      coherence by FUNCTOR0:def 27;

      cluster Contravariant comp-reversing -> contravariant for Functor of A, B;

      coherence by FUNCTOR0:def 27;

    end

    theorem :: FUNCTOR2:1

    

     Th1: for A,B be transitive with_units non empty AltCatStr, F be covariant Functor of A, B holds for a be Object of A holds (F . ( idm a)) = ( idm (F . a))

    proof

      let A,B be transitive with_units non empty AltCatStr, F be covariant Functor of A, B;

      let a be Object of A;

       <^a, a^> <> {} & <^(F . a), (F . a)^> <> {} by ALTCAT_2:def 7;

      

      hence (F . ( idm a)) = (( Morph-Map (F,a,a)) . ( idm a)) by FUNCTOR0:def 15

      .= ( idm (F . a)) by FUNCTOR0:def 20;

    end;

    begin

    definition

      let A,B be transitive with_units non empty AltCatStr, F1,F2 be Functor of A, B;

      :: FUNCTOR2:def1

      pred F1 is_transformable_to F2 means for a be Object of A holds <^(F1 . a), (F2 . a)^> <> {} ;

      reflexivity by ALTCAT_2:def 7;

    end

    theorem :: FUNCTOR2:2

    

     Th2: for A,B be transitive with_units non empty AltCatStr, F,F1,F2 be Functor of A, B holds F is_transformable_to F1 & F1 is_transformable_to F2 implies F is_transformable_to F2

    proof

      let A,B be transitive with_units non empty AltCatStr, F,F1,F2 be Functor of A, B;

      assume

       A1: F is_transformable_to F1 & F1 is_transformable_to F2;

      let a be Object of A;

       <^(F . a), (F1 . a)^> <> {} & <^(F1 . a), (F2 . a)^> <> {} by A1;

      hence thesis by ALTCAT_1:def 2;

    end;

    definition

      let A,B be transitive with_units non empty AltCatStr, F1,F2 be Functor of A, B;

      assume

       A1: F1 is_transformable_to F2;

      :: FUNCTOR2:def2

      mode transformation of F1,F2 -> ManySortedSet of the carrier of A means

      : Def2: for a be Object of A holds (it . a) is Morphism of (F1 . a), (F2 . a);

      existence

      proof

        defpred P[ Object of A, object] means $2 in <^(F1 . $1), (F2 . $1)^>;

        

         A2: for a be Element of A holds ex j be object st P[a, j]

        proof

          let a be Element of A;

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

          then ex j be object st j in <^(F1 . a), (F2 . a)^> by XBOOLE_0:def 1;

          hence thesis;

        end;

        consider t be ManySortedSet of the carrier of A such that

         A3: for a be Element of A holds P[a, (t . a)] from PBOOLE:sch 6( A2);

        take t;

        thus thesis by A3;

      end;

    end

    definition

      let A,B be transitive with_units non empty AltCatStr;

      let F be Functor of A, B;

      :: FUNCTOR2:def3

      func idt F -> transformation of F, F means

      : Def3: for a be Object of A holds (it . a) = ( idm (F . a));

      existence

      proof

        defpred P[ Object of A, object] means $2 = ( idm (F . $1));

        

         A1: for a be Element of A holds ex j be object st P[a, j];

        consider t be ManySortedSet of the carrier of A such that

         A2: for a be Element of A holds P[a, (t . a)] from PBOOLE:sch 6( A1);

        for a be Object of A holds (t . a) is Morphism of (F . a), (F . a)

        proof

          let a be Element of A;

           P[a, (t . a)] by A2;

          hence thesis;

        end;

        then t is transformation of F, F by Def2;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let it1,it2 be transformation of F, F such that

         A3: for a be Object of A holds (it1 . a) = ( idm (F . a)) and

         A4: for a be Object of A holds (it2 . a) = ( idm (F . a));

        now

          let a be object;

          assume a in the carrier of A;

          then

          reconsider o = a as Object of A;

          

          thus (it1 . a) = ( idm (F . o)) by A3

          .= (it2 . a) by A4;

        end;

        hence it1 = it2 by PBOOLE: 3;

      end;

    end

    definition

      let A,B be transitive with_units non empty AltCatStr, F1,F2 be Functor of A, B;

      assume

       A1: F1 is_transformable_to F2;

      let t be transformation of F1, F2;

      let a be Object of A;

      :: FUNCTOR2:def4

      func t ! a -> Morphism of (F1 . a), (F2 . a) means

      : Def4: it = (t . a);

      existence

      proof

        (t . a) is Morphism of (F1 . a), (F2 . a) by A1, Def2;

        hence thesis;

      end;

      correctness ;

    end

    definition

      let A,B be transitive with_units non empty AltCatStr, F,F1,F2 be Functor of A, B;

      assume

       A1: F is_transformable_to F1 & F1 is_transformable_to F2;

      let t1 be transformation of F, F1;

      let t2 be transformation of F1, F2;

      :: FUNCTOR2:def5

      func t2 `*` t1 -> transformation of F, F2 means

      : Def5: for a be Object of A holds (it ! a) = ((t2 ! a) * (t1 ! a));

      existence

      proof

        defpred P[ Object of A, object] means $2 = ((t2 ! $1) * (t1 ! $1));

        

         A2: for a be Element of A holds ex j be object st P[a, j];

        consider t be ManySortedSet of the carrier of A such that

         A3: for a be Element of A holds P[a, (t . a)] from PBOOLE:sch 6( A2);

        

         A4: F is_transformable_to F2 by A1, Th2;

        for a be Object of A holds (t . a) is Morphism of (F . a), (F2 . a)

        proof

          let o be Element of A;

           P[o, (t . o)] by A3;

          hence thesis;

        end;

        then

        reconsider t9 = t as transformation of F, F2 by A4, Def2;

        take t9;

        let a be Element of A;

         P[a, (t . a)] by A3;

        hence thesis by A4, Def4;

      end;

      uniqueness

      proof

        let it1,it2 be transformation of F, F2 such that

         A5: for a be Object of A holds (it1 ! a) = ((t2 ! a) * (t1 ! a)) and

         A6: for a be Object of A holds (it2 ! a) = ((t2 ! a) * (t1 ! a));

        

         A7: F is_transformable_to F2 by A1, Th2;

        now

          let a be object;

          assume a in the carrier of A;

          then

          reconsider o = a as Object of A;

          

          thus (it1 qua ManySortedSet of the carrier of A . a) = (it1 ! o) by A7, Def4

          .= ((t2 ! o) * (t1 ! o)) by A5

          .= (it2 ! o) by A6

          .= (it2 qua ManySortedSet of the carrier of A . a) by A7, Def4;

        end;

        hence it1 = it2 by PBOOLE: 3;

      end;

    end

    theorem :: FUNCTOR2:3

    

     Th3: for A,B be transitive with_units non empty AltCatStr, F1,F2 be Functor of A, B holds F1 is_transformable_to F2 implies for t1,t2 be transformation of F1, F2 st for a be Object of A holds (t1 ! a) = (t2 ! a) holds t1 = t2

    proof

      let A,B be transitive with_units non empty AltCatStr, F1,F2 be Functor of A, B;

      assume

       A1: F1 is_transformable_to F2;

      let t1,t2 be transformation of F1, F2;

      assume

       A2: for a be Object of A holds (t1 ! a) = (t2 ! a);

      now

        let a be object;

        assume a in the carrier of A;

        then

        reconsider o = a as Object of A;

        

        thus (t1 qua ManySortedSet of the carrier of A . a) = (t1 ! o) by A1, Def4

        .= (t2 ! o) by A2

        .= (t2 qua ManySortedSet of the carrier of A . a) by A1, Def4;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: FUNCTOR2:4

    

     Th4: for A,B be transitive with_units non empty AltCatStr, F be Functor of A, B holds for a be Object of A holds (( idt F) ! a) = ( idm (F . a))

    proof

      let A,B be transitive with_units non empty AltCatStr, F be Functor of A, B;

      let a be Object of A;

      

      thus (( idt F) ! a) = (( idt F) qua ManySortedSet of the carrier of A . a) by Def4

      .= ( idm (F . a)) by Def3;

    end;

    theorem :: FUNCTOR2:5

    

     Th5: for A,B be transitive with_units non empty AltCatStr, F1,F2 be Functor of A, B holds F1 is_transformable_to F2 implies for t be transformation of F1, F2 holds (( idt F2) `*` t) = t & (t `*` ( idt F1)) = t

    proof

      let A,B be transitive with_units non empty AltCatStr, F1,F2 be Functor of A, B;

      assume

       A1: F1 is_transformable_to F2;

      let t be transformation of F1, F2;

      now

        let a be Object of A;

        

         A2: <^(F1 . a), (F2 . a)^> <> {} by A1;

        

        thus ((( idt F2) `*` t) ! a) = ((( idt F2) ! a) * (t ! a)) by A1, Def5

        .= (( idm (F2 . a)) * (t ! a)) by Th4

        .= (t ! a) by A2, ALTCAT_1: 20;

      end;

      hence (( idt F2) `*` t) = t by A1, Th3;

      now

        let a be Object of A;

        

         A3: <^(F1 . a), (F2 . a)^> <> {} by A1;

        

        thus ((t `*` ( idt F1)) ! a) = ((t ! a) * (( idt F1) ! a)) by A1, Def5

        .= ((t ! a) * ( idm (F1 . a))) by Th4

        .= (t ! a) by A3, ALTCAT_1:def 17;

      end;

      hence thesis by A1, Th3;

    end;

    theorem :: FUNCTOR2:6

    

     Th6: for A,B be category, F,F1,F2,F3 be Functor of A, B holds F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 implies for t1 be transformation of F, F1, t2 be transformation of F1, F2, t3 be transformation of F2, F3 holds ((t3 `*` t2) `*` t1) = (t3 `*` (t2 `*` t1))

    proof

      let A,B be category, F,F1,F2,F3 be Functor of A, B;

      assume that

       A1: F is_transformable_to F1 and

       A2: F1 is_transformable_to F2 and

       A3: F2 is_transformable_to F3;

      let t1 be transformation of F, F1, t2 be transformation of F1, F2, t3 be transformation of F2, F3;

      

       A4: F1 is_transformable_to F3 by A2, A3, Th2;

      

       A5: F is_transformable_to F2 by A1, A2, Th2;

      now

        let a be Object of A;

        

         A6: <^(F2 . a), (F3 . a)^> <> {} by A3;

        

         A7: <^(F . a), (F1 . a)^> <> {} & <^(F1 . a), (F2 . a)^> <> {} by A1, A2;

        

        thus (((t3 `*` t2) `*` t1) ! a) = (((t3 `*` t2) ! a) * (t1 ! a)) by A1, A4, Def5

        .= (((t3 ! a) * (t2 ! a)) * (t1 ! a)) by A2, A3, Def5

        .= ((t3 ! a) * ((t2 ! a) * (t1 ! a))) by A7, A6, ALTCAT_1: 21

        .= ((t3 ! a) * ((t2 `*` t1) ! a)) by A1, A2, Def5

        .= ((t3 `*` (t2 `*` t1)) ! a) by A3, A5, Def5;

      end;

      hence thesis by A1, A4, Th2, Th3;

    end;

    begin

    

     Lm1: for A,B be transitive with_units non empty AltCatStr, F,G be covariant Functor of A, B holds for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds ((( idt F) ! b) * (F . f)) = ((F . f) * (( idt F) ! a))

    proof

      let A,B be transitive with_units non empty AltCatStr, F,G be covariant Functor of A, B;

      let a,b be Object of A such that

       A1: <^a, b^> <> {} ;

      let f be Morphism of a, b;

      

       A2: <^a, a^> <> {} by ALTCAT_2:def 7;

      

       A3: <^b, b^> <> {} by ALTCAT_2:def 7;

      

      thus ((( idt F) ! b) * (F . f)) = (( idm (F . b)) * (F . f)) by Th4

      .= ((F . ( idm b)) * (F . f)) by Th1

      .= (F . (( idm b) * f)) by A1, A3, FUNCTOR0:def 23

      .= (F . f) by A1, ALTCAT_1: 20

      .= (F . (f * ( idm a))) by A1, ALTCAT_1:def 17

      .= ((F . f) * (F . ( idm a))) by A1, A2, FUNCTOR0:def 23

      .= ((F . f) * ( idm (F . a))) by Th1

      .= ((F . f) * (( idt F) ! a)) by Th4;

    end;

    definition

      let A,B be transitive with_units non empty AltCatStr, F1,F2 be covariant Functor of A, B;

      :: FUNCTOR2:def6

      pred F1 is_naturally_transformable_to F2 means F1 is_transformable_to F2 & ex t be transformation of F1, F2 st for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds ((t ! b) * (F1 . f)) = ((F2 . f) * (t ! a));

      reflexivity

      proof

        let F be covariant Functor of A, B;

        thus F is_transformable_to F;

        take ( idt F);

        thus thesis by Lm1;

      end;

    end

    theorem :: FUNCTOR2:7

    for A,B be transitive with_units non empty AltCatStr, F be covariant Functor of A, B holds F is_naturally_transformable_to F;

    

     Lm2: for A,B be category, F,F1,F2 be covariant Functor of A, B holds F is_transformable_to F1 & F1 is_transformable_to F2 implies for t1 be transformation of F, F1 st for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds ((t1 ! b) * (F . f)) = ((F1 . f) * (t1 ! a)) holds for t2 be transformation of F1, F2 st for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds ((t2 ! b) * (F1 . f)) = ((F2 . f) * (t2 ! a)) holds for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds (((t2 `*` t1) ! b) * (F . f)) = ((F2 . f) * ((t2 `*` t1) ! a))

    proof

      let A,B be category, F,F1,F2 be covariant Functor of A, B;

      assume that

       A1: F is_transformable_to F1 and

       A2: F1 is_transformable_to F2;

      let t1 be transformation of F, F1 such that

       A3: for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds ((t1 ! b) * (F . f)) = ((F1 . f) * (t1 ! a));

      let t2 be transformation of F1, F2 such that

       A4: for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds ((t2 ! b) * (F1 . f)) = ((F2 . f) * (t2 ! a));

      let a,b be Object of A;

      

       A5: <^(F . b), (F1 . b)^> <> {} by A1;

      

       A6: <^(F . a), (F1 . a)^> <> {} by A1;

      

       A7: <^(F1 . b), (F2 . b)^> <> {} by A2;

      

       A8: <^(F1 . a), (F2 . a)^> <> {} by A2;

      assume

       A9: <^a, b^> <> {} ;

      then

       A10: <^(F . a), (F . b)^> <> {} by FUNCTOR0:def 18;

      let f be Morphism of a, b;

      

       A11: <^(F2 . a), (F2 . b)^> <> {} by A9, FUNCTOR0:def 18;

      

       A12: <^(F1 . a), (F1 . b)^> <> {} by A9, FUNCTOR0:def 18;

      

      thus (((t2 `*` t1) ! b) * (F . f)) = (((t2 ! b) * (t1 ! b)) * (F . f)) by A1, A2, Def5

      .= ((t2 ! b) * ((t1 ! b) * (F . f))) by A10, A5, A7, ALTCAT_1: 21

      .= ((t2 ! b) * ((F1 . f) * (t1 ! a))) by A3, A9

      .= (((t2 ! b) * (F1 . f)) * (t1 ! a)) by A6, A7, A12, ALTCAT_1: 21

      .= (((F2 . f) * (t2 ! a)) * (t1 ! a)) by A4, A9

      .= ((F2 . f) * ((t2 ! a) * (t1 ! a))) by A6, A8, A11, ALTCAT_1: 21

      .= ((F2 . f) * ((t2 `*` t1) ! a)) by A1, A2, Def5;

    end;

    theorem :: FUNCTOR2:8

    

     Th8: for A,B be category, F,F1,F2 be covariant Functor of A, B holds F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies F is_naturally_transformable_to F2

    proof

      let A,B be category, F,F1,F2 be covariant Functor of A, B;

      assume

       A1: F is_transformable_to F1;

      given t1 be transformation of F, F1 such that

       A2: for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds ((t1 ! b) * (F . f)) = ((F1 . f) * (t1 ! a));

      assume

       A3: F1 is_transformable_to F2;

      given t2 be transformation of F1, F2 such that

       A4: for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds ((t2 ! b) * (F1 . f)) = ((F2 . f) * (t2 ! a));

      thus F is_transformable_to F2 by A1, A3, Th2;

      take (t2 `*` t1);

      thus thesis by A1, A2, A3, A4, Lm2;

    end;

    definition

      let A,B be transitive with_units non empty AltCatStr, F1,F2 be covariant Functor of A, B;

      assume

       A1: F1 is_naturally_transformable_to F2;

      :: FUNCTOR2:def7

      mode natural_transformation of F1,F2 -> transformation of F1, F2 means

      : Def7: for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds ((it ! b) * (F1 . f)) = ((F2 . f) * (it ! a));

      existence by A1;

    end

    definition

      let A,B be transitive with_units non empty AltCatStr, F be covariant Functor of A, B;

      :: original: idt

      redefine

      func idt F -> natural_transformation of F, F ;

      coherence

      proof

        F is_naturally_transformable_to F & for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds ((( idt F) ! b) * (F . f)) = ((F . f) * (( idt F) ! a)) by Lm1;

        hence thesis by Def7;

      end;

    end

    definition

      let A,B be category, F,F1,F2 be covariant Functor of A, B;

      let t1 be natural_transformation of F, F1;

      let t2 be natural_transformation of F1, F2;

      :: FUNCTOR2:def8

      func t2 `*` t1 -> natural_transformation of F, F2 means

      : Def8: it = (t2 `*` t1);

      existence

      proof

        

         A2: F is_naturally_transformable_to F2 by A1, Th8;

        

         A3: (for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds ((t1 ! b) * (F . f)) = ((F1 . f) * (t1 ! a))) & for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds ((t2 ! b) * (F1 . f)) = ((F2 . f) * (t2 ! a)) by A1, Def7;

        F is_transformable_to F1 & F1 is_transformable_to F2 by A1;

        then for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds (((t2 `*` t1) ! b) * (F . f)) = ((F2 . f) * ((t2 `*` t1) ! a)) by A3, Lm2;

        then (t2 `*` t1) is natural_transformation of F, F2 by A2, Def7;

        hence thesis;

      end;

      correctness ;

    end

    theorem :: FUNCTOR2:9

    for A,B be transitive with_units non empty AltCatStr, F1,F2 be covariant Functor of A, B holds F1 is_naturally_transformable_to F2 implies for t be natural_transformation of F1, F2 holds (( idt F2) `*` t) = t & (t `*` ( idt F1)) = t by Th5;

    theorem :: FUNCTOR2:10

    for A,B be transitive with_units non empty AltCatStr, F,F1,F2 be covariant Functor of A, B holds F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies for t1 be natural_transformation of F, F1 holds for t2 be natural_transformation of F1, F2 holds for a be Object of A holds ((t2 `*` t1) ! a) = ((t2 ! a) * (t1 ! a)) by Def5;

    theorem :: FUNCTOR2:11

    for A,B be category, F,F1,F2,F3 be covariant Functor of A, B holds for t be natural_transformation of F, F1, t1 be natural_transformation of F1, F2 holds F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies for t3 be natural_transformation of F2, F3 holds ((t3 `*` t1) `*` t) = (t3 `*` (t1 `*` t))

    proof

      let A,B be category, F,F1,F2,F3 be covariant Functor of A, B;

      let t be natural_transformation of F, F1, t1 be natural_transformation of F1, F2;

      assume that

       A1: F is_naturally_transformable_to F1 and

       A2: F1 is_naturally_transformable_to F2 and

       A3: F2 is_naturally_transformable_to F3;

      

       A4: F is_naturally_transformable_to F2 by A1, A2, Th8;

      let t3 be natural_transformation of F2, F3;

      

       A5: F2 is_transformable_to F3 by A3;

      

       A6: F is_transformable_to F1 & F1 is_transformable_to F2 by A1, A2;

      F1 is_naturally_transformable_to F3 by A2, A3, Th8;

      

      hence ((t3 `*` t1) `*` t) = ((t3 `*` t1) `*` t qua transformation of F, F1) by A1, Def8

      .= ((t3 qua transformation of F2, F3 `*` t1) `*` t) by A2, A3, Def8

      .= (t3 `*` (t1 `*` t qua transformation of F, F1)) by A6, A5, Th6

      .= (t3 qua transformation of F2, F3 `*` (t1 `*` t)) by A1, A2, Def8

      .= (t3 `*` (t1 `*` t)) by A3, A4, Def8;

    end;

    begin

    definition

      let I be set;

      let A,B be ManySortedSet of I;

      :: FUNCTOR2:def9

      func Funcs (A,B) -> set means

      : Def9: for x be set holds x in it iff x is ManySortedFunction of A, B if for i be set st i in I holds (B . i) = {} implies (A . i) = {}

      otherwise it = {} ;

      existence

      proof

        thus (for i be set st i in I holds (B . i) = {} implies (A . i) = {} ) implies ex IT be set st for x be set holds x in IT iff x is ManySortedFunction of A, B

        proof

          deffunc F( object) = ( Funcs ((A . $1),(B . $1)));

          assume

           A1: for i be set st i in I holds (B . i) = {} implies (A . i) = {} ;

          consider F be ManySortedSet of I such that

           A2: for i be object st i in I holds (F . i) = F(i) from PBOOLE:sch 4;

          take ( product F);

          let x be set;

          thus x in ( product F) implies x is ManySortedFunction of A, B

          proof

            assume x in ( product F);

            then

            consider g be Function such that

             A3: x = g and

             A4: ( dom g) = ( dom F) and

             A5: for i be object st i in ( dom F) holds (g . i) in (F . i) by CARD_3:def 5;

            

             A6: for i be object st i in I holds (g . i) is Function of (A . i), (B . i)

            proof

              let i be object such that

               A7: i in I;

              ( dom F) = I & (F . i) = ( Funcs ((A . i),(B . i))) by A2, A7, PARTFUN1:def 2;

              hence thesis by A5, A7, FUNCT_2: 66;

            end;

            ( dom F) = I by PARTFUN1:def 2;

            then

            reconsider g as ManySortedSet of I by A4, PARTFUN1:def 2, RELAT_1:def 18;

            g is ManySortedFunction of A, B by A6, PBOOLE:def 15;

            hence thesis by A3;

          end;

          assume

           A8: x is ManySortedFunction of A, B;

          then

          reconsider g = x as ManySortedSet of I;

          

           A9: for i be set st i in I holds (g . i) in ( Funcs ((A . i),(B . i)))

          proof

            let i be set;

            assume

             A10: i in I;

            then

             A11: (B . i) = {} implies (A . i) = {} by A1;

            (g . i) is Function of (A . i), (B . i) by A8, A10, PBOOLE:def 15;

            hence thesis by A11, FUNCT_2: 8;

          end;

          

           A12: for i be set st i in I holds (g . i) in (F . i)

          proof

            let i be set;

            assume

             A13: i in I;

            then (F . i) = ( Funcs ((A . i),(B . i))) by A2;

            hence thesis by A9, A13;

          end;

          

           A14: for i be object st i in ( dom F) holds (g . i) in (F . i)

          proof

            

             A15: ( dom F) = I by PARTFUN1:def 2;

            let i be object;

            assume i in ( dom F);

            hence thesis by A12, A15;

          end;

          ( dom g) = I by PARTFUN1:def 2;

          then ( dom g) = ( dom F) by PARTFUN1:def 2;

          hence thesis by A14, CARD_3:def 5;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let it1,it2 be set;

        hereby

          assume for i be set st i in I holds (B . i) = {} implies (A . i) = {} ;

          assume that

           A16: for x be set holds x in it1 iff x is ManySortedFunction of A, B and

           A17: for x be set holds x in it2 iff x is ManySortedFunction of A, B;

          now

            let x be object;

            x in it1 iff x is ManySortedFunction of A, B by A16;

            hence x in it1 iff x in it2 by A17;

          end;

          hence it1 = it2 by TARSKI: 2;

        end;

        thus thesis;

      end;

      consistency ;

    end

    definition

      let A,B be transitive with_units non empty AltCatStr;

      :: FUNCTOR2:def10

      func Funct (A,B) -> set means

      : Def10: for x be object holds x in it iff x is covariant strict Functor of A, B;

      existence

      proof

        set A9 = ( Funcs ( [:the carrier of A, the carrier of A:], [:the carrier of B, the carrier of B:]));

        set sAA = the set of all (the Arrows of B * f) where f be Element of A9;

        set f = the Element of A9;

        (the Arrows of B * f) in sAA;

        then

        reconsider sAA as non empty set;

        defpred R[ object, object] means ex f be Covariant bifunction of the carrier of A, the carrier of B, m be MSUnTrans of f, the Arrows of A, the Arrows of B st $1 = [f, m] & $2 = FunctorStr (# f, m #) & $2 is covariant Functor of A, B;

        defpred P[ object, object] means ex AA be ManySortedSet of [:the carrier of A, the carrier of A:] st $1 = AA & $2 = ( Funcs (the Arrows of A,AA));

        

         A1: for x,y,z be object st P[x, y] & P[x, z] holds y = z;

        consider XX be set such that

         A2: for x be object holds x in XX iff ex y be object st y in sAA & P[y, x] from TARSKI:sch 1( A1);

        

         A3: for x,y,z be object st R[x, y] & R[x, z] holds y = z

        proof

          let x,y,z be object;

          given f be Covariant bifunction of the carrier of A, the carrier of B, m be MSUnTrans of f, the Arrows of A, the Arrows of B such that

           A4: x = [f, m] and

           A5: y = FunctorStr (# f, m #) and y is covariant Functor of A, B;

          given f1 be Covariant bifunction of the carrier of A, the carrier of B, m1 be MSUnTrans of f1, the Arrows of A, the Arrows of B such that

           A6: x = [f1, m1] and

           A7: z = FunctorStr (# f1, m1 #) and z is covariant Functor of A, B;

          f = f1 by A4, A6, XTUPLE_0: 1;

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

        end;

        consider X be set such that

         A8: for x be object holds x in X iff ex y be object st y in [:A9, ( union XX):] & R[y, x] from TARSKI:sch 1( A3);

        take X;

        let x be object;

        thus x in X implies x is covariant strict Functor of A, B

        proof

          assume x in X;

          then ex y be object st y in [:A9, ( union XX):] & ex f be Covariant bifunction of the carrier of A, the carrier of B, m be MSUnTrans of f, the Arrows of A, the Arrows of B st y = [f, m] & x = FunctorStr (# f, m #) & x is covariant Functor of A, B by A8;

          hence thesis;

        end;

        assume x is covariant strict Functor of A, B;

        then

        reconsider F = x as covariant strict Functor of A, B;

        reconsider f = the ObjectMap of F as Covariant bifunction of the carrier of A, the carrier of B by FUNCTOR0:def 12;

        reconsider m = the MorphMap of F as MSUnTrans of f, the Arrows of A, the Arrows of B;

        reconsider y = [f, m] as set by TARSKI: 1;

        

         A9: for o1,o2 be Object of A st (the Arrows of A . (o1,o2)) <> {} holds (the Arrows of B . (f . (o1,o2))) <> {}

        proof

          let o1,o2 be Object of A such that

           A10: (the Arrows of A . (o1,o2)) <> {} ;

          (the Arrows of A . (o1,o2)) = <^o1, o2^>;

          hence thesis by A10, FUNCTOR0:def 11;

        end;

        

         A11: for o1,o2 be Object of A st (the Arrows of A . (o1,o2)) <> {} holds (the Arrows of B . [(F . o1), (F . o2)]) <> {}

        proof

          let o1,o2 be Object of A such that

           A12: (the Arrows of A . (o1,o2)) <> {} ;

          (f . (o1,o2)) = [(F . o1), (F . o2)] by FUNCTOR0: 22;

          hence thesis by A9, A12;

        end;

        y in [:A9, ( union XX):]

        proof

          set I = [:the carrier of A, the carrier of A:];

          reconsider AA = (the Arrows of B * f) as ManySortedSet of [:the carrier of A, the carrier of A:];

          

           A13: for i be set st i in I & (the Arrows of A . i) <> {} holds (the Arrows of B . (f . i)) <> {}

          proof

            let i be set such that

             A14: i in I and

             A15: (the Arrows of A . i) <> {} ;

            consider o1,o2 be object such that

             A16: o1 in the carrier of A & o2 in the carrier of A and

             A17: i = [o1, o2] by A14, ZFMISC_1:def 2;

            reconsider a1 = o1, a2 = o2 as Object of A by A16;

            

             A18: (the Arrows of B . (f . i)) = (the Arrows of B . (f . (o1,o2))) by A17

            .= (the Arrows of B . [(F . a1), (F . a2)]) by FUNCTOR0: 22;

            (the Arrows of A . (o1,o2)) <> {} by A15, A17;

            hence thesis by A11, A18;

          end;

          for i be set st i in I holds (the Arrows of A . i) <> {} implies (AA . i) <> {}

          proof

            let i be set such that

             A19: i in I;

            assume

             A20: (the Arrows of A . i) <> {} ;

            (AA . i) = (the Arrows of B . (f . i)) by A19, FUNCT_2: 15;

            hence thesis by A13, A19, A20;

          end;

          then m is ManySortedFunction of the Arrows of A, AA & for i be set st i in I holds (AA . i) = {} implies (the Arrows of A . i) = {} by FUNCTOR0:def 4;

          then

           A21: m in ( Funcs (the Arrows of A,AA)) by Def9;

          

           A22: f in A9 by FUNCT_2: 8;

          then (the Arrows of B * f) in sAA;

          then ( Funcs (the Arrows of A,AA)) in XX by A2;

          then m in ( union XX) by A21, TARSKI:def 4;

          hence thesis by A22, ZFMISC_1:def 2;

        end;

        hence thesis by A8;

      end;

      uniqueness

      proof

        let it1,it2 be set such that

         A23: for x be object holds x in it1 iff x is covariant strict Functor of A, B and

         A24: for x be object holds x in it2 iff x is covariant strict Functor of A, B;

        now

          let x be object;

          x in it1 iff x is covariant strict Functor of A, B by A23;

          hence x in it1 iff x in it2 by A24;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let A,B be category;

      :: FUNCTOR2:def11

      func Functors (A,B) -> strict non empty transitive AltCatStr means the carrier of it = ( Funct (A,B)) & (for F,G be strict covariant Functor of A, B, x be set holds x in (the Arrows of it . (F,G)) iff F is_naturally_transformable_to G & x is natural_transformation of F, G) & for F,G,H be strict covariant Functor of A, B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 be natural_transformation of F, G, t2 be natural_transformation of G, H holds ex f be Function st f = (the Comp of it . (F,G,H)) & (f . (t2,t1)) = (t2 `*` t1);

      existence

      proof

        defpred Q[ object, object, object] means for f,g,h be strict covariant Functor of A, B st [f, g, h] = $3 holds for t1 be natural_transformation of f, g holds for t2 be natural_transformation of g, h st [t2, t1] = $2 & ex v be Function st (v . $2) = $1 holds $1 = (t2 `*` t1);

        defpred P[ object, object] means ex D2 be set st D2 = $2 & for f,g be strict covariant Functor of A, B st [f, g] = $1 holds for x be set holds x in D2 iff f is_naturally_transformable_to g & x is natural_transformation of f, g;

        

         A1: for i be object st i in [:( Funct (A,B)), ( Funct (A,B)):] holds ex j be object st P[i, j]

        proof

          let i be object;

          assume i in [:( Funct (A,B)), ( Funct (A,B)):];

          then

          consider f,g be object such that

           A2: f in ( Funct (A,B)) & g in ( Funct (A,B)) and

           A3: i = [f, g] by ZFMISC_1:def 2;

          reconsider f, g as strict covariant Functor of A, B by A2, Def10;

          defpred P[ Object of A, object] means $2 = <^(f . $1), (g . $1)^>;

          defpred P[ object] means f is_naturally_transformable_to g & $1 is natural_transformation of f, g;

          

           A4: for a be Element of A holds ex j be object st P[a, j];

          consider N be ManySortedSet of the carrier of A such that

           A5: for a be Element of A holds P[a, (N . a)] from PBOOLE:sch 6( A4);

          consider j be set such that

           A6: for x be object holds x in j iff x in ( product N) & P[x] from XBOOLE_0:sch 1;

          take j, j;

          thus j = j;

          let f9,g9 be strict covariant Functor of A, B such that

           A7: [f9, g9] = i;

          let x be set;

          thus x in j implies f9 is_naturally_transformable_to g9 & x is natural_transformation of f9, g9

          proof

            assume

             A8: x in j;

            f9 = f & g9 = g by A3, A7, XTUPLE_0: 1;

            hence thesis by A6, A8;

          end;

          thus f9 is_naturally_transformable_to g9 & x is natural_transformation of f9, g9 implies x in j

          proof

            

             A9: f9 = f & g9 = g by A3, A7, XTUPLE_0: 1;

            set I = the carrier of A;

            assume that

             A10: f9 is_naturally_transformable_to g9 and

             A11: x is natural_transformation of f9, g9;

            reconsider h = x as ManySortedSet of the carrier of A by A11;

            

             A12: f9 is_transformable_to g9 by A10;

            

             A13: for i9 be set st i9 in I holds (h . i9) in (N . i9)

            proof

              let i9 be set;

              assume i9 in I;

              then

              reconsider i9 as Element of A;

              

               A14: P[i9, (N . i9)] by A5;

               <^(f . i9), (g . i9)^> <> {} & (h . i9) is Element of <^(f . i9), (g . i9)^> by A11, A12, A9, Def2;

              hence thesis by A14;

            end;

            

             A15: for i9 be object st i9 in ( dom N) holds (h . i9) in (N . i9)

            proof

              

               A16: ( dom N) = I by PARTFUN1:def 2;

              let i9 be object;

              assume i9 in ( dom N);

              hence thesis by A13, A16;

            end;

            ( dom h) = the carrier of A by PARTFUN1:def 2;

            then ( dom h) = ( dom N) by PARTFUN1:def 2;

            then x in ( product N) by A15, CARD_3: 9;

            hence thesis by A6, A10, A11, A9;

          end;

        end;

        consider a be ManySortedSet of [:( Funct (A,B)), ( Funct (A,B)):] such that

         A17: for i be object st i in [:( Funct (A,B)), ( Funct (A,B)):] holds P[i, (a . i)] from PBOOLE:sch 3( A1);

        

         A18: for o be object st o in [:( Funct (A,B)), ( Funct (A,B)), ( Funct (A,B)):] holds for x be object st x in ( {|a, a|} . o) holds ex y be object st y in ( {|a|} . o) & Q[y, x, o]

        proof

          let o be object;

          assume o in [:( Funct (A,B)), ( Funct (A,B)), ( Funct (A,B)):];

          then o in [: [:( Funct (A,B)), ( Funct (A,B)):], ( Funct (A,B)):] by ZFMISC_1:def 3;

          then

          consider ff,h be object such that

           A19: ff in [:( Funct (A,B)), ( Funct (A,B)):] and

           A20: h in ( Funct (A,B)) and

           A21: o = [ff, h] by ZFMISC_1:def 2;

          consider f,g be object such that

           A22: f in ( Funct (A,B)) & g in ( Funct (A,B)) and

           A23: ff = [f, g] by A19, ZFMISC_1:def 2;

          

           A24: o = [f, g, h] by A21, A23;

          reconsider T = ( Funct (A,B)) as non empty set by A20;

          reconsider i = f, j = g, k = h as Element of T by A20, A22;

          

           A25: ( {|a|} . [i, j, k]) = ( {|a|} . (i,j,k)) by MULTOP_1:def 1

          .= (a . (i,k)) by ALTCAT_1:def 3;

          

           A26: ( {|a, a|} . [i, j, k]) = ( {|a, a|} . (i,j,k)) by MULTOP_1:def 1

          .= [:(a . (j,k)), (a . (i,j)):] by ALTCAT_1:def 4;

          for x be object st x in ( {|a, a|} . o) holds ex y be object st y in ( {|a|} . o) & Q[y, x, o]

          proof

            reconsider i9 = i, j9 = j, k9 = k as strict covariant Functor of A, B by Def10;

            let x be object;

            assume x in ( {|a, a|} . o);

            then

            consider x2,x1 be object such that

             A27: x2 in (a . (j,k)) and

             A28: x1 in (a . (i,j)) and

             A29: x = [x2, x1] by A24, A26, ZFMISC_1:def 2;

            

             A30: x2 in (a . [j, k]) by A27;

            

             A31: P[ [j, k], (a . [j, k])] by A17;

            then

             A32: j9 is_naturally_transformable_to k9 by A30;

            reconsider x2 as natural_transformation of j9, k9 by A30, A31;

            

             A33: x1 in (a . [i, j]) by A28;

             P[ [i, j], (a . [i, j])] by A17;

            then

            reconsider x1 as natural_transformation of i9, j9 by A33;

            reconsider vv = (x2 `*` x1) as natural_transformation of i9, k9;

            

             A34: for f,g,h be strict covariant Functor of A, B st [f, g, h] = o holds for t1 be natural_transformation of f, g holds for t2 be natural_transformation of g, h st [t2, t1] = x & ex v be Function st (v . x) = vv holds vv = (t2 `*` t1)

            proof

              let f,g,h be strict covariant Functor of A, B such that

               A35: [f, g, h] = o;

              

               A36: j9 = g by A24, A35, XTUPLE_0: 3;

              then

              reconsider x2 as natural_transformation of g, h by A24, A35, XTUPLE_0: 3;

              

               A37: i9 = f & k9 = h by A24, A35, XTUPLE_0: 3;

              let t1 be natural_transformation of f, g, t2 be natural_transformation of g, h such that

               A38: [t2, t1] = x and ex v be Function st (v . x) = vv;

              x2 = t2 by A29, A38, XTUPLE_0: 1;

              hence thesis by A29, A38, A36, A37, XTUPLE_0: 1;

            end;

             P[ [i, j], (a . [i, j])] by A17;

            then i9 is_naturally_transformable_to j9 by A33;

            then

             A39: i9 is_naturally_transformable_to k9 by A32, Th8;

             P[ [i, k], (a . [i, k])] by A17;

            then vv in (a . [i9, k9]) by A39;

            hence thesis by A24, A25, A34;

          end;

          hence thesis;

        end;

        consider c be ManySortedFunction of {|a, a|}, {|a|} such that

         A40: for i be object st i in [:( Funct (A,B)), ( Funct (A,B)), ( Funct (A,B)):] holds ex v be Function of ( {|a, a|} . i), ( {|a|} . i) st v = (c . i) & for x be object st x in ( {|a, a|} . i) holds Q[(v . x), x, i] from MSSUBFAM:sch 1( A18);

        set F = AltCatStr (# ( Funct (A,B)), a, c #);

        

         A41: ( Funct (A,B)) is non empty

        proof

          set f = the strict covariant Functor of A, B;

          f in ( Funct (A,B)) by Def10;

          hence thesis;

        end;

        F is transitive

        proof

          let o1,o2,o3 be Object of F;

          reconsider a1 = o1, a2 = o2, a3 = o3 as strict covariant Functor of A, B by A41, Def10;

          assume that

           A42: <^o1, o2^> <> {} and

           A43: <^o2, o3^> <> {} ;

          consider x be object such that

           A44: x in (a . [o2, o3]) by A43, XBOOLE_0:def 1;

           [o2, o3] in [:( Funct (A,B)), ( Funct (A,B)):] by A41, ZFMISC_1:def 2;

          then

           A45: P[ [o2, o3], (a . [o2, o3])] by A17;

          then

           A46: a2 is_naturally_transformable_to a3 by A44;

          reconsider x as natural_transformation of a2, a3 by A44, A45;

          consider y be object such that

           A47: y in (a . [o1, o2]) by A42, XBOOLE_0:def 1;

           [o1, o2] in [:( Funct (A,B)), ( Funct (A,B)):] by A41, ZFMISC_1:def 2;

          then

           A48: P[ [o1, o2], (a . [o1, o2])] by A17;

          then

          reconsider y as natural_transformation of a1, a2 by A47;

          a1 is_naturally_transformable_to a2 by A47, A48;

          then

           A49: a1 is_naturally_transformable_to a3 by A46, Th8;

          

           A50: (x `*` y) is natural_transformation of a1, a3 & [o1, o3] in [:( Funct (A,B)), ( Funct (A,B)):] by A41, ZFMISC_1:def 2;

          then P[ [o1, o3], (a . [o1, o3])] by A17;

          hence thesis by A49, A50;

        end;

        then

        reconsider F as strict non empty transitive AltCatStr by A41;

        take F;

        thus the carrier of F = ( Funct (A,B));

        thus for f,g be strict covariant Functor of A, B, x be set holds x in (the Arrows of F . (f,g)) iff f is_naturally_transformable_to g & x is natural_transformation of f, g

        proof

          let f,g be strict covariant Functor of A, B;

          let x be set;

          thus x in (the Arrows of F . (f,g)) implies f is_naturally_transformable_to g & x is natural_transformation of f, g

          proof

            f in ( Funct (A,B)) & g in ( Funct (A,B)) by Def10;

            then

             A51: [f, g] in [:( Funct (A,B)), ( Funct (A,B)):] by ZFMISC_1:def 2;

            assume

             A52: x in (the Arrows of F . (f,g));

             P[ [f, g], (a . [f, g])] by A17, A51;

            hence thesis by A52;

          end;

          thus f is_naturally_transformable_to g & x is natural_transformation of f, g implies x in (the Arrows of F . (f,g))

          proof

            f in ( Funct (A,B)) & g in ( Funct (A,B)) by Def10;

            then

             A53: [f, g] in [:( Funct (A,B)), ( Funct (A,B)):] by ZFMISC_1: 87;

            assume

             A54: f is_naturally_transformable_to g & x is natural_transformation of f, g;

             P[ [f, g], (a . [f, g])] by A17, A53;

            hence thesis by A54;

          end;

        end;

        let f,g,h be strict covariant Functor of A, B such that

         A55: f is_naturally_transformable_to g and

         A56: g is_naturally_transformable_to h;

        let t1 be natural_transformation of f, g, t2 be natural_transformation of g, h;

        

         A57: f in ( Funct (A,B)) by Def10;

        then

        reconsider T = ( Funct (A,B)) as non empty set;

        

         A58: g in ( Funct (A,B)) by Def10;

        then

         A59: [f, g] in [:( Funct (A,B)), ( Funct (A,B)):] by A57, ZFMISC_1: 87;

        

         A60: h in ( Funct (A,B)) by Def10;

        then [g, h] in [:( Funct (A,B)), ( Funct (A,B)):] by A58, ZFMISC_1: 87;

        then P[ [g, h], (a . [g, h])] by A17;

        then

         A61: t2 in (a . [g, h]) by A56;

        reconsider i = f, j = g, k = h as Element of T by Def10;

        

         A62: ( {|a, a|} . [i, j, k]) = ( {|a, a|} . (i,j,k)) by MULTOP_1:def 1

        .= [:(a . (j,k)), (a . (i,j)):] by ALTCAT_1:def 4;

         [:( Funct (A,B)), ( Funct (A,B)), ( Funct (A,B)):] = [: [:( Funct (A,B)), ( Funct (A,B)):], ( Funct (A,B)):] & [f, g, h] = [ [f, g], h] by ZFMISC_1:def 3;

        then [f, g, h] in [:( Funct (A,B)), ( Funct (A,B)), ( Funct (A,B)):] by A60, A59, ZFMISC_1: 87;

        then

        consider v be Function of ( {|a, a|} . [f, g, h]), ( {|a|} . [f, g, h]) such that

         A63: v = (c . [f, g, h]) and

         A64: for x be object st x in ( {|a, a|} . [f, g, h]) holds Q[(v . x), x, [f, g, h]] by A40;

         P[ [f, g], (a . [f, g])] by A17, A59;

        then t1 in (a . [f, g]) by A55;

        then [t2, t1] in ( {|a, a|} . [f, g, h]) by A62, A61, ZFMISC_1: 87;

        then

         A65: (v . (t2,t1)) = (t2 `*` t1) by A64;

        v = (c . (f,g,h)) by A63, MULTOP_1:def 1;

        hence thesis by A65;

      end;

      uniqueness

      proof

        let C1,C2 be strict non empty transitive AltCatStr such that

         A66: the carrier of C1 = ( Funct (A,B)) and

         A67: for F,G be strict covariant Functor of A, B, x be set holds x in (the Arrows of C1 . (F,G)) iff F is_naturally_transformable_to G & x is natural_transformation of F, G and

         A68: for F,G,H be strict covariant Functor of A, B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 be natural_transformation of F, G, t2 be natural_transformation of G, H holds ex f be Function st f = (the Comp of C1 . (F,G,H)) & (f . (t2,t1)) = (t2 `*` t1) and

         A69: the carrier of C2 = ( Funct (A,B)) and

         A70: for F,G be strict covariant Functor of A, B, x be set holds x in (the Arrows of C2 . (F,G)) iff F is_naturally_transformable_to G & x is natural_transformation of F, G and

         A71: for F,G,H be strict covariant Functor of A, B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds for t1 be natural_transformation of F, G, t2 be natural_transformation of G, H holds ex f be Function st f = (the Comp of C2 . (F,G,H)) & (f . (t2,t1)) = (t2 `*` t1);

        set R = the carrier of C1, T = the carrier of C2, N = the Arrows of C1, M = the Arrows of C2, O = the Comp of C1, P = the Comp of C2;

        

         A72: for i,j be object st i in R & j in T holds (N . (i,j)) = (M . (i,j))

        proof

          let i,j be object such that

           A73: i in R and

           A74: j in T;

          reconsider g = j as strict covariant Functor of A, B by A69, A74, Def10;

          reconsider f = i as strict covariant Functor of A, B by A66, A73, Def10;

          now

            let x be object;

            x in (N . (i,j)) iff f is_naturally_transformable_to g & x is natural_transformation of f, g by A67;

            hence x in (N . (i,j)) iff x in (M . (i,j)) by A70;

          end;

          hence thesis by TARSKI: 2;

        end;

        then

         A75: the Arrows of C1 = the Arrows of C2 by A66, A69, ALTCAT_1: 6;

        for i,j,k be object st i in R & j in R & k in R holds (O . (i,j,k)) = (P . (i,j,k))

        proof

          let i,j,k be object;

          assume that

           A76: i in R and

           A77: j in R and

           A78: k in R;

          reconsider h = k as strict covariant Functor of A, B by A66, A78, Def10;

          reconsider g = j as strict covariant Functor of A, B by A66, A77, Def10;

          reconsider f = i as strict covariant Functor of A, B by A66, A76, Def10;

          per cases ;

            suppose

             A79: (N . (i,j)) = {} or (N . (j,k)) = {} ;

            thus (O . (i,j,k)) = (P . (i,j,k))

            proof

              per cases by A79;

                suppose

                 A80: (N . (i,j)) = {} ;

                reconsider T as non empty set;

                reconsider i9 = i, j9 = j, k9 = k as Element of T by A66, A69, A76, A77, A78;

                (M . (i,j)) = {} by A66, A69, A72, A80, ALTCAT_1: 6;

                then

                 A81: [:(M . (j9,k9)), (M . (i9,j9)):] = {} by ZFMISC_1: 90;

                

                 A82: ( {|M, M|} . [i9, j9, k9]) = ( {|M, M|} . (i9,j9,k9)) by MULTOP_1:def 1

                .= [:(M . (j9,k9)), (M . (i9,j9)):] by ALTCAT_1:def 4;

                

                 A83: ( {|M|} . [i9, j9, k9]) = ( {|M|} . (i9,j9,k9)) by MULTOP_1:def 1

                .= (M . (i9,k9)) by ALTCAT_1:def 3;

                (P . [i9, j9, k9]) = (P . (i9,j9,k9)) by MULTOP_1:def 1;

                then

                 A84: (P . (i9,j9,k9)) is Function of [:(M . (j9,k9)), (M . (i9,j9)):], (M . (i9,k9)) by A82, A83, PBOOLE:def 15;

                

                 A85: ( {|M, M|} . [i9, j9, k9]) = ( {|M, M|} . (i9,j9,k9)) by MULTOP_1:def 1

                .= [:(M . (j9,k9)), (M . (i9,j9)):] by ALTCAT_1:def 4;

                

                 A86: ( {|M|} . [i9, j9, k9]) = ( {|M|} . (i9,j9,k9)) by MULTOP_1:def 1

                .= (M . (i9,k9)) by ALTCAT_1:def 3;

                (O . [i9, j9, k9]) = (O . (i9,j9,k9)) by MULTOP_1:def 1;

                then (O . (i9,j9,k9)) is Function of [:(M . (j9,k9)), (M . (i9,j9)):], (M . (i9,k9)) by A66, A69, A75, A85, A86, PBOOLE:def 15;

                hence thesis by A81, A84;

              end;

                suppose

                 A87: (N . (j,k)) = {} ;

                reconsider T as non empty set;

                reconsider i9 = i, j9 = j, k9 = k as Element of T by A66, A69, A76, A77, A78;

                (M . (j,k)) = {} by A66, A69, A72, A87, ALTCAT_1: 6;

                then

                 A88: [:(M . (j9,k9)), (M . (i9,j9)):] = {} by ZFMISC_1: 90;

                

                 A89: ( {|M, M|} . [i9, j9, k9]) = ( {|M, M|} . (i9,j9,k9)) by MULTOP_1:def 1

                .= [:(M . (j9,k9)), (M . (i9,j9)):] by ALTCAT_1:def 4;

                

                 A90: ( {|M|} . [i9, j9, k9]) = ( {|M|} . (i9,j9,k9)) by MULTOP_1:def 1

                .= (M . (i9,k9)) by ALTCAT_1:def 3;

                (P . [i9, j9, k9]) = (P . (i9,j9,k9)) by MULTOP_1:def 1;

                then

                 A91: (P . (i9,j9,k9)) is Function of [:(M . (j9,k9)), (M . (i9,j9)):], (M . (i9,k9)) by A89, A90, PBOOLE:def 15;

                

                 A92: ( {|M, M|} . [i9, j9, k9]) = ( {|M, M|} . (i9,j9,k9)) by MULTOP_1:def 1

                .= [:(M . (j9,k9)), (M . (i9,j9)):] by ALTCAT_1:def 4;

                

                 A93: ( {|M|} . [i9, j9, k9]) = ( {|M|} . (i9,j9,k9)) by MULTOP_1:def 1

                .= (M . (i9,k9)) by ALTCAT_1:def 3;

                (O . [i9, j9, k9]) = (O . (i9,j9,k9)) by MULTOP_1:def 1;

                then (O . (i9,j9,k9)) is Function of [:(M . (j9,k9)), (M . (i9,j9)):], (M . (i9,k9)) by A66, A69, A75, A92, A93, PBOOLE:def 15;

                hence thesis by A88, A91;

              end;

            end;

          end;

            suppose that

             A94: (N . (i,j)) <> {} and

             A95: (N . (j,k)) <> {} ;

            reconsider T as non empty set;

            reconsider i9 = i, j9 = j, k9 = k as Element of T by A66, A69, A76, A77, A78;

            

             A96: ( {|M, M|} . [i9, j9, k9]) = ( {|M, M|} . (i9,j9,k9)) by MULTOP_1:def 1

            .= [:(M . (j9,k9)), (M . (i9,j9)):] by ALTCAT_1:def 4;

            

             A97: ( {|M|} . [i9, j9, k9]) = ( {|M|} . (i9,j9,k9)) by MULTOP_1:def 1

            .= (M . (i9,k9)) by ALTCAT_1:def 3;

            (P . [i9, j9, k9]) = (P . (i9,j9,k9)) by MULTOP_1:def 1;

            then

            reconsider t2 = (P . (i,j,k)) as Function of [:(M . (j,k)), (M . (i,j)):], (M . (i,k)) by A96, A97, PBOOLE:def 15;

            

             A98: ( {|M, M|} . [i9, j9, k9]) = ( {|M, M|} . (i9,j9,k9)) by MULTOP_1:def 1

            .= [:(M . (j9,k9)), (M . (i9,j9)):] by ALTCAT_1:def 4;

            

             A99: ( {|M|} . [i9, j9, k9]) = ( {|M|} . (i9,j9,k9)) by MULTOP_1:def 1

            .= (M . (i9,k9)) by ALTCAT_1:def 3;

            (O . [i9, j9, k9]) = (O . (i9,j9,k9)) by MULTOP_1:def 1;

            then

            reconsider t1 = (O . (i,j,k)) as Function of [:(M . (j,k)), (M . (i,j)):], (M . (i,k)) by A66, A69, A75, A98, A99, PBOOLE:def 15;

            

             A100: (M . (j,k)) <> {} by A66, A69, A72, A95, ALTCAT_1: 6;

            

             A101: (M . (i,j)) <> {} by A66, A69, A72, A94, ALTCAT_1: 6;

            for a be Element of (M . (j,k)) holds for b be Element of (M . (i,j)) holds (t1 . (a,b)) = (t2 . (a,b))

            proof

              let a be Element of (M . (j,k)), b be Element of (M . (i,j));

              a in (M . (j,k)) by A100;

              then

               A102: g is_naturally_transformable_to h by A70;

              reconsider a as natural_transformation of g, h by A70, A100;

              b in (M . (i,j)) by A101;

              then

               A103: f is_naturally_transformable_to g by A70;

              reconsider b as natural_transformation of f, g by A70, A101;

              (ex t19 be Function st t19 = (O . (f,g,h)) & (t19 . (a,b)) = (a `*` b)) & ex t29 be Function st t29 = (P . (f,g,h)) & (t29 . (a,b)) = (a `*` b) by A68, A71, A102, A103;

              hence thesis;

            end;

            hence thesis by BINOP_1: 2;

          end;

        end;

        hence thesis by A66, A69, A75, ALTCAT_1: 8;

      end;

    end