functor1.miz



    begin

    reserve X,Y for set;

    reserve Z for non empty set;

    registration

      cluster transitive with_units reflexive for non empty AltCatStr;

      existence

      proof

        set C = the category;

        take C;

        thus thesis;

      end;

    end

    registration

      let A be non empty reflexive AltCatStr;

      cluster non empty reflexive for SubCatStr of A;

      existence

      proof

        reconsider B = A as SubCatStr of A by ALTCAT_2: 20;

        take B;

        thus thesis;

      end;

    end

    registration

      let C1,C2 be non empty reflexive AltCatStr;

      let F be feasible FunctorStr over C1, C2, A be non empty reflexive SubCatStr of C1;

      cluster (F | A) -> feasible;

      coherence ;

    end

    begin

    registration

      let X be set;

      cluster ( id X) -> onto;

      coherence

      proof

        reconsider f = ( id X) as Function of X, X;

        ( rng f) = X;

        hence thesis by FUNCT_2:def 3;

      end;

    end

    theorem :: FUNCTOR1:1

    for A be non empty set, B,C be non empty Subset of A, D be non empty Subset of B st C = D holds ( incl C) = (( incl B) * ( incl D))

    proof

      let A be non empty set, B,C be non empty Subset of A, D be non empty Subset of B such that

       A1: C = D;

      (( incl B) * ( incl D)) = ( id (B /\ D)) by FUNCT_1: 22

      .= ( incl C) by A1, XBOOLE_1: 28;

      hence thesis;

    end;

    theorem :: FUNCTOR1:2

    

     Th2: for f be Function of X, Y st f is bijective holds (f " ) is Function of Y, X

    proof

      let f be Function of X, Y;

      assume

       A1: f is bijective;

      then ( rng f) = Y by FUNCT_2:def 3;

      hence thesis by A1, FUNCT_2: 25;

    end;

    theorem :: FUNCTOR1:3

    for f be Function of X, Y, g be Function of Y, Z st f is bijective & g is bijective holds ex h be Function of X, Z st h = (g * f) & h is bijective

    proof

      let f be Function of X, Y, g be Function of Y, Z;

      assume that

       A1: f is bijective and

       A2: g is bijective;

      

       A3: ( rng g) = Z by A2, FUNCT_2:def 3;

      then Y = {} iff Z = {} ;

      then

      reconsider h = (g * f) as Function of X, Z;

      take h;

      ( rng f) = Y by A1, FUNCT_2:def 3;

      then ( rng (g * f)) = Z by A3, FUNCT_2: 14;

      then h is onto by FUNCT_2:def 3;

      hence thesis by A1, A2;

    end;

    begin

    theorem :: FUNCTOR1:4

    

     Th4: for A be non empty reflexive AltCatStr, B be non empty reflexive SubCatStr of A, C be non empty SubCatStr of A, D be non empty SubCatStr of B st C = D holds ( incl C) = (( incl B) * ( incl D))

    proof

      let A be non empty reflexive AltCatStr, B be non empty reflexive SubCatStr of A, C be non empty SubCatStr of A, D be non empty SubCatStr of B such that

       A1: C = D;

      set X = [:the carrier of B, the carrier of B:], Y = [:the carrier of D, the carrier of D:];

      

       A2: the carrier of D c= the carrier of B by ALTCAT_2:def 11;

      then

       A3: Y c= X by ZFMISC_1: 96;

      for i be object st i in Y holds (the MorphMap of ( incl C) . i) = (((the MorphMap of ( incl B) * the ObjectMap of ( incl D)) ** the MorphMap of ( incl D)) . i)

      proof

        set dom2 = ( dom the MorphMap of ( incl D));

        set dom1 = ( dom (the MorphMap of ( incl B) * the ObjectMap of ( incl D)));

        set XX = the Arrows of B, YY = the Arrows of D;

        let i be object;

        

         A4: (the MorphMap of ( incl C) . i) = (( id the Arrows of C) . i) by FUNCTOR0:def 28;

        

         A5: ( dom ((the MorphMap of ( incl B) * the ObjectMap of ( incl D)) ** the MorphMap of ( incl D))) = (dom2 /\ dom1) & ( dom the MorphMap of ( incl D)) = Y by PARTFUN1:def 2, PBOOLE:def 19;

        

         A6: ( dom (the MorphMap of ( incl B) * the ObjectMap of ( incl D))) = ( dom (the MorphMap of ( incl B) * ( id Y))) by FUNCTOR0:def 28

        .= (( dom the MorphMap of ( incl B)) /\ Y) by FUNCT_1: 19

        .= (X /\ Y) by PARTFUN1:def 2

        .= Y by A2, XBOOLE_1: 28, ZFMISC_1: 96;

        assume

         A7: i in Y;

        then

         A8: i in ( dom ( id Y));

        YY cc= XX by ALTCAT_2:def 11;

        then

         A9: (YY . i) c= (XX . i) by A7;

        

         A10: ((the MorphMap of ( incl B) * the ObjectMap of ( incl D)) . i) = ((the MorphMap of ( incl B) * ( id Y)) . i) by FUNCTOR0:def 28

        .= (the MorphMap of ( incl B) . (( id Y) . i)) by A8, FUNCT_1: 13

        .= (the MorphMap of ( incl B) . i) by A7, FUNCT_1: 18;

        (the MorphMap of ( incl B) . i) = (( id the Arrows of B) . i) & (the MorphMap of ( incl D) . i) = (( id the Arrows of D) . i) by FUNCTOR0:def 28;

        

        then ((the MorphMap of ( incl B) . i) * (the MorphMap of ( incl D) . i)) = ((( id XX) . i) * ( id (YY . i))) by A7, MSUALG_3:def 1

        .= (( id (XX . i)) * ( id (YY . i))) by A3, A7, MSUALG_3:def 1

        .= ( id ((XX . i) /\ (YY . i))) by FUNCT_1: 22

        .= ( id (the Arrows of D . i)) by A9, XBOOLE_1: 28

        .= (the MorphMap of ( incl C) . i) by A1, A7, A4, MSUALG_3:def 1;

        hence thesis by A7, A10, A5, A6, PBOOLE:def 19;

      end;

      then

       A11: the MorphMap of ( incl C) = ((the MorphMap of ( incl B) * the ObjectMap of ( incl D)) ** the MorphMap of ( incl D)) by A1, PBOOLE: 3;

      the ObjectMap of ( incl C) = ( id Y) by A1, FUNCTOR0:def 28

      .= ( id (X /\ Y)) by A2, XBOOLE_1: 28, ZFMISC_1: 96

      .= (( id X) * ( id Y)) by FUNCT_1: 22

      .= (( id X) * the ObjectMap of ( incl D)) by FUNCTOR0:def 28

      .= (the ObjectMap of ( incl B) * the ObjectMap of ( incl D)) by FUNCTOR0:def 28;

      hence thesis by A1, A11, FUNCTOR0:def 36;

    end;

    theorem :: FUNCTOR1:5

    

     Th5: for A,B be non empty AltCatStr, F be FunctorStr over A, B st F is bijective holds the ObjectMap of F is bijective & the MorphMap of F is "1-1"

    proof

      let A,B be non empty AltCatStr, F be FunctorStr over A, B;

      assume

       A1: F is bijective;

      then

       A2: F is injective;

      then F is one-to-one;

      then

       A3: the ObjectMap of F is one-to-one;

      F is surjective by A1;

      then F is onto;

      then

       A4: the ObjectMap of F is onto;

      F is faithful by A2;

      hence thesis by A3, A4;

    end;

    theorem :: FUNCTOR1:6

    

     Th6: for C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be feasible FunctorStr over C1, C2, G be FunctorStr over C2, C3 st F is one-to-one & G is one-to-one holds (G * F) is one-to-one

    proof

      let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be feasible FunctorStr over C1, C2, G be FunctorStr over C2, C3;

      assume F is one-to-one & G is one-to-one;

      then

       A1: the ObjectMap of F is one-to-one & the ObjectMap of G is one-to-one;

      the ObjectMap of (G * F) = (the ObjectMap of G * the ObjectMap of F) by FUNCTOR0:def 36;

      hence the ObjectMap of (G * F) is one-to-one by A1;

    end;

    theorem :: FUNCTOR1:7

    

     Th7: for C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be feasible FunctorStr over C1, C2, G be FunctorStr over C2, C3 st F is faithful & G is faithful holds (G * F) is faithful

    proof

      let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be feasible FunctorStr over C1, C2, G be FunctorStr over C2, C3 such that

       A1: F is faithful and

       A2: G is faithful;

      set MMG = the MorphMap of G;

      

       A3: MMG is "1-1" by A2;

      set MMF = the MorphMap of F;

      set CC2 = [:the carrier of C2, the carrier of C2:];

      set CC1 = [:the carrier of C1, the carrier of C1:];

      reconsider MMGF = the MorphMap of (G * F) as ManySortedFunction of CC1;

      reconsider OMF = the ObjectMap of F as Function of CC1, CC2;

      

       A4: MMGF = ((MMG * OMF) ** MMF) by FUNCTOR0:def 36;

      

       A5: MMF is "1-1" by A1;

      for i be set st i in CC1 holds (MMGF . i) is one-to-one

      proof

        let i be set;

        assume

         A6: i in CC1;

        then i in ( dom ((MMG * OMF) ** MMF)) by PARTFUN1:def 2;

        

        then

         A7: (MMGF . i) = (((MMG * OMF) . i) * (MMF . i)) by A4, PBOOLE:def 19

        .= ((MMG . (OMF . i)) * (MMF . i)) by A6, FUNCT_2: 15;

        (OMF . i) in CC2 by A6, FUNCT_2: 5;

        then

         A8: (MMG . (OMF . i)) is one-to-one by A3, MSUALG_3: 1;

        (MMF . i) is one-to-one by A5, A6, MSUALG_3: 1;

        hence thesis by A7, A8;

      end;

      hence the MorphMap of (G * F) is "1-1" by MSUALG_3: 1;

    end;

    theorem :: FUNCTOR1:8

    

     Th8: for C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be feasible FunctorStr over C1, C2, G be FunctorStr over C2, C3 st F is onto & G is onto holds (G * F) is onto

    proof

      let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be feasible FunctorStr over C1, C2, G be FunctorStr over C2, C3 such that

       A1: F is onto and

       A2: G is onto;

      set CC3 = [:the carrier of C3, the carrier of C3:];

      set CC2 = [:the carrier of C2, the carrier of C2:];

      reconsider OMG = the ObjectMap of G as Function of CC2, CC3;

      OMG is onto by A2;

      then

       A3: ( rng OMG) = CC3 by FUNCT_2:def 3;

      set CC1 = [:the carrier of C1, the carrier of C1:];

      reconsider OMF = the ObjectMap of F as Function of CC1, CC2;

      OMF is onto by A1;

      then ( rng OMF) = CC2 by FUNCT_2:def 3;

      then ( rng (OMG * OMF)) = CC3 by A3, FUNCT_2: 14;

      then (OMG * OMF) is onto by FUNCT_2:def 3;

      hence the ObjectMap of (G * F) is onto by FUNCTOR0:def 36;

    end;

    theorem :: FUNCTOR1:9

    

     Th9: for C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be feasible FunctorStr over C1, C2, G be FunctorStr over C2, C3 st F is full & G is full holds (G * F) is full

    proof

      let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be feasible FunctorStr over C1, C2, G be FunctorStr over C2, C3 such that

       A1: F is full and

       A2: G is full;

      set CC3 = [:the carrier of C3, the carrier of C3:];

      set CC2 = [:the carrier of C2, the carrier of C2:];

      set CC1 = [:the carrier of C1, the carrier of C1:];

      reconsider OMF = the ObjectMap of F as Function of CC1, CC2;

      reconsider OMG = the ObjectMap of G as Function of CC2, CC3;

      consider MMF be ManySortedFunction of the Arrows of C1, (the Arrows of C2 * the ObjectMap of F) such that

       A3: MMF = the MorphMap of F and

       A4: MMF is "onto" by A1;

      consider MMG be ManySortedFunction of the Arrows of C2, (the Arrows of C3 * the ObjectMap of G) such that

       A5: MMG = the MorphMap of G and

       A6: MMG is "onto" by A2;

      ex f be ManySortedFunction of the Arrows of C1, (the Arrows of C3 * the ObjectMap of (G * F)) st f = the MorphMap of (G * F) & f is "onto"

      proof

        reconsider MMGF = the MorphMap of (G * F) as ManySortedFunction of the Arrows of C1, (the Arrows of C3 * the ObjectMap of (G * F)) by FUNCTOR0:def 4;

        take MMGF;

        

         A7: MMGF = ((MMG * OMF) ** MMF) by A3, A5, FUNCTOR0:def 36;

        for i be set st i in CC1 holds ( rng (MMGF . i)) = ((the Arrows of C3 * the ObjectMap of (G * F)) . i)

        proof

          let i be set;

          assume

           A8: i in CC1;

          then

          reconsider MMGI = (MMG . (OMF . i)) as Function of (the Arrows of C2 . (OMF . i)), ((the Arrows of C3 * the ObjectMap of G) . (OMF . i)) by FUNCT_2: 5, PBOOLE:def 15;

          

           A9: (OMF . i) in CC2 by A8, FUNCT_2: 5;

          

           A10: ( rng ((MMG . (OMF . i)) * (MMF . i))) = ( rng (MMG . (OMF . i)))

          proof

            per cases ;

              suppose

               A11: ( rng MMGI) = {} ;

              ( rng ( {} * (MMF . i))) = {} ;

              hence thesis by A11, RELAT_1: 41;

            end;

              suppose

               A12: ( rng MMGI) <> {} ;

              ( rng MMGI) = ((the Arrows of C3 * the ObjectMap of G) . (OMF . i)) by A6, A9;

              then ( dom MMGI) = (the Arrows of C2 . (OMF . i)) by A12, FUNCT_2:def 1;

              

              then ( dom MMGI) = ((the Arrows of C2 * OMF) . i) by A8, FUNCT_2: 15

              .= ( rng (MMF . i)) by A4, A8;

              hence thesis by RELAT_1: 28;

            end;

          end;

          i in ( dom ((MMG * OMF) ** MMF)) by A8, PARTFUN1:def 2;

          

          then ( rng (MMGF . i)) = ( rng (((MMG * OMF) . i) * (MMF . i))) by A7, PBOOLE:def 19

          .= ( rng (MMG . (OMF . i))) by A8, A10, FUNCT_2: 15

          .= ((the Arrows of C3 * the ObjectMap of G) . (OMF . i)) by A6, A9

          .= (the Arrows of C3 . (OMG . (OMF . i))) by A8, FUNCT_2: 5, FUNCT_2: 15

          .= (the Arrows of C3 . ((OMG * OMF) . i)) by A8, FUNCT_2: 15

          .= (the Arrows of C3 . (the ObjectMap of (G * F) . i)) by FUNCTOR0:def 36

          .= ((the Arrows of C3 * the ObjectMap of (G * F)) . i) by A8, FUNCT_2: 15;

          hence thesis;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: FUNCTOR1:10

    

     Th10: for C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be feasible FunctorStr over C1, C2, G be FunctorStr over C2, C3 st F is injective & G is injective holds (G * F) is injective by Th7, Th6;

    theorem :: FUNCTOR1:11

    

     Th11: for C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be feasible FunctorStr over C1, C2, G be FunctorStr over C2, C3 st F is surjective & G is surjective holds (G * F) is surjective by Th8, Th9;

    theorem :: FUNCTOR1:12

    

     Th12: for C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be feasible FunctorStr over C1, C2, G be FunctorStr over C2, C3 st F is bijective & G is bijective holds (G * F) is bijective by Th11, Th10;

    begin

    theorem :: FUNCTOR1:13

    for A,I be non empty reflexive AltCatStr, B be non empty reflexive SubCatStr of A, C be non empty SubCatStr of A, D be non empty SubCatStr of B st C = D holds for F be FunctorStr over A, I holds (F | C) = ((F | B) | D)

    proof

      let A,I be non empty reflexive AltCatStr, B be non empty reflexive SubCatStr of A, C be non empty SubCatStr of A, D be non empty SubCatStr of B such that

       A1: C = D;

      let F be FunctorStr over A, I;

      

      thus (F | C) = (F * (( incl B) * ( incl D))) by A1, Th4

      .= ((F | B) | D) by FUNCTOR0: 32;

    end;

    theorem :: FUNCTOR1:14

    for A be non empty AltCatStr, B be non empty SubCatStr of A holds B is full iff ( incl B) is full

    proof

      let A be non empty AltCatStr, B be non empty SubCatStr of A;

      hereby

        ex I29 be non empty set, B9 be ManySortedSet of I29, f9 be Function of [:the carrier of B, the carrier of B:], I29 st the ObjectMap of ( incl B) = f9 & the Arrows of A = B9 & the MorphMap of ( incl B) is ManySortedFunction of the Arrows of B, (B9 * f9) by FUNCTOR0:def 3;

        then

        reconsider f = the MorphMap of ( incl B) as ManySortedFunction of the Arrows of B, (the Arrows of A * the ObjectMap of ( incl B));

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

        the carrier of B c= the carrier of A & ( dom the Arrows of A) = [:the carrier of A, the carrier of A:] by ALTCAT_2:def 11, PARTFUN1:def 2;

        then

         A1: (( dom the Arrows of A) /\ I) = I by XBOOLE_1: 28, ZFMISC_1: 96;

        assume

         A2: B is full;

        f is "onto"

        proof

          let i be set such that

           A3: i in I;

          the Arrows of B = (the Arrows of A || the carrier of B) by A2;

          then

           A4: (the Arrows of B . i) = (the Arrows of A . i) by A3, FUNCT_1: 49;

          ( rng (f . i)) = ( rng (( id the Arrows of B) . i)) by FUNCTOR0:def 28

          .= ( rng ( id (the Arrows of B . i))) by A3, MSUALG_3:def 1

          .= (the Arrows of A . i) by A4

          .= ((the Arrows of A * ( id I)) . i) by A1, A3, FUNCT_1: 20

          .= ((the Arrows of A * the ObjectMap of ( incl B)) . i) by FUNCTOR0:def 28;

          hence thesis;

        end;

        hence ( incl B) is full;

      end;

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

      

       A5: the carrier of B c= the carrier of A by ALTCAT_2:def 11;

      then

       A6: I c= [:the carrier of A, the carrier of A:] by ZFMISC_1: 96;

      ( dom the Arrows of A) = [:the carrier of A, the carrier of A:] by PARTFUN1:def 2;

      then

       A7: (( dom the Arrows of A) /\ I) = I by A5, XBOOLE_1: 28, ZFMISC_1: 96;

      then ( dom (the Arrows of A | I qua set)) = I by RELAT_1: 61;

      then

      reconsider XX = (the Arrows of A || the carrier of B) as ManySortedSet of I by PARTFUN1:def 2;

      assume

       A8: ( incl B) is full;

      

       A9: XX c= the Arrows of B

      proof

        let i be object such that

         A10: i in I;

        let x be object;

        assume

         A11: x in (XX . i);

        x in (the Arrows of B . i)

        proof

          consider f be ManySortedFunction of the Arrows of B, (the Arrows of A * the ObjectMap of ( incl B)) such that

           A12: f = the MorphMap of ( incl B) and

           A13: f is "onto" by A8;

          f = ( id the Arrows of B) by A12, FUNCTOR0:def 28;

          

          then

           A14: ( rng (( id the Arrows of B) . i)) = ((the Arrows of A * the ObjectMap of ( incl B)) . i) by A10, A13

          .= ((the Arrows of A * ( id I)) . i) by FUNCTOR0:def 28

          .= (the Arrows of A . i) by A7, A10, FUNCT_1: 20;

          consider y,z be object such that y in the carrier of A and z in the carrier of A and

           A15: i = [y, z] by A6, A10, ZFMISC_1: 84;

          y in the carrier of B & z in the carrier of B by A10, A15, ZFMISC_1: 87;

          then

           A16: (XX . (y,z)) = (the Arrows of A . (y,z)) by A5, ALTCAT_1: 5;

          ( rng (( id the Arrows of B) . i)) = ( rng ( id (the Arrows of B . i))) by A10, MSUALG_3:def 1

          .= (the Arrows of B . i);

          hence thesis by A11, A15, A16, A14;

        end;

        hence thesis;

      end;

      the Arrows of B c= XX

      proof

        let i be object;

        assume

         A17: i in I;

        then

        consider y,z be object such that y in the carrier of A and z in the carrier of A and

         A18: i = [y, z] by A6, ZFMISC_1: 84;

        y in the carrier of B & z in the carrier of B by A17, A18, ZFMISC_1: 87;

        then

         A19: (XX . (y,z)) = (the Arrows of A . (y,z)) by A5, ALTCAT_1: 5;

        let x be object;

        assume

         A20: x in (the Arrows of B . i);

        the Arrows of B cc= the Arrows of A by ALTCAT_2:def 11;

        then (the Arrows of B . (y,z)) c= (the Arrows of A . (y,z)) by A17, A18;

        hence thesis by A18, A20, A19;

      end;

      hence the Arrows of B = (the Arrows of A || the carrier of B) by A9, PBOOLE: 146;

    end;

    begin

    theorem :: FUNCTOR1:15

    for C1,C2 be non empty AltCatStr, F be Covariant FunctorStr over C1, C2 holds F is full iff for o1,o2 be Object of C1 holds ( Morph-Map (F,o1,o2)) is onto

    proof

      let C1,C2 be non empty AltCatStr, F be Covariant FunctorStr over C1, C2;

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

      hereby

        assume F is full;

        then

        consider f be ManySortedFunction of the Arrows of C1, (the Arrows of C2 * the ObjectMap of F) such that

         A1: f = the MorphMap of F and

         A2: f is "onto";

        let o1,o2 be Object of C1;

        

         A3: [o1, o2] in I by ZFMISC_1: 87;

        then

         A4: [o1, o2] in ( dom the ObjectMap of F) by FUNCT_2:def 1;

        ( rng (f . [o1, o2])) = ((the Arrows of C2 * the ObjectMap of F) . [o1, o2]) by A2, A3;

        

        then ( rng ( Morph-Map (F,o1,o2))) = (the Arrows of C2 . (the ObjectMap of F . (o1,o2))) by A1, A4, FUNCT_1: 13

        .= (the Arrows of C2 . ((F . o1),(F . o2))) by FUNCTOR0: 22

        .= <^(F . o1), (F . o2)^> by ALTCAT_1:def 1;

        hence ( Morph-Map (F,o1,o2)) is onto by FUNCT_2:def 3;

      end;

      ex I29 be non empty set, B9 be ManySortedSet of I29, f9 be Function of I, I29 st the ObjectMap of F = f9 & the Arrows of C2 = B9 & the MorphMap of F is ManySortedFunction of the Arrows of C1, (B9 * f9) by FUNCTOR0:def 3;

      then

      reconsider f = the MorphMap of F as ManySortedFunction of the Arrows of C1, (the Arrows of C2 * the ObjectMap of F);

      assume

       A5: for o1,o2 be Object of C1 holds ( Morph-Map (F,o1,o2)) is onto;

      f is "onto"

      proof

        let i be set;

        assume i in I;

        then

        consider o1,o2 be object such that

         A6: o1 in the carrier of C1 & o2 in the carrier of C1 and

         A7: i = [o1, o2] by ZFMISC_1: 84;

        reconsider o1, o2 as Object of C1 by A6;

         [o1, o2] in I by ZFMISC_1: 87;

        then

         A8: [o1, o2] in ( dom the ObjectMap of F) by FUNCT_2:def 1;

        ( Morph-Map (F,o1,o2)) is onto by A5;

        

        then ( rng ( Morph-Map (F,o1,o2))) = <^(F . o1), (F . o2)^> by FUNCT_2:def 3

        .= (the Arrows of C2 . ((F . o1),(F . o2))) by ALTCAT_1:def 1

        .= (the Arrows of C2 . (the ObjectMap of F . (o1,o2))) by FUNCTOR0: 22

        .= ((the Arrows of C2 * the ObjectMap of F) . (o1,o2)) by A8, FUNCT_1: 13;

        hence thesis by A7;

      end;

      hence ex f be ManySortedFunction of the Arrows of C1, (the Arrows of C2 * the ObjectMap of F) st f = the MorphMap of F & f is "onto";

    end;

    theorem :: FUNCTOR1:16

    for C1,C2 be non empty AltCatStr, F be Covariant FunctorStr over C1, C2 holds F is faithful iff for o1,o2 be Object of C1 holds ( Morph-Map (F,o1,o2)) is one-to-one

    proof

      let C1,C2 be non empty AltCatStr, F be Covariant FunctorStr over C1, C2;

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

      hereby

        assume F is faithful;

        then

         A1: the MorphMap of F is "1-1";

        let o1,o2 be Object of C1;

         [o1, o2] in I & ( dom the MorphMap of F) = I by PARTFUN1:def 2, ZFMISC_1: 87;

        hence ( Morph-Map (F,o1,o2)) is one-to-one by A1;

      end;

      assume

       A2: for o1,o2 be Object of C1 holds ( Morph-Map (F,o1,o2)) is one-to-one;

      let i be set, f be Function such that

       A3: i in ( dom the MorphMap of F) and

       A4: (the MorphMap of F . i) = f;

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

      then

      consider o1,o2 be object such that

       A5: o1 in the carrier of C1 & o2 in the carrier of C1 and

       A6: i = [o1, o2] by A3, ZFMISC_1: 84;

      reconsider o1, o2 as Object of C1 by A5;

      (the MorphMap of F . (o1,o2)) = ( Morph-Map (F,o1,o2));

      hence thesis by A2, A4, A6;

    end;

    begin

    theorem :: FUNCTOR1:17

    for A be transitive with_units non empty AltCatStr holds (( id A) " ) = ( id A)

    proof

      let A be transitive with_units non empty AltCatStr;

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

      consider f be ManySortedFunction of the Arrows of A, (the Arrows of A * the ObjectMap of ( id A)) such that

       A1: f = the MorphMap of ( id A) and

       A2: the MorphMap of (( id A) " ) = ((f "" ) * (the ObjectMap of ( id A) " )) by FUNCTOR0:def 38;

      

       A3: for i be set st i in CCA holds (( id the Arrows of A) . i) is one-to-one

      proof

        let i be set such that

         A4: i in CCA;

        ( id (the Arrows of A . i)) is one-to-one;

        hence thesis by A4, MSUALG_3:def 1;

      end;

      the MorphMap of ( id A) = ( id the Arrows of A) by FUNCTOR0:def 29;

      then

       A5: the MorphMap of ( id A) is "1-1" by A3, MSUALG_3: 1;

      for i be set st i in CCA holds ( rng (f . i)) = ((the Arrows of A * the ObjectMap of ( id A)) . i)

      proof

        ( dom the Arrows of A) = CCA by PARTFUN1:def 2;

        then

         A6: (( dom the Arrows of A) /\ CCA) = CCA;

        let i be set such that

         A7: i in CCA;

        ( rng (f . i)) = ( rng (( id the Arrows of A) . i)) by A1, FUNCTOR0:def 29

        .= ( rng ( id (the Arrows of A . i))) by A7, MSUALG_3:def 1

        .= (the Arrows of A . i)

        .= ((the Arrows of A * ( id CCA)) . i) by A7, A6, FUNCT_1: 20

        .= ((the Arrows of A * the ObjectMap of ( id A)) . i) by FUNCTOR0:def 29;

        hence thesis;

      end;

      then

       A8: f is "onto";

      for i be object st i in CCA holds ((f "" ) . i) = (f . i)

      proof

        let i be object;

        assume

         A9: i in CCA;

        

        then ((f "" ) . i) = ((the MorphMap of ( id A) . i) " ) by A1, A5, A8, MSUALG_3:def 4

        .= ((( id the Arrows of A) . i) " ) by FUNCTOR0:def 29

        .= (( id (the Arrows of A . i)) " ) by A9, MSUALG_3:def 1

        .= ( id (the Arrows of A . i)) by FUNCT_1: 45

        .= (( id the Arrows of A) . i) by A9, MSUALG_3:def 1

        .= (f . i) by A1, FUNCTOR0:def 29;

        hence thesis;

      end;

      then

       A10: (f "" ) = f;

      for i be object st i in CCA holds ((the MorphMap of ( id A) * ( id CCA)) . i) = (the MorphMap of ( id A) . i)

      proof

        ( dom the MorphMap of ( id A)) = CCA by PARTFUN1:def 2;

        then

         A11: (( dom the MorphMap of ( id A)) /\ CCA) = CCA;

        let i be object;

        assume i in CCA;

        hence thesis by A11, FUNCT_1: 20;

      end;

      then

       A12: (the MorphMap of ( id A) * ( id CCA)) = the MorphMap of ( id A);

      

       A13: the ObjectMap of (( id A) " ) = (the ObjectMap of ( id A) " ) by FUNCTOR0:def 38;

      

      then the ObjectMap of (( id A) " ) = (( id CCA) " ) by FUNCTOR0:def 29

      .= ( id CCA) by FUNCT_1: 45

      .= the ObjectMap of ( id A) by FUNCTOR0:def 29;

      hence thesis by A13, A1, A2, A10, A12, FUNCTOR0:def 29;

    end;

    theorem :: FUNCTOR1:18

    for A,B be transitive with_units reflexive non empty AltCatStr holds for F be feasible FunctorStr over A, B st F is bijective holds for G be feasible FunctorStr over B, A st the FunctorStr of G = (F " ) holds (F * G) = ( id B)

    proof

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

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

      set I2 = [:the carrier of B, the carrier of B:];

      let F be feasible FunctorStr over A, B such that

       A1: F is bijective;

      consider k be ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of F) such that

       A2: k = the MorphMap of F and

       A3: the MorphMap of (F " ) = ((k "" ) * (the ObjectMap of F " )) by A1, FUNCTOR0:def 38;

      F is injective by A1;

      then F is one-to-one;

      then

       A4: the ObjectMap of F is one-to-one;

      set OM = the ObjectMap of F;

      F is surjective by A1;

      then F is onto;

      then the ObjectMap of F is onto;

      then

       A5: ( rng OM) = I2 by FUNCT_2:def 3;

      F is injective by A1;

      then

       A6: F is faithful;

      then

       A7: the MorphMap of F is "1-1";

      F is surjective by A1;

      then F is full onto;

      then

      consider f be ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of F) such that

       A8: f = the MorphMap of F and

       A9: f is "onto";

      let G be feasible FunctorStr over B, A such that

       A10: the FunctorStr of G = (F " );

      

       A11: the ObjectMap of G = (the ObjectMap of F " ) by A1, A10, FUNCTOR0:def 38;

       the FunctorStr of G is bijective by A1, A10, FUNCTOR0: 35;

      then the FunctorStr of G is surjective;

      then the FunctorStr of G is full onto;

      then

       A12: the ObjectMap of G is onto;

      set OMG = the ObjectMap of G;

      

       A13: ( dom OM) = I1 by FUNCT_2:def 1;

      reconsider OM as bifunction of the carrier of A, the carrier of B;

      

       A14: I2 = ( dom ((f * OMG) ** ((k "" ) * OMG))) by PARTFUN1:def 2;

      

       A15: for i be object st i in I2 holds (((f * OMG) ** ((k "" ) * OMG)) . i) = (( id the Arrows of B) . i)

      proof

        let i be object such that

         A16: i in I2;

        

         A17: ( dom OMG) = I2 by FUNCT_2:def 1;

        then

         A18: ((f * OMG) . i) = (k . (OMG . i)) by A2, A8, A16, FUNCT_1: 13;

        ( rng OMG) = I1 by A12, FUNCT_2:def 3;

        then

         A19: (OMG . i) in I1 by A16, A17, FUNCT_1:def 3;

        

        then

         A20: ( rng (f . (OMG . i))) = ((the Arrows of B * the ObjectMap of F) . (OMG . i)) by A9

        .= (the Arrows of B . (the ObjectMap of F . (OMG . i))) by A13, A19, FUNCT_1: 13;

        

         A21: (the ObjectMap of F . (OMG . i)) = ((OM * (OM " )) . i) by A11, A16, A17, FUNCT_1: 13

        .= (( id I2) . i) by A4, A5, FUNCT_1: 39

        .= i by A16, FUNCT_1: 18;

        f is "1-1" & ( dom f) = I1 by A6, A8, PARTFUN1:def 2;

        then

         A22: (f . (OMG . i)) is one-to-one by A19;

        (((k "" ) * OMG) . i) = ((k "" ) . (OMG . i)) by A16, A17, FUNCT_1: 13

        .= ((k . (OMG . i)) " ) by A7, A2, A8, A9, A19, MSUALG_3:def 4;

        

        then (((f * OMG) ** ((k "" ) * OMG)) . i) = ((f . (OMG . i)) * ((f . (OMG . i)) " )) by A2, A8, A14, A16, A18, PBOOLE:def 19

        .= ( id (the Arrows of B . i)) by A22, A20, A21, FUNCT_1: 39

        .= (( id the Arrows of B) . i) by A16, MSUALG_3:def 1;

        hence thesis;

      end;

      the MorphMap of (F * G) = ((f * OMG) ** ((k "" ) * OMG)) by A10, A3, A8, A11, FUNCTOR0:def 36;

      then

       A23: the MorphMap of (F * G) = ( id the Arrows of B) by A15;

      the ObjectMap of (F * G) = (the ObjectMap of F * the ObjectMap of G) by FUNCTOR0:def 36;

      then the ObjectMap of (F * G) = (the ObjectMap of F * (the ObjectMap of F " )) by A1, A10, FUNCTOR0:def 38;

      then the ObjectMap of (F * G) = ( id [:the carrier of B, the carrier of B:]) by A4, A5, FUNCT_1: 39;

      hence thesis by A23, FUNCTOR0:def 29;

    end;

    

     Lm1: for I be set, A,B be ManySortedSet of I st A is_transformable_to B holds for H be ManySortedFunction of A, B, H1 be ManySortedFunction of B, A st H is "1-1" "onto" & H1 = (H "" ) holds (H ** H1) = ( id B) & (H1 ** H) = ( id A)

    proof

      let I be set, A,B be ManySortedSet of I such that

       A1: A is_transformable_to B;

      let H be ManySortedFunction of A, B, H1 be ManySortedFunction of B, A;

      assume that

       A2: H is "1-1" "onto" and

       A3: H1 = (H "" );

      reconsider F1 = (H ** H1) as ManySortedFunction of I;

       A4:

      now

        let i be set;

        assume

         A5: i in I;

        then

        reconsider h = (H . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

        reconsider h1 = (H1 . i) as Function of (B . i), (A . i) by A5, PBOOLE:def 15;

        i in ( dom H) by A5, PARTFUN1:def 2;

        then

         A6: h is one-to-one by A2;

        h1 = (h " ) by A2, A3, A5, MSUALG_3:def 4;

        then (h * h1) = ( id ( rng h)) by A6, FUNCT_1: 39;

        then (h * h1) = ( id (B . i)) by A2, A5;

        hence ((H ** H1) . i) = ( id (B . i)) by A5, MSUALG_3: 2;

      end;

      now

        let i be object;

        assume i in I;

        then (F1 . i) = ( id (B . i)) by A4;

        hence (F1 . i) is Function of (B . i), (B . i);

      end;

      then

       A7: F1 is ManySortedFunction of B, B by PBOOLE:def 15;

      reconsider F = (H1 ** H) as ManySortedFunction of I;

      

       A8: for i be set st i in I holds ((H1 ** H) . i) = ( id (A . i))

      proof

        let i be set;

        assume

         A9: i in I;

        then

        reconsider h = (H . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

        reconsider h1 = (H1 . i) as Function of (B . i), (A . i) by A9, PBOOLE:def 15;

        i in ( dom H) by A9, PARTFUN1:def 2;

        then

         A10: h is one-to-one by A2;

        (B . i) = {} implies (A . i) = {} by A1, A9;

        then

         A11: ( dom h) = (A . i) by FUNCT_2:def 1;

        h1 = (h " ) by A2, A3, A9, MSUALG_3:def 4;

        then (h1 * h) = ( id (A . i)) by A10, A11, FUNCT_1: 39;

        hence thesis by A9, MSUALG_3: 2;

      end;

      now

        let i be object;

        assume i in I;

        then ((H1 ** H) . i) = ( id (A . i)) by A8;

        hence ((H1 ** H) . i) is Function of (A . i), (A . i);

      end;

      then

      reconsider F as ManySortedFunction of A, A by PBOOLE:def 15;

      F = ( id A) by A8, MSUALG_3:def 1;

      hence thesis by A4, A7, MSUALG_3:def 1;

    end;

    theorem :: FUNCTOR1:19

    for A,B be transitive with_units reflexive non empty AltCatStr holds for F be feasible FunctorStr over A, B st F is bijective holds ((F " ) * F) = ( id A)

    proof

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

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

      let F be feasible FunctorStr over A, B such that

       A1: F is bijective;

      consider f be ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of F) such that

       A2: f = the MorphMap of F and

       A3: the MorphMap of (F " ) = ((f "" ) * (the ObjectMap of F " )) by A1, FUNCTOR0:def 38;

      set OM = the ObjectMap of F;

      

       A4: ( dom OM) = I1 by FUNCT_2:def 1;

      

       A5: the Arrows of A is_transformable_to (the Arrows of B * the ObjectMap of F)

      proof

        let i be set;

        assume

         A6: i in I1;

        then

        consider o1,o2 be object such that

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

         A8: i = [o1, o2] by ZFMISC_1: 84;

        reconsider o1, o2 as Object of A by A7;

        

         A9: (the Arrows of A . i) = (the Arrows of A . (o1,o2)) by A8

        .= <^o1, o2^> by ALTCAT_1:def 1;

        assume ((the Arrows of B * the ObjectMap of F) . i) = {} ;

        then (the Arrows of B . (the ObjectMap of F . (o1,o2))) = {} by A6, A8, FUNCT_2: 15;

        hence thesis by A9, FUNCTOR0:def 11;

      end;

      F is injective by A1;

      then F is faithful;

      then

       A10: the MorphMap of F is "1-1";

      for i be object st i in I1 holds (((f "" ) * ( id I1)) . i) = ((f "" ) . i)

      proof

        let i be object;

        assume

         A11: i in I1;

        

        then (((f "" ) * ( id I1)) . i) = ((f "" ) . (( id I1) . i)) by FUNCT_2: 15

        .= ((f "" ) . i) by A11, FUNCT_1: 18;

        hence thesis;

      end;

      then

       A12: ((f "" ) * ( id I1)) = (f "" );

      F is injective by A1;

      then F is one-to-one;

      then

       A13: the ObjectMap of F is one-to-one;

      the ObjectMap of ((F " ) * F) = (the ObjectMap of (F " ) * the ObjectMap of F) by FUNCTOR0:def 36;

      then the ObjectMap of ((F " ) * F) = ((the ObjectMap of F " ) * the ObjectMap of F) by A1, FUNCTOR0:def 38;

      then

       A14: the ObjectMap of ((F " ) * F) = ( id [:the carrier of A, the carrier of A:]) by A13, A4, FUNCT_1: 39;

      F is surjective by A1;

      then F is full onto;

      then

       A15: ex k be ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of F) st k = the MorphMap of F & k is "onto";

      the MorphMap of ((F " ) * F) = ((((f "" ) * (the ObjectMap of F " )) * the ObjectMap of F) ** f) by A2, A3, FUNCTOR0:def 36

      .= (((f "" ) * ((the ObjectMap of F " ) * the ObjectMap of F)) ** f) by RELAT_1: 36;

      then the MorphMap of ((F " ) * F) = (((f "" ) * ( id I1)) ** f) by A13, A4, FUNCT_1: 39;

      then the MorphMap of ((F " ) * F) = ( id the Arrows of A) by A5, A2, A10, A15, A12, Lm1;

      hence thesis by A14, FUNCTOR0:def 29;

    end;

    theorem :: FUNCTOR1:20

    for A,B be transitive with_units reflexive non empty AltCatStr holds for F be feasible FunctorStr over A, B st F is bijective holds ((F " ) " ) = the FunctorStr of F

    proof

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

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

      set CCB = [:the carrier of B, the carrier of B:];

      let F be feasible FunctorStr over A, B such that

       A1: F is bijective;

      

       A2: F is injective by A1;

      then F is one-to-one;

      then

       A3: the ObjectMap of F is one-to-one;

      

       A4: (F " ) is bijective by A1, FUNCTOR0: 35;

      then (F " ) is surjective;

      then

       A5: (F " ) is full;

      (F " ) is injective by A4;

      then

       A6: (F " ) is faithful;

      

       A7: (the ObjectMap of (F " ) " ) = ((the ObjectMap of F " ) " ) by A1, FUNCTOR0:def 38

      .= the ObjectMap of F by A3, FUNCT_1: 43;

      F is faithful by A2;

      then

       A8: the MorphMap of F is "1-1";

      

       A9: F is surjective by A1;

      then F is onto;

      then the ObjectMap of F is onto;

      then

       A10: ( rng the ObjectMap of F) = CCB by FUNCT_2:def 3;

      

       A11: F is full by A9;

      the MorphMap of ((F " ) " ) = the MorphMap of F

      proof

        

         A12: ex kk be ManySortedFunction of the Arrows of B, (the Arrows of A * the ObjectMap of (F " )) st kk = the MorphMap of (F " ) & kk is "onto" by A5;

        

         A13: ex k be ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of F) st k = the MorphMap of F & k is "onto" by A11;

        consider f be ManySortedFunction of the Arrows of B, (the Arrows of A * the ObjectMap of (F " )) such that

         A14: f = the MorphMap of (F " ) and

         A15: the MorphMap of ((F " ) " ) = ((f "" ) * (the ObjectMap of (F " ) " )) by A4, FUNCTOR0:def 38;

        consider g be ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of F) such that

         A16: g = the MorphMap of F and

         A17: the MorphMap of (F " ) = ((g "" ) * (the ObjectMap of F " )) by A1, FUNCTOR0:def 38;

        

         A18: f is "1-1" by A6, A14;

        for i be object st i in CCA holds (((f "" ) * (the ObjectMap of (F " ) " )) . i) = (the MorphMap of F . i)

        proof

          

           A19: (the ObjectMap of F " ) is Function of CCB, CCA by A3, A10, FUNCT_2: 25;

          let i be object;

          assume

           A20: i in CCA;

          then

           A21: (the ObjectMap of F . i) in CCB by FUNCT_2: 5;

          (the ObjectMap of F " ) is Function of CCB, CCA by A3, A10, FUNCT_2: 25;

          then

           A22: ((the ObjectMap of F " ) . (the ObjectMap of F . i)) in CCA by A21, FUNCT_2: 5;

          

           A23: (g . i) is one-to-one by A8, A16, A20, MSUALG_3: 1;

          (((f "" ) * (the ObjectMap of (F " ) " )) . i) = ((f "" ) . (the ObjectMap of F . i)) by A7, A20, FUNCT_2: 15

          .= ((the MorphMap of (F " ) . (the ObjectMap of F . i)) " ) by A14, A12, A18, A21, MSUALG_3:def 4

          .= (((g "" ) . ((the ObjectMap of F " ) . (the ObjectMap of F . i))) " ) by A17, A20, A19, FUNCT_2: 5, FUNCT_2: 15

          .= (((g . ((the ObjectMap of F " ) . (the ObjectMap of F . i))) " ) " ) by A8, A16, A13, A22, MSUALG_3:def 4

          .= (((g . i) " ) " ) by A3, A20, FUNCT_2: 26

          .= (the MorphMap of F . i) by A16, A23, FUNCT_1: 43;

          hence thesis;

        end;

        hence thesis by A15;

      end;

      hence thesis by A4, A7, FUNCTOR0:def 38;

    end;

    theorem :: FUNCTOR1:21

    for A,B,C be transitive with_units reflexive non empty AltCatStr, G be feasible FunctorStr over A, B, F be feasible FunctorStr over B, C, GI be feasible FunctorStr over B, A, FI be feasible FunctorStr over C, B st F is bijective & G is bijective & the FunctorStr of GI = (G " ) & the FunctorStr of FI = (F " ) holds ((F * G) " ) = (GI * FI)

    proof

      let A,B,C be transitive with_units reflexive non empty AltCatStr, G be feasible FunctorStr over A, B, F be feasible FunctorStr over B, C, GI be feasible FunctorStr over B, A, FI be feasible FunctorStr over C, B such that

       A1: F is bijective and

       A2: G is bijective and

       A3: the FunctorStr of GI = (G " ) and

       A4: the FunctorStr of FI = (F " );

      reconsider MF = the MorphMap of F as ManySortedFunction of the Arrows of B, (the Arrows of C * the ObjectMap of F) by FUNCTOR0:def 4;

      

       A5: MF is "1-1" by A1, Th5;

      set OG = the ObjectMap of G;

      set CB = [:the carrier of B, the carrier of B:];

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

      reconsider OGI = (OG " ) as Function of CB, CA by A2, Th2, Th5;

      set CC = [:the carrier of C, the carrier of C:];

      set OF = the ObjectMap of F;

      reconsider OFI = (OF " ) as Function of CC, CB by A1, Th2, Th5;

      reconsider MFG = the MorphMap of (F * G) as ManySortedFunction of the Arrows of A, (the Arrows of C * the ObjectMap of (F * G)) by FUNCTOR0:def 4;

      reconsider OG as Function of CA, CB;

      reconsider OFG = the ObjectMap of (F * G) as Function of CA, CC;

      reconsider MG = the MorphMap of G as ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of G) by FUNCTOR0:def 4;

      

       A6: MG is "1-1" by A2, Th5;

      F is surjective by A1;

      then F is full;

      then

       A7: ex mf be ManySortedFunction of the Arrows of B, (the Arrows of C * the ObjectMap of F) st mf = the MorphMap of F & mf is "onto";

      F is injective by A1;

      then F is one-to-one;

      then

       A8: the ObjectMap of F is one-to-one;

      

       A9: G is surjective by A2;

      then G is onto;

      then

       A10: the ObjectMap of G is onto;

      G is full by A9;

      then

       A11: ex mg be ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of G) st mg = the MorphMap of G & mg is "onto";

      G is injective by A2;

      then G is one-to-one;

      then

       A12: the ObjectMap of G is one-to-one;

      

       A13: (F * G) is bijective by A1, A2, Th12;

      then (F * G) is surjective;

      then (F * G) is full;

      then

       A14: ex mfg be ManySortedFunction of the Arrows of A, (the Arrows of C * the ObjectMap of (F * G)) st mfg = the MorphMap of (F * G) & mfg is "onto";

      

       A15: MFG is "1-1" by A13, Th5;

      

       A16: the MorphMap of ((F * G) " ) = the MorphMap of (GI * FI)

      proof

        consider f be ManySortedFunction of the Arrows of A, (the Arrows of C * the ObjectMap of (F * G)) such that

         A17: f = the MorphMap of (F * G) and

         A18: the MorphMap of ((F * G) " ) = ((f "" ) * (the ObjectMap of (F * G) " )) by A13, FUNCTOR0:def 38;

        

         A19: ( rng the ObjectMap of G) = CB by A10, FUNCT_2:def 3;

        for i be object st i in CC holds (((f "" ) * (the ObjectMap of (F * G) " )) . i) = (((the MorphMap of (G " ) * the ObjectMap of (F " )) ** the MorphMap of (F " )) . i)

        proof

          

           A20: (ex x1 be ManySortedFunction of the Arrows of B, (the Arrows of C * the ObjectMap of F) st x1 = the MorphMap of F & the MorphMap of (F " ) = ((x1 "" ) * (the ObjectMap of F " ))) & ex x1 be ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of G) st x1 = the MorphMap of G & the MorphMap of (G " ) = ((x1 "" ) * (the ObjectMap of G " )) by A1, A2, FUNCTOR0:def 38;

          

           A21: (OF " ) = the ObjectMap of (F " ) & ( dom ((((MG "" ) * OGI) * OFI) ** ((MF "" ) * OFI))) = CC by A1, FUNCTOR0:def 38, PARTFUN1:def 2;

          

           A22: (OG * (OG " )) = ( id CB) by A12, A19, FUNCT_2: 29;

          

           A23: (OFG " ) = ((OF * OG) " ) by FUNCTOR0:def 36

          .= ((OG " ) * (OF " )) by A8, A12, FUNCT_1: 44;

          let i be object such that

           A24: i in CC;

          

           A25: (((MF . (OG . (((OG " ) * (OF " )) . i))) * (MG . ((OFG " ) . i))) " ) = (((MF . (OG . (OGI . (OFI . i)))) * (MG . ((OFG " ) . i))) " ) by A24, FUNCT_2: 15

          .= (((MF . ((OG * OGI) . (OFI . i))) * (MG . ((OFG " ) . i))) " ) by A24, FUNCT_2: 5, FUNCT_2: 15

          .= (((MF . ((( id CB) * OFI) . i)) * (MG . ((OFG " ) . i))) " ) by A24, A22, FUNCT_2: 15

          .= (((MF . ((OF " ) . i)) * (MG . ((OGI * OFI) . i))) " ) by A23, FUNCT_2: 17;

          (OFG " ) is Function of CC, CA by A13, Th2, Th5;

          then

           A26: ( dom ((MF * OG) ** MG)) = CA & ((OFG " ) . i) in CA by A24, FUNCT_2: 5, PARTFUN1:def 2;

          

           A27: (the ObjectMap of (F * G) " ) is Function of CC, CA by A13, Th2, Th5;

          then

           A28: ((the ObjectMap of (F * G) " ) . i) in CA by A24, FUNCT_2: 5;

          i in ( dom (the ObjectMap of (F * G) " )) by A24, A27, FUNCT_2:def 1;

          

          then

           A29: (((f "" ) * (the ObjectMap of (F * G) " )) . i) = ((MFG "" ) . ((the ObjectMap of (F * G) " ) . i)) by A17, FUNCT_1: 13

          .= ((MFG . ((the ObjectMap of (F * G) " ) . i)) " ) by A14, A15, A28, MSUALG_3:def 4

          .= ((((MF * OG) ** MG) . ((OFG " ) . i)) " ) by FUNCTOR0:def 36

          .= ((((MF * OG) . ((OFG " ) . i)) * (MG . ((OFG " ) . i))) " ) by A26, PBOOLE:def 19

          .= (((MF . (OG . (((OG " ) * (OF " )) . i))) * (MG . ((OFG " ) . i))) " ) by A24, A27, A23, FUNCT_2: 5, FUNCT_2: 15;

          

           A30: (OFI . i) in CB by A24, FUNCT_2: 5;

          then

           A31: (MF . (OFI . i)) is one-to-one by A5, MSUALG_3: 1;

          

           A32: (OGI . (OFI . i)) in CA by A30, FUNCT_2: 5;

          then

           A33: (MG . (OGI . (OFI . i))) is one-to-one by A6, MSUALG_3: 1;

          (((MF . ((OF " ) . i)) * (MG . ((OGI * OFI) . i))) " ) = (((MF . ((OF " ) . i)) * (MG . (OGI . (OFI . i)))) " ) by A24, FUNCT_2: 15

          .= (((MG . (OGI . (OFI . i))) " ) * ((MF . (OFI . i)) " )) by A33, A31, FUNCT_1: 44

          .= (((MG "" ) . (OGI . (OFI . i))) * ((MF . ((OF " ) . i)) " )) by A11, A6, A32, MSUALG_3:def 4

          .= ((((MG "" ) * OGI) . (OFI . i)) * ((MF . ((OF " ) . i)) " )) by A24, FUNCT_2: 5, FUNCT_2: 15

          .= (((((MG "" ) * OGI) * OFI) . i) * ((MF . (OFI . i)) " )) by A24, FUNCT_2: 15

          .= (((((MG "" ) * OGI) * OFI) . i) * ((MF "" ) . (OFI . i))) by A5, A7, A30, MSUALG_3:def 4

          .= (((((MG "" ) * OGI) * OFI) . i) * (((MF "" ) * OFI) . i)) by A24, FUNCT_2: 15;

          hence thesis by A20, A24, A21, A29, A25, PBOOLE:def 19;

        end;

        

        then the MorphMap of ((F * G) " ) = ((the MorphMap of GI * the ObjectMap of FI) ** the MorphMap of FI) by A3, A4, A18

        .= the MorphMap of (GI * FI) by FUNCTOR0:def 36;

        hence thesis;

      end;

      the ObjectMap of ((F * G) " ) = (the ObjectMap of (F * G) " ) by A13, FUNCTOR0:def 38

      .= ((the ObjectMap of F * the ObjectMap of G) " ) by FUNCTOR0:def 36

      .= ((the ObjectMap of G " ) * (the ObjectMap of F " )) by A8, A12, FUNCT_1: 44

      .= (the ObjectMap of GI * (the ObjectMap of F " )) by A2, A3, FUNCTOR0:def 38

      .= (the ObjectMap of GI * the ObjectMap of FI) by A1, A4, FUNCTOR0:def 38

      .= the ObjectMap of (GI * FI) by FUNCTOR0:def 36;

      hence thesis by A16;

    end;