functor0.miz



    begin

    scheme :: FUNCTOR0:sch1

    ValOnPair { X() -> non empty set , f() -> Function , x1,x2() -> Element of X() , F( object, object) -> set , P[ object, object] } :

(f() . (x1(),x2())) = F(x1,x2)

      provided

       A1: f() = { [ [o, o9], F(o,o9)] where o be Element of X(), o9 be Element of X() : P[o, o9] }

       and

       A2: P[x1(), x2()];

      defpred R[ set] means P[($1 `1 ), ($1 `2 )];

      deffunc G( set) = F(`1,`2);

      

       A3: f() = { [o, G(o)] where o be Element of [:X(), X():] : R[o] }

      proof

        thus f() c= { [o, F(`1,`2)] where o be Element of [:X(), X():] : P[(o `1 ), (o `2 )] }

        proof

          let y be object;

          assume y in f();

          then

          consider o1,o2 be Element of X() such that

           A4: y = [ [o1, o2], F(o1,o2)] and

           A5: P[o1, o2] by A1;

          reconsider p = [o1, o2] as Element of [:X(), X():] by ZFMISC_1: 87;

          

           A6: (p `1 ) = o1;

          (p `2 ) = o2;

          hence thesis by A4, A5, A6;

        end;

        let y be object;

        assume y in { [o, F(`1,`2)] where o be Element of [:X(), X():] : P[(o `1 ), (o `2 )] };

        then

        consider o be Element of [:X(), X():] such that

         A7: y = [o, F(`1,`2)] and

         A8: P[(o `1 ), (o `2 )];

        reconsider o1 = (o `1 ), o2 = (o `2 ) as Element of X() by MCART_1: 10;

        o = [o1, o2] by MCART_1: 21;

        hence thesis by A1, A7, A8;

      end;

      reconsider x = [x1(), x2()] as Element of [:X(), X():] by ZFMISC_1: 87;

      

       A9: R[x] by A2;

      

      thus (f() . (x1(),x2())) = (f() . x)

      .= G(x) from ALTCAT_2:sch 3( A3, A9)

      .= F(x1,x2);

    end;

    theorem :: FUNCTOR0:1

    

     Th1: for A be set holds {} is Function of A, {} by FUNCT_2: 130;

    theorem :: FUNCTOR0:2

    

     Th2: for I be set holds for M be ManySortedSet of I holds (M * ( id I)) = M

    proof

      let I be set;

      let M be ManySortedSet of I;

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

      hence thesis by RELAT_1: 52;

    end;

    registration

      let f be empty Function;

      cluster ( ~ f) -> empty;

      coherence ;

      let g be Function;

      cluster [:f, g:] -> empty;

      coherence

      proof

        ( dom f) = {} ;

        then ( dom [:f, g:]) = [: {} , ( dom g):] by FUNCT_3:def 8;

        hence thesis;

      end;

      cluster [:g, f:] -> empty;

      coherence

      proof

        ( dom f) = {} ;

        then ( dom [:g, f:]) = [:( dom g), {} :] by FUNCT_3:def 8;

        hence thesis;

      end;

    end

    theorem :: FUNCTOR0:3

    

     Th3: for A be set, f be Function holds (f .: ( id A)) = (( ~ f) .: ( id A))

    proof

      let A be set, f be Function;

      thus (f .: ( id A)) c= (( ~ f) .: ( id A))

      proof

        let y be object;

        assume y in (f .: ( id A));

        then

        consider x be object such that

         A1: x in ( dom f) and

         A2: x in ( id A) and

         A3: y = (f . x) by FUNCT_1:def 6;

        consider x1,x2 be object such that

         A4: x = [x1, x2] by A2, RELAT_1:def 1;

        

         A5: x1 = x2 by A2, A4, RELAT_1:def 10;

        then

         A6: x in ( dom ( ~ f)) by A1, A4, FUNCT_4: 42;

        then (f . (x1,x2)) = (( ~ f) . (x1,x2)) by A4, A5, FUNCT_4: 43;

        hence thesis by A2, A3, A4, A6, FUNCT_1:def 6;

      end;

      let y be object;

      assume y in (( ~ f) .: ( id A));

      then

      consider x be object such that

       A7: x in ( dom ( ~ f)) and

       A8: x in ( id A) and

       A9: y = (( ~ f) . x) by FUNCT_1:def 6;

      consider x1,x2 be object such that

       A10: x = [x1, x2] by A8, RELAT_1:def 1;

      

       A11: x1 = x2 by A8, A10, RELAT_1:def 10;

      then

       A12: x in ( dom f) by A7, A10, FUNCT_4: 42;

      then (( ~ f) . (x1,x2)) = (f . (x1,x2)) by A10, A11, FUNCT_4:def 2;

      hence thesis by A8, A9, A10, A12, FUNCT_1:def 6;

    end;

    theorem :: FUNCTOR0:4

    

     Th4: for X,Y be set, f be Function of X, Y holds f is onto iff [:f, f:] is onto

    proof

      let X,Y be set, f be Function of X, Y;

      ( rng [:f, f:]) = [:( rng f), ( rng f):] by FUNCT_3: 67;

      then ( rng f) = Y iff ( rng [:f, f:]) = [:Y, Y:] by ZFMISC_1: 92;

      hence thesis;

    end;

    registration

      let f be Function-yielding Function;

      cluster ( ~ f) -> Function-yielding;

      coherence ;

    end

    theorem :: FUNCTOR0:5

    

     Th5: for A,B be set, a be object holds ( ~ ( [:A, B:] --> a)) = ( [:B, A:] --> a)

    proof

      let A,B be set, a be object;

       A1:

      now

        let x be object;

        hereby

          assume x in ( dom ( [:B, A:] --> a));

          then

          consider z,y be object such that

           A2: z in B and

           A3: y in A and

           A4: x = [z, y] by ZFMISC_1:def 2;

          take y, z;

          thus x = [z, y] by A4;

           [y, z] in [:A, B:] by A2, A3, ZFMISC_1: 87;

          hence [y, z] in ( dom ( [:A, B:] --> a));

        end;

        given y,z be object such that

         A5: x = [z, y] and

         A6: [y, z] in ( dom ( [:A, B:] --> a));

        

         A7: y in A by A6, ZFMISC_1: 87;

        z in B by A6, ZFMISC_1: 87;

        then x in [:B, A:] by A5, A7, ZFMISC_1: 87;

        hence x in ( dom ( [:B, A:] --> a));

      end;

      now

        let y,z be object;

        assume

         A8: [y, z] in ( dom ( [:A, B:] --> a));

        then

         A9: y in A by ZFMISC_1: 87;

        z in B by A8, ZFMISC_1: 87;

        

        hence (( [:B, A:] --> a) . (z,y)) = a by A9, FUNCOP_1: 7, ZFMISC_1: 87

        .= (( [:A, B:] --> a) . (y,z)) by A8, FUNCOP_1: 7;

      end;

      hence thesis by A1, FUNCT_4:def 2;

    end;

    theorem :: FUNCTOR0:6

    

     Th6: for f,g be Function st f is one-to-one & g is one-to-one holds ( [:f, g:] " ) = [:(f " ), (g " ):]

    proof

      let f,g be Function;

      assume that

       A1: f is one-to-one and

       A2: g is one-to-one;

      

       A3: [:f, g:] is one-to-one by A1, A2;

      

       A4: ( dom (f " )) = ( rng f) by A1, FUNCT_1: 33;

      

       A5: ( dom (g " )) = ( rng g) by A2, FUNCT_1: 33;

      

       A6: ( dom ( [:f, g:] " )) = ( rng [:f, g:]) by A3, FUNCT_1: 33

      .= [:( dom (f " )), ( dom (g " )):] by A4, A5, FUNCT_3: 67;

      for x,y be object st x in ( dom (f " )) & y in ( dom (g " )) holds (( [:f, g:] " ) . (x,y)) = [((f " ) . x), ((g " ) . y)]

      proof

        let x,y be object such that

         A7: x in ( dom (f " )) and

         A8: y in ( dom (g " ));

        

         A9: ( dom [:f, g:]) = [:( dom f), ( dom g):] by FUNCT_3:def 8;

        

         A10: ((f " ) . x) in ( rng (f " )) by A7, FUNCT_1:def 3;

        

         A11: ((g " ) . y) in ( rng (g " )) by A8, FUNCT_1:def 3;

        

         A12: ((f " ) . x) in ( dom f) by A1, A10, FUNCT_1: 33;

        ((g " ) . y) in ( dom g) by A2, A11, FUNCT_1: 33;

        then

         A13: [((f " ) . x), ((g " ) . y)] in ( dom [:f, g:]) by A9, A12, ZFMISC_1: 87;

        

         A14: (f . ((f " ) . x)) = ((f * (f " )) . x) by A7, FUNCT_1: 13

        .= ((((f " ) " ) * (f " )) . x) by A1, FUNCT_1: 43

        .= (( id ( dom (f " ))) . x) by A1, FUNCT_1: 39

        .= x by A7, FUNCT_1: 18;

        (g . ((g " ) . y)) = ((g * (g " )) . y) by A8, FUNCT_1: 13

        .= ((((g " ) " ) * (g " )) . y) by A2, FUNCT_1: 43

        .= (( id ( dom (g " ))) . y) by A2, FUNCT_1: 39

        .= y by A8, FUNCT_1: 18;

        then ( [:f, g:] . (((f " ) . x),((g " ) . y))) = [x, y] by A9, A13, A14, FUNCT_3: 65;

        hence thesis by A1, A2, A13, FUNCT_1: 32;

      end;

      hence thesis by A6, FUNCT_3:def 8;

    end;

    theorem :: FUNCTOR0:7

    

     Th7: for f be Function st [:f, f:] is one-to-one holds f is one-to-one

    proof

      let f be Function such that

       A1: [:f, f:] is one-to-one;

      let x1,x2 be object such that

       A2: x1 in ( dom f) and

       A3: x2 in ( dom f) and

       A4: (f . x1) = (f . x2);

      

       A5: ( dom [:f, f:]) = [:( dom f), ( dom f):] by FUNCT_3:def 8;

      then

       A6: [x1, x1] in ( dom [:f, f:]) by A2, ZFMISC_1: 87;

      

       A7: [x2, x2] in ( dom [:f, f:]) by A3, A5, ZFMISC_1: 87;

      ( [:f, f:] . (x1,x1)) = [(f . x2), (f . x2)] by A4, A5, A6, FUNCT_3: 65

      .= ( [:f, f:] . (x2,x2)) by A5, A7, FUNCT_3: 65;

      then [x1, x1] = [x2, x2] by A1, A6, A7;

      hence thesis by XTUPLE_0: 1;

    end;

    theorem :: FUNCTOR0:8

    

     Th8: for f be Function st f is one-to-one holds ( ~ f) is one-to-one

    proof

      let f be Function such that

       A1: f is one-to-one;

      let x1,x2 be object;

      consider X,Y be set such that

       A2: ( dom ( ~ f)) c= [:X, Y:] by FUNCT_4: 44;

      assume

       A3: x1 in ( dom ( ~ f));

      then

      consider x11,x12 be object such that x11 in X and x12 in Y and

       A4: x1 = [x11, x12] by A2, ZFMISC_1: 84;

      assume

       A5: x2 in ( dom ( ~ f));

      then

      consider x21,x22 be object such that x21 in X and x22 in Y and

       A6: x2 = [x21, x22] by A2, ZFMISC_1: 84;

      assume

       A7: (( ~ f) . x1) = (( ~ f) . x2);

      

       A8: [x12, x11] in ( dom f) by A3, A4, FUNCT_4: 42;

      

       A9: [x22, x21] in ( dom f) by A5, A6, FUNCT_4: 42;

      (f . (x12,x11)) = (( ~ f) . (x11,x12)) by A3, A4, FUNCT_4: 43

      .= (( ~ f) . (x21,x22)) by A4, A6, A7

      .= (f . (x22,x21)) by A5, A6, FUNCT_4: 43;

      then

       A10: [x12, x11] = [x22, x21] by A1, A8, A9;

      then x12 = x22 by XTUPLE_0: 1;

      hence thesis by A4, A6, A10, XTUPLE_0: 1;

    end;

    theorem :: FUNCTOR0:9

    

     Th9: for f,g be Function st ( ~ [:f, g:]) is one-to-one holds [:g, f:] is one-to-one

    proof

      let f,g be Function such that

       A1: ( ~ [:f, g:]) is one-to-one;

      let x1,x2 be object;

      

       A2: ( dom [:g, f:]) = [:( dom g), ( dom f):] by FUNCT_3:def 8;

      

       A3: ( dom [:f, g:]) = [:( dom f), ( dom g):] by FUNCT_3:def 8;

      assume x1 in ( dom [:g, f:]);

      then

      consider x11,x12 be object such that

       A4: x11 in ( dom g) and

       A5: x12 in ( dom f) and

       A6: x1 = [x11, x12] by A2, ZFMISC_1: 84;

      assume x2 in ( dom [:g, f:]);

      then

      consider x21,x22 be object such that

       A7: x21 in ( dom g) and

       A8: x22 in ( dom f) and

       A9: x2 = [x21, x22] by A2, ZFMISC_1: 84;

      x1 in ( dom [:g, f:]) by A2, A4, A5, A6, ZFMISC_1: 87;

      then

       A10: x1 in ( dom ( ~ [:f, g:])) by A2, A3, FUNCT_4: 46;

      x2 in ( dom [:g, f:]) by A2, A7, A8, A9, ZFMISC_1: 87;

      then

       A11: x2 in ( dom ( ~ [:f, g:])) by A2, A3, FUNCT_4: 46;

      assume

       A12: ( [:g, f:] . x1) = ( [:g, f:] . x2);

      

       A13: ( [:g, f:] . (x11,x12)) = [(g . x11), (f . x12)] by A4, A5, FUNCT_3:def 8;

      

       A14: ( [:g, f:] . (x21,x22)) = [(g . x21), (f . x22)] by A7, A8, FUNCT_3:def 8;

      then

       A15: (f . x22) = (f . x12) by A6, A9, A12, A13, XTUPLE_0: 1;

      

       A16: (g . x11) = (g . x21) by A6, A9, A12, A13, A14, XTUPLE_0: 1;

      (( ~ [:f, g:]) . [x11, x12]) = (( ~ [:f, g:]) . (x11,x12))

      .= ( [:f, g:] . (x12,x11)) by A6, A10, FUNCT_4: 43

      .= [(f . x22), (g . x21)] by A4, A5, A15, A16, FUNCT_3:def 8

      .= ( [:f, g:] . (x22,x21)) by A7, A8, FUNCT_3:def 8

      .= (( ~ [:f, g:]) . (x21,x22)) by A9, A11, FUNCT_4: 43

      .= (( ~ [:f, g:]) . [x21, x22]);

      hence thesis by A1, A6, A9, A10, A11;

    end;

    theorem :: FUNCTOR0:10

    

     Th10: for f,g be Function st f is one-to-one & g is one-to-one holds (( ~ [:f, g:]) " ) = ( ~ ( [:g, f:] " ))

    proof

      let f,g be Function such that

       A1: f is one-to-one and

       A2: g is one-to-one;

      

       A3: ( [:g, f:] " ) = [:(g " ), (f " ):] by A1, A2, Th6;

      then

       A4: ( dom ( [:g, f:] " )) = [:( dom (g " )), ( dom (f " )):] by FUNCT_3:def 8;

      

       A5: ( dom [:f, g:]) = [:( dom f), ( dom g):] by FUNCT_3:def 8;

      

       A6: ( dom [:g, f:]) = [:( dom g), ( dom f):] by FUNCT_3:def 8;

      

       A7: [:g, f:] is one-to-one by A1, A2;

      

       A8: ( ~ [:f, g:]) is one-to-one by Th8, A1, A2;

      

       A9: ( [:f, g:] " ) = [:(f " ), (g " ):] by A1, A2, Th6;

      

       A10: ( dom ( ~ ( [:g, f:] " ))) = [:( dom (f " )), ( dom (g " )):] by A4, FUNCT_4: 46

      .= ( dom [:(f " ), (g " ):]) by FUNCT_3:def 8

      .= ( rng [:f, g:]) by A1, A2, A9, FUNCT_1: 32

      .= ( rng ( ~ [:f, g:])) by A5, FUNCT_4: 47;

      now

        let y,x be object;

        hereby

          assume that

           A11: y in ( rng ( ~ [:f, g:])) and

           A12: x = (( ~ ( [:g, f:] " )) . y);

          y in ( rng [:f, g:]) by A5, A11, FUNCT_4: 47;

          then y in [:( rng f), ( rng g):] by FUNCT_3: 67;

          then

          consider y1,y2 be object such that

           A13: y1 in ( rng f) and

           A14: y2 in ( rng g) and

           A15: y = [y1, y2] by ZFMISC_1: 84;

          set x1 = ((f " ) . y1), x2 = ((g " ) . y2);

          

           A16: y2 in ( dom (g " )) by A2, A14, FUNCT_1: 32;

          

           A17: y1 in ( dom (f " )) by A1, A13, FUNCT_1: 32;

          then [y2, y1] in ( dom ( [:g, f:] " )) by A4, A16, ZFMISC_1: 87;

          

          then

           A18: (( ~ ( [:g, f:] " )) . (y1,y2)) = ( [:(g " ), (f " ):] . (y2,y1)) by A3, FUNCT_4:def 2

          .= [x2, x1] by A16, A17, FUNCT_3:def 8;

          

           A19: y1 in ( dom (f " )) by A1, A13, FUNCT_1: 32;

          

           A20: y2 in ( dom (g " )) by A2, A14, FUNCT_1: 32;

          

           A21: x1 in ( rng (f " )) by A19, FUNCT_1:def 3;

          

           A22: x2 in ( rng (g " )) by A20, FUNCT_1:def 3;

          

           A23: x1 in ( dom f) by A1, A21, FUNCT_1: 33;

          

           A24: x2 in ( dom g) by A2, A22, FUNCT_1: 33;

          then

           A25: [x2, x1] in ( dom [:g, f:]) by A6, A23, ZFMISC_1: 87;

          then

           A26: [x2, x1] in ( dom ( ~ [:f, g:])) by A5, A6, FUNCT_4: 46;

          thus x in ( dom ( ~ [:f, g:])) by A5, A6, A12, A15, A18, A25, FUNCT_4: 46;

          

           A27: (f . x1) = y1 by A1, A13, FUNCT_1: 32;

          

           A28: (g . x2) = y2 by A2, A14, FUNCT_1: 32;

          

          thus (( ~ [:f, g:]) . x) = (( ~ [:f, g:]) . (x2,x1)) by A12, A15, A18

          .= ( [:f, g:] . (x1,x2)) by A26, FUNCT_4: 43

          .= y by A15, A23, A24, A27, A28, FUNCT_3:def 8;

        end;

        assume that

         A29: x in ( dom ( ~ [:f, g:])) and

         A30: (( ~ [:f, g:]) . x) = y;

        thus y in ( rng ( ~ [:f, g:])) by A29, A30, FUNCT_1:def 3;

        x in ( dom [:g, f:]) by A5, A6, A29, FUNCT_4: 46;

        then

        consider x1,x2 be object such that

         A31: x1 in ( dom g) and

         A32: x2 in ( dom f) and

         A33: x = [x1, x2] by A6, ZFMISC_1: 84;

        

         A34: (( ~ [:f, g:]) . (x1,x2)) = ( [:f, g:] . (x2,x1)) by A29, A33, FUNCT_4: 43

        .= [(f . x2), (g . x1)] by A31, A32, FUNCT_3:def 8;

        

         A35: (g . x1) in ( rng g) by A31, FUNCT_1:def 3;

        (f . x2) in ( rng f) by A32, FUNCT_1:def 3;

        then [(g . x1), (f . x2)] in [:( rng g), ( rng f):] by A35, ZFMISC_1: 87;

        then [(g . x1), (f . x2)] in ( rng [:g, f:]) by FUNCT_3: 67;

        then

         A36: [(g . x1), (f . x2)] in ( dom ( [:g, f:] " )) by A7, FUNCT_1: 33;

         [x1, x2] in ( dom [:g, f:]) by A6, A31, A32, ZFMISC_1: 87;

        

        hence x = (( [:g, f:] " ) . ( [:g, f:] . (x1,x2))) by A1, A2, A33, FUNCT_1: 34

        .= (( [:g, f:] " ) . ((g . x1),(f . x2))) by A31, A32, FUNCT_3:def 8

        .= (( ~ ( [:g, f:] " )) . ((f . x2),(g . x1))) by A36, FUNCT_4:def 2

        .= (( ~ ( [:g, f:] " )) . y) by A30, A33, A34;

      end;

      hence thesis by A8, A10, FUNCT_1: 32;

    end;

    theorem :: FUNCTOR0:11

    

     Th11: for A,B be set, f be Function of A, B st f is onto holds ( id B) c= ( [:f, f:] .: ( id A))

    proof

      let A,B be set, f be Function of A, B;

      assume f is onto;

      then

       A1: ( rng f) = B;

      let xx be object;

      assume

       A2: xx in ( id B);

      then

      consider x,x9 be object such that

       A3: xx = [x, x9] by RELAT_1:def 1;

      

       A4: x = x9 by A2, A3, RELAT_1:def 10;

      

       A5: x in B by A2, A3, RELAT_1:def 10;

      then

      consider y be object such that

       A6: y in A and

       A7: (f . y) = x by A1, FUNCT_2: 11;

      

       A8: ( dom f) = A by A5, FUNCT_2:def 1;

      

       A9: [y, y] in ( id A) by A6, RELAT_1:def 10;

      ( [:f, f:] . (y,y)) = xx by A3, A4, A6, A7, A8, FUNCT_3:def 8;

      hence thesis by A2, A9, FUNCT_2: 35;

    end;

    theorem :: FUNCTOR0:12

    

     Th12: for F,G be Function-yielding Function, f be Function holds ((G ** F) * f) = ((G * f) ** (F * f))

    proof

      let F,G be Function-yielding Function, f be Function;

      

       A1: ( dom ((G ** F) * f)) = (f " ( dom (G ** F))) by RELAT_1: 147

      .= (f " (( dom G) /\ ( dom F))) by PBOOLE:def 19

      .= ((f " ( dom F)) /\ (f " ( dom G))) by FUNCT_1: 68

      .= ((f " ( dom F)) /\ ( dom (G * f))) by RELAT_1: 147

      .= (( dom (F * f)) /\ ( dom (G * f))) by RELAT_1: 147;

      now

        let i be object;

        assume

         A2: i in ( dom ((G ** F) * f));

        then

         A3: i in ( dom f) by FUNCT_1: 11;

        

         A4: (f . i) in ( dom (G ** F)) by A2, FUNCT_1: 11;

        

        thus (((G ** F) * f) . i) = ((G ** F) . (f . i)) by A2, FUNCT_1: 12

        .= ((G . (f . i)) * (F . (f . i))) by A4, PBOOLE:def 19

        .= (((G * f) . i) * (F . (f . i))) by A3, FUNCT_1: 13

        .= (((G * f) . i) * ((F * f) . i)) by A3, FUNCT_1: 13;

      end;

      hence thesis by A1, PBOOLE:def 19;

    end;

    theorem :: FUNCTOR0:13

    

     Th13: for A,B,C be set, f be Function of [:A, B:], C st ( ~ f) is onto holds f is onto

    proof

      let A,B,C be set, f be Function of [:A, B:], C;

      

       A1: ( rng ( ~ f)) c= ( rng f) by FUNCT_4: 41;

      assume ( ~ f) is onto;

      then ( rng ( ~ f)) = C;

      hence ( rng f) = C by A1;

    end;

    theorem :: FUNCTOR0:14

    

     Th14: for A be set, B be non empty set, f be Function of A, B holds ( [:f, f:] .: ( id A)) c= ( id B)

    proof

      let A be set, B be non empty set, f be Function of A, B;

      let x be object;

      assume x in ( [:f, f:] .: ( id A));

      then

      consider yy be object such that

       A1: yy in [:A, A:] and

       A2: yy in ( id A) and

       A3: ( [:f, f:] . yy) = x by FUNCT_2: 64;

      consider y,y9 be object such that

       A4: y in A and y9 in A and

       A5: yy = [y, y9] by A1, ZFMISC_1: 84;

      

       A6: y = y9 by A2, A5, RELAT_1:def 10;

      reconsider y as Element of A by A4;

      

       A7: (f . y) in B by A4, FUNCT_2: 5;

      

       A8: y in ( dom f) by A4, FUNCT_2:def 1;

      x = ( [:f, f:] . (y,y9)) by A3, A5

      .= [(f . y), (f . y)] by A6, A8, FUNCT_3:def 8;

      hence thesis by A7, RELAT_1:def 10;

    end;

    begin

    definition

      let A,B be set;

      mode bifunction of A,B is Function of [:A, A:], [:B, B:];

    end

    definition

      let A,B be set, f be bifunction of A, B;

      :: FUNCTOR0:def1

      attr f is Covariant means

      : Def1: ex g be Function of A, B st f = [:g, g:];

      :: FUNCTOR0:def2

      attr f is Contravariant means

      : Def2: ex g be Function of A, B st f = ( ~ [:g, g:]);

    end

    theorem :: FUNCTOR0:15

    

     Th15: for A be set, B be non empty set, b be Element of B, f be bifunction of A, B st f = ( [:A, A:] --> [b, b]) holds f is Covariant Contravariant

    proof

      let A be set, B be non empty set, b be Element of B, f be bifunction of A, B such that

       A1: f = ( [:A, A:] --> [b, b]);

      reconsider g = (A --> b) as Function of A, B;

      thus f is Covariant

      proof

        take g;

        thus thesis by A1, ALTCAT_2: 1;

      end;

      take g;

      ( [:A, A:] --> [b, b]) = ( ~ ( [:A, A:] --> [b, b])) by Th5;

      hence thesis by A1, ALTCAT_2: 1;

    end;

    registration

      let A,B be set;

      cluster Covariant Contravariant for bifunction of A, B;

      existence

      proof

        per cases ;

          suppose

           A1: B = {} ;

          then [:B, B:] = {} by ZFMISC_1: 90;

          then

          reconsider f = {} as bifunction of A, B by Th1;

          take f;

          reconsider g = {} as Function of A, B by A1, Th1;

          reconsider h = g as empty Function;

          thus f is Covariant

          proof

            take g;

            

            thus f = [:h, h:]

            .= [:g, g:];

          end;

          take g;

          

          thus f = ( ~ [:h, h:])

          .= ( ~ [:g, g:]);

        end;

          suppose

           A2: B <> {} ;

          set b = the Element of B;

          set f = ( [:A, A:] --> [b, b]);

           [b, b] in [:B, B:] by A2, ZFMISC_1: 87;

          then

          reconsider f as bifunction of A, B by FUNCOP_1: 45;

          take f;

          thus thesis by A2, Th15;

        end;

      end;

    end

    theorem :: FUNCTOR0:16

    for A,B be non empty set holds for f be Covariant Contravariant bifunction of A, B holds ex b be Element of B st f = ( [:A, A:] --> [b, b])

    proof

      let A,B be non empty set;

      let f be Covariant Contravariant bifunction of A, B;

      consider g1 be Function of A, B such that

       A1: f = [:g1, g1:] by Def1;

      consider g2 be Function of A, B such that

       A2: f = ( ~ [:g2, g2:]) by Def2;

      set a = the Element of A;

      take b = (g1 . a);

      

       A3: ( dom f) = [:A, A:] by FUNCT_2:def 1;

      now

        let z be object;

        assume z in ( dom f);

        then

        consider a1,a2 be Element of A such that

         A4: z = [a1, a2] by DOMAIN_1: 1;

        

         A5: ( dom g2) = A by FUNCT_2:def 1;

        

         A6: ( dom g1) = A by FUNCT_2:def 1;

        

         A7: ( dom [:g2, g2:]) = [:( dom g2), ( dom g2):] by FUNCT_3:def 8;

        then

         A8: [a1, a] in ( dom [:g2, g2:]) by A5, ZFMISC_1: 87;

        

         A9: ( dom g2) = A by FUNCT_2:def 1;

         [b, (g1 . a1)] = (f . (a,a1)) by A1, A6, FUNCT_3:def 8

        .= ( [:g2, g2:] . (a1,a)) by A2, A8, FUNCT_4:def 2

        .= [(g2 . a1), (g2 . a)] by A9, FUNCT_3:def 8;

        then

         A10: (g2 . a1) = b by XTUPLE_0: 1;

        

         A11: [a2, a] in ( dom [:g2, g2:]) by A5, A7, ZFMISC_1: 87;

         [b, (g1 . a2)] = (f . (a,a2)) by A1, A6, FUNCT_3:def 8

        .= ( [:g2, g2:] . (a2,a)) by A2, A11, FUNCT_4:def 2

        .= [(g2 . a2), (g2 . a)] by A9, FUNCT_3:def 8;

        then

         A12: (g2 . a2) = b by XTUPLE_0: 1;

        

         A13: [a2, a1] in ( dom [:g2, g2:]) by A5, A7, ZFMISC_1: 87;

        

        thus (f . z) = ( [:g1, g1:] . (a1,a2)) by A1, A4

        .= ( [:g2, g2:] . (a2,a1)) by A1, A2, A13, FUNCT_4:def 2

        .= [b, b] by A9, A10, A12, FUNCT_3:def 8;

      end;

      hence thesis by A3, FUNCOP_1: 11;

    end;

    begin

    definition

      let I1,I2 be set, f be Function of I1, I2;

      let A be ManySortedSet of I1, B be ManySortedSet of I2;

      :: FUNCTOR0:def3

      mode MSUnTrans of f,A,B -> ManySortedSet of I1 means

      : Def3: ex I29 be non empty set, B9 be ManySortedSet of I29, f9 be Function of I1, I29 st f = f9 & B = B9 & it is ManySortedFunction of A, (B9 * f9) if I2 <> {}

      otherwise it = ( EmptyMS I1);

      existence

      proof

        hereby

          assume I2 <> {} ;

          then

          reconsider I29 = I2 as non empty set;

          reconsider f9 = f as Function of I1, I29;

          reconsider B9 = B as ManySortedSet of I29;

          set IT = the ManySortedFunction of A, (B9 * f9);

          reconsider IT9 = IT as ManySortedSet of I1;

          take IT9, I29;

          reconsider f9 = f as Function of I1, I29;

          reconsider B9 = B as ManySortedSet of I29;

          take B9, f9;

          thus f = f9 & B = B9;

          thus IT9 is ManySortedFunction of A, (B9 * f9);

        end;

        thus thesis;

      end;

      consistency ;

    end

    definition

      let I1 be set, I2 be non empty set, f be Function of I1, I2;

      let A be ManySortedSet of I1, B be ManySortedSet of I2;

      :: original: MSUnTrans

      redefine

      :: FUNCTOR0:def4

      mode MSUnTrans of f,A,B means

      : Def4: it is ManySortedFunction of A, (B * f);

      compatibility

      proof

        let M be ManySortedSet of I1;

        hereby

          assume M is MSUnTrans of f, A, B;

          then ex I29 be non empty set, B9 be ManySortedSet of I29, f9 be Function of I1, I29 st f = f9 & B = B9 & M is ManySortedFunction of A, (B9 * f9) by Def3;

          hence M is ManySortedFunction of A, (B * f);

        end;

        thus thesis by Def3;

      end;

    end

    registration

      let I1,I2 be set;

      let f be Function of I1, I2;

      let A be ManySortedSet of I1, B be ManySortedSet of I2;

      cluster -> Function-yielding for MSUnTrans of f, A, B;

      coherence

      proof

        let M be MSUnTrans of f, A, B;

        per cases ;

          suppose I2 <> {} ;

          then ex I29 be non empty set, B9 be ManySortedSet of I29, f9 be Function of I1, I29 st f = f9 & B = B9 & M is ManySortedFunction of A, (B9 * f9) by Def3;

          hence thesis;

        end;

          suppose I2 = {} ;

          then M = ( EmptyMS I1) by Def3;

          hence thesis;

        end;

      end;

    end

    theorem :: FUNCTOR0:17

    

     Th17: for I1 be set, I2,I3 be non empty set, f be Function of I1, I2, g be Function of I2, I3, B be ManySortedSet of I2, C be ManySortedSet of I3, G be MSUnTrans of g, B, C holds (G * f) is MSUnTrans of (g * f), (B * f), C

    proof

      let I1 be set, I2,I3 be non empty set, f be Function of I1, I2, g be Function of I2, I3, B be ManySortedSet of I2, C be ManySortedSet of I3, G be MSUnTrans of g, B, C;

      

       A1: (C * (g * f)) = ((C * g) * f) by RELAT_1: 36;

      G is ManySortedFunction of B, (C * g) by Def4;

      hence (G * f) is ManySortedFunction of (B * f), (C * (g * f)) by A1, ALTCAT_2: 5;

    end;

    definition

      let I1 be set, I2 be non empty set, f be Function of I1, I2, A be ManySortedSet of [:I1, I1:], B be ManySortedSet of [:I2, I2:], F be MSUnTrans of [:f, f:], A, B;

      :: original: ~

      redefine

      func ~ F -> MSUnTrans of [:f, f:], ( ~ A), ( ~ B) ;

      coherence

      proof

        reconsider G = F as ManySortedFunction of A, (B * [:f, f:]) by Def4;

        ( ~ G) is ManySortedFunction of ( ~ A), (( ~ B) * [:f, f:]) by ALTCAT_2: 3;

        hence ( ~ F) is MSUnTrans of [:f, f:], ( ~ A), ( ~ B) by Def4;

      end;

    end

    theorem :: FUNCTOR0:18

    

     Th18: for I1,I2 be non empty set, A be ManySortedSet of I1, B be ManySortedSet of I2, o be Element of I2 st (B . o) <> {} holds for m be Element of (B . o), f be Function of I1, I2 st f = (I1 --> o) holds the set of all [o9, ((A . o9) --> m)] where o9 be Element of I1 is MSUnTrans of f, A, B

    proof

      let I1,I2 be non empty set, A be ManySortedSet of I1, B be ManySortedSet of I2, o be Element of I2 such that

       A1: (B . o) <> {} ;

      let m be Element of (B . o), f be Function of I1, I2 such that

       A2: f = (I1 --> o);

      defpred P[ set] means not contradiction;

      deffunc F( set) = ((A . $1) --> m);

      reconsider Xm = { [o9, F(o9)] where o9 be Element of I1 : P[o9] } as Function from ALTCAT_2:sch 1;

      

       A3: Xm = { [o9, F(o9)] where o9 be Element of I1 : P[o9] };

      ( dom Xm) = { o9 where o9 be Element of I1 : P[o9] } from ALTCAT_2:sch 2( A3)

      .= I1 by DOMAIN_1: 18;

      then

      reconsider Xm as ManySortedSet of I1 by PARTFUN1:def 2, RELAT_1:def 18;

      deffunc F( set) = ((A . $1) --> m);

      

       A4: Xm = { [o9, F(o9)] where o9 be Element of I1 : P[o9] };

      now

        let i be object;

        assume

         A5: i in I1;

        then

        reconsider o9 = i as Element of I1;

        

         A6: P[o9];

        

         A7: i in ( dom f) by A2, A5;

        (f . i) = o by A2, A5, FUNCOP_1: 7;

        then m in (B . (f . i)) by A1;

        then

         A8: m in ((B * f) . i) by A7, FUNCT_1: 13;

        (Xm . o9) = F(o9) from ALTCAT_2:sch 3( A4, A6);

        hence (Xm . i) is Function of (A . i), ((B * f) . i) by A8, FUNCOP_1: 45;

      end;

      then Xm is ManySortedFunction of A, (B * f) by PBOOLE:def 15;

      hence thesis by Def4;

    end;

    theorem :: FUNCTOR0:19

    

     Th19: for I1 be set, I2,I3 be non empty set, f be Function of I1, I2, g be Function of I2, I3, A be ManySortedSet of I1, B be ManySortedSet of I2, C be ManySortedSet of I3, F be MSUnTrans of f, A, B, G be MSUnTrans of (g * f), (B * f), C st for ii be set st ii in I1 & ((B * f) . ii) = {} holds (A . ii) = {} or ((C * (g * f)) . ii) = {} holds (G ** F qua Function-yielding Function) is MSUnTrans of (g * f), A, C

    proof

      let I1 be set, I2,I3 be non empty set, f be Function of I1, I2, g be Function of I2, I3, A be ManySortedSet of I1, B be ManySortedSet of I2, C be ManySortedSet of I3, F be MSUnTrans of f, A, B, G be MSUnTrans of (g * f), (B * f), C such that

       A1: for ii be set st ii in I1 & ((B * f) . ii) = {} holds (A . ii) = {} or ((C * (g * f)) . ii) = {} ;

      reconsider G as ManySortedFunction of (B * f), (C * (g * f)) by Def4;

      reconsider F as ManySortedFunction of A, (B * f) by Def4;

      

       A2: ( dom G) = I1 by PARTFUN1:def 2;

      

       A3: ( dom F) = I1 by PARTFUN1:def 2;

      

       A4: ( dom (G ** F)) = (( dom G) /\ ( dom F)) by PBOOLE:def 19

      .= I1 by A2, A3;

      reconsider GF = (G ** F) as ManySortedSet of I1;

      GF is ManySortedFunction of A, (C * (g * f))

      proof

        let ii be object;

        assume

         A5: ii in I1;

        then

        reconsider Fi = (F . ii) as Function of (A . ii), ((B * f) . ii) by PBOOLE:def 15;

        reconsider Gi = (G . ii) as Function of ((B * f) . ii), ((C * (g * f)) . ii) by A5, PBOOLE:def 15;

        ((B * f) . ii) = {} implies (A . ii) = {} or ((C * (g * f)) . ii) = {} by A1, A5;

        then (Gi * Fi) is Function of (A . ii), ((C * (g * f)) . ii) by FUNCT_2: 13;

        hence thesis by A4, A5, PBOOLE:def 19;

      end;

      hence thesis by Def4;

    end;

    begin

    definition

      let C1,C2 be 1-sorted;

      struct BimapStr over C1,C2 (# the ObjectMap -> bifunction of the carrier of C1, the carrier of C2 #)

       attr strict strict;

    end

    definition

      let C1,C2 be non empty AltGraph;

      let F be BimapStr over C1, C2;

      let o be Object of C1;

      :: FUNCTOR0:def5

      func F . o -> Object of C2 equals ((the ObjectMap of F . (o,o)) `1 );

      coherence by MCART_1: 10;

    end

    definition

      let A,B be 1-sorted, F be BimapStr over A, B;

      :: FUNCTOR0:def6

      attr F is one-to-one means the ObjectMap of F is one-to-one;

      :: FUNCTOR0:def7

      attr F is onto means the ObjectMap of F is onto;

      :: FUNCTOR0:def8

      attr F is reflexive means (the ObjectMap of F .: ( id the carrier of A)) c= ( id the carrier of B);

      :: FUNCTOR0:def9

      attr F is coreflexive means ( id the carrier of B) c= (the ObjectMap of F .: ( id the carrier of A));

    end

    definition

      let A,B be non empty AltGraph, F be BimapStr over A, B;

      :: original: reflexive

      redefine

      :: FUNCTOR0:def10

      attr F is reflexive means

      : Def10: for o be Object of A holds (the ObjectMap of F . (o,o)) = [(F . o), (F . o)];

      compatibility

      proof

        hereby

          assume F is reflexive;

          then

           A1: (the ObjectMap of F .: ( id the carrier of A)) c= ( id the carrier of B);

          let o be Object of A;

           [o, o] in ( id the carrier of A) by RELAT_1:def 10;

          then

           A2: (the ObjectMap of F . (o,o)) in (the ObjectMap of F .: ( id the carrier of A)) by FUNCT_2: 35;

          consider p,p9 be object such that

           A3: (the ObjectMap of F . (o,o)) = [p, p9] by RELAT_1:def 1;

          thus (the ObjectMap of F . (o,o)) = [(F . o), (F . o)] by A1, A2, A3, RELAT_1:def 10;

        end;

        assume

         A4: for o be Object of A holds (the ObjectMap of F . (o,o)) = [(F . o), (F . o)];

        let x be object;

        assume x in (the ObjectMap of F .: ( id the carrier of A));

        then

        consider y be object such that

         A5: y in [:the carrier of A, the carrier of A:] and

         A6: y in ( id the carrier of A) and

         A7: x = (the ObjectMap of F . y) by FUNCT_2: 64;

        consider o,o9 be Element of A such that

         A8: y = [o, o9] by A5, DOMAIN_1: 1;

        reconsider o as Object of A;

        o = o9 by A6, A8, RELAT_1:def 10;

        then x = [(F . o), (F . o)] by A4, A7, A8;

        hence thesis by RELAT_1:def 10;

      end;

    end

    theorem :: FUNCTOR0:20

    

     Th20: for A,B be reflexive non empty AltGraph, F be BimapStr over A, B st F is coreflexive holds for o be Object of B holds ex o9 be Object of A st (F . o9) = o

    proof

      let A,B be reflexive non empty AltGraph, F be BimapStr over A, B;

      assume F is coreflexive;

      then

       A1: ( id the carrier of B) c= (the ObjectMap of F .: ( id the carrier of A));

      let o be Object of B;

      reconsider oo = [o, o] as Element of [:the carrier of B, the carrier of B:] by ZFMISC_1: 87;

       [o, o] in ( id the carrier of B) by RELAT_1:def 10;

      then

      consider pp be Element of [:the carrier of A, the carrier of A:] such that

       A2: pp in ( id the carrier of A) and

       A3: (the ObjectMap of F . pp) = oo by A1, FUNCT_2: 65;

      consider p,p9 be object such that

       A4: pp = [p, p9] by RELAT_1:def 1;

      

       A5: p = p9 by A2, A4, RELAT_1:def 10;

      reconsider p as Object of A by A2, A4, RELAT_1:def 10;

      take p;

      thus thesis by A3, A4, A5;

    end;

    definition

      let C1,C2 be non empty AltGraph;

      let F be BimapStr over C1, C2;

      :: FUNCTOR0:def11

      attr F is feasible means

      : Def11: for o1,o2 be Object of C1 st <^o1, o2^> <> {} holds (the Arrows of C2 . (the ObjectMap of F . (o1,o2))) <> {} ;

    end

    definition

      let C1,C2 be AltGraph;

      struct ( BimapStr over C1, C2) FunctorStr over C1,C2 (# the ObjectMap -> bifunction of the carrier of C1, the carrier of C2,

the MorphMap -> MSUnTrans of the ObjectMap, the Arrows of C1, the Arrows of C2 #)

       attr strict strict;

    end

    definition

      let C1,C2 be 1-sorted;

      let IT be BimapStr over C1, C2;

      :: FUNCTOR0:def12

      attr IT is Covariant means

      : Def12: the ObjectMap of IT is Covariant;

      :: FUNCTOR0:def13

      attr IT is Contravariant means

      : Def13: the ObjectMap of IT is Contravariant;

    end

    registration

      let C1,C2 be AltGraph;

      cluster Covariant for FunctorStr over C1, C2;

      existence

      proof

        set f = the Covariant bifunction of the carrier of C1, the carrier of C2;

        set M = the MSUnTrans of f, the Arrows of C1, the Arrows of C2;

        take F = FunctorStr (# f, M #);

        thus the ObjectMap of F is Covariant;

      end;

      cluster Contravariant for FunctorStr over C1, C2;

      existence

      proof

        set f = the Contravariant bifunction of the carrier of C1, the carrier of C2;

        set M = the MSUnTrans of f, the Arrows of C1, the Arrows of C2;

        take F = FunctorStr (# f, M #);

        thus the ObjectMap of F is Contravariant;

      end;

    end

    definition

      let C1,C2 be AltGraph;

      let F be FunctorStr over C1, C2;

      let o1,o2 be Object of C1;

      :: FUNCTOR0:def14

      func Morph-Map (F,o1,o2) -> set equals (the MorphMap of F . (o1,o2));

      correctness ;

    end

    registration

      let C1,C2 be AltGraph;

      let F be FunctorStr over C1, C2;

      let o1,o2 be Object of C1;

      cluster ( Morph-Map (F,o1,o2)) -> Relation-like Function-like;

      coherence ;

    end

    definition

      let C1,C2 be non empty AltGraph;

      let F be Covariant FunctorStr over C1, C2;

      let o1,o2 be Object of C1;

      :: original: Morph-Map

      redefine

      func Morph-Map (F,o1,o2) -> Function of <^o1, o2^>, <^(F . o1), (F . o2)^> ;

      coherence

      proof

        consider I29 be non empty set, B9 be ManySortedSet of I29, f9 be Function of [:the carrier of C1, the carrier of C1:], I29 such that

         A1: the ObjectMap of F = f9 and

         A2: the Arrows of C2 = B9 and

         A3: the MorphMap of F is ManySortedFunction of the Arrows of C1, (B9 * f9) by Def3;

        

         A4: (the Arrows of C1 . [o1, o2]) = (the Arrows of C1 . (o1,o2))

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

        

         A5: [o1, o2] in [:the carrier of C1, the carrier of C1:] by ZFMISC_1: 87;

        the ObjectMap of F is Covariant by Def12;

        then

        consider g be Function of the carrier of C1, the carrier of C2 such that

         A6: the ObjectMap of F = [:g, g:];

        

         A7: (F . o1) = ( [(g . o1), (g . o1)] `1 ) by A6, FUNCT_3: 75

        .= (g . o1);

        

         A8: (F . o2) = ( [(g . o2), (g . o2)] `1 ) by A6, FUNCT_3: 75

        .= (g . o2);

        ( dom f9) = [:the carrier of C1, the carrier of C1:] by FUNCT_2:def 1;

        

        then ((B9 * f9) . [o1, o2]) = (B9 . (f9 . (o1,o2))) by A5, FUNCT_1: 13

        .= (the Arrows of C2 . ((F . o1),(F . o2))) by A1, A2, A6, A7, A8, FUNCT_3: 75

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

        hence thesis by A3, A4, A5, PBOOLE:def 15;

      end;

    end

    definition

      let C1,C2 be non empty AltGraph;

      let F be Covariant FunctorStr over C1, C2;

      let o1,o2 be Object of C1;

      let m be Morphism of o1, o2;

      :: FUNCTOR0:def15

      func F . m -> Morphism of (F . o1), (F . o2) equals

      : Def15: (( Morph-Map (F,o1,o2)) . m);

      coherence

      proof

        reconsider A = <^o1, o2^>, B = <^(F . o1), (F . o2)^> as non empty set by A1, A2;

        reconsider M = ( Morph-Map (F,o1,o2)) as Function of A, B;

        reconsider m as Element of A;

        (M . m) is Element of B;

        hence thesis;

      end;

    end

    definition

      let C1,C2 be non empty AltGraph;

      let F be Contravariant FunctorStr over C1, C2;

      let o1,o2 be Object of C1;

      :: original: Morph-Map

      redefine

      func Morph-Map (F,o1,o2) -> Function of <^o1, o2^>, <^(F . o2), (F . o1)^> ;

      coherence

      proof

        consider I29 be non empty set, B9 be ManySortedSet of I29, f9 be Function of [:the carrier of C1, the carrier of C1:], I29 such that

         A1: the ObjectMap of F = f9 and

         A2: the Arrows of C2 = B9 and

         A3: the MorphMap of F is ManySortedFunction of the Arrows of C1, (B9 * f9) by Def3;

        

         A4: (the Arrows of C1 . [o1, o2]) = (the Arrows of C1 . (o1,o2))

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

        

         A5: [o1, o2] in [:the carrier of C1, the carrier of C1:] by ZFMISC_1: 87;

        the ObjectMap of F is Contravariant by Def13;

        then

        consider g be Function of the carrier of C1, the carrier of C2 such that

         A6: the ObjectMap of F = ( ~ [:g, g:]);

        

         A7: ( dom f9) = [:the carrier of C1, the carrier of C1:] by FUNCT_2:def 1;

        then [o1, o1] in ( dom ( ~ [:g, g:])) by A1, A6, ZFMISC_1: 87;

        then [o1, o1] in ( dom [:g, g:]) by FUNCT_4: 42;

        

        then

         A8: (F . o1) = (( [:g, g:] . (o1,o1)) `1 ) by A6, FUNCT_4:def 2

        .= ( [(g . o1), (g . o1)] `1 ) by FUNCT_3: 75

        .= (g . o1);

         [o2, o2] in ( dom ( ~ [:g, g:])) by A1, A6, A7, ZFMISC_1: 87;

        then [o2, o2] in ( dom [:g, g:]) by FUNCT_4: 42;

        

        then

         A9: (F . o2) = (( [:g, g:] . (o2,o2)) `1 ) by A6, FUNCT_4:def 2

        .= ( [(g . o2), (g . o2)] `1 ) by FUNCT_3: 75

        .= (g . o2);

         [o1, o2] in ( dom ( ~ [:g, g:])) by A1, A6, A7, ZFMISC_1: 87;

        then

         A10: [o2, o1] in ( dom [:g, g:]) by FUNCT_4: 42;

        ((B9 * f9) . [o1, o2]) = (B9 . (f9 . (o1,o2))) by A5, A7, FUNCT_1: 13

        .= (B9 . ( [:g, g:] . (o2,o1))) by A1, A6, A10, FUNCT_4:def 2

        .= (the Arrows of C2 . ((F . o2),(F . o1))) by A2, A8, A9, FUNCT_3: 75

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

        hence thesis by A3, A4, A5, PBOOLE:def 15;

      end;

    end

    definition

      let C1,C2 be non empty AltGraph;

      let F be Contravariant FunctorStr over C1, C2;

      let o1,o2 be Object of C1;

      let m be Morphism of o1, o2;

      :: FUNCTOR0:def16

      func F . m -> Morphism of (F . o2), (F . o1) equals

      : Def16: (( Morph-Map (F,o1,o2)) . m);

      coherence

      proof

        reconsider A = <^o1, o2^>, B = <^(F . o2), (F . o1)^> as non empty set by A1, A2;

        reconsider M = ( Morph-Map (F,o1,o2)) as Function of A, B;

        reconsider m as Element of A;

        (M . m) is Element of B;

        hence thesis;

      end;

    end

    definition

      let C1,C2 be non empty AltGraph;

      let o be Object of C2;

      let m be Morphism of o, o;

      :: FUNCTOR0:def17

      func C1 --> m -> strict FunctorStr over C1, C2 means

      : Def17: the ObjectMap of it = ( [:the carrier of C1, the carrier of C1:] --> [o, o]) & the MorphMap of it = the set of all [ [o1, o2], ( <^o1, o2^> --> m)] where o1 be Object of C1, o2 be Object of C1;

      existence

      proof

        set I1 = [:the carrier of C1, the carrier of C1:], I2 = [:the carrier of C2, the carrier of C2:], A = the Arrows of C1, B = the Arrows of C2;

        reconsider oo = [o, o] as Element of I2 by ZFMISC_1: 87;

        (B . oo) = (B . (o,o))

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

        then

        reconsider m as Element of (B . oo);

        reconsider f = (I1 --> oo) as Function of I1, I2;

        reconsider f as bifunction of the carrier of C1, the carrier of C2;

        set M = the set of all [ [o1, o2], ( <^o1, o2^> --> m)] where o1 be Object of C1, o2 be Object of C1;

        

         A2: M = the set of all [o9, ((A . o9) --> m)] where o9 be Element of I1

        proof

          thus M c= the set of all [o9, ((A . o9) --> m)] where o9 be Element of I1

          proof

            let x be object;

            assume x in M;

            then

            consider o3,o4 be Object of C1 such that

             A3: x = [ [o3, o4], ( <^o3, o4^> --> m)];

            reconsider oo = [o3, o4] as Element of I1 by ZFMISC_1: 87;

            x = [oo, ((A . (o3,o4)) --> m)] by A3, ALTCAT_1:def 1

            .= [oo, ((A . oo) --> m)];

            hence thesis;

          end;

          let x be object;

          assume x in the set of all [o9, ((A . o9) --> m)] where o9 be Element of I1;

          then

          consider o9 be Element of I1 such that

           A4: x = [o9, ((A . o9) --> m)];

          reconsider o1 = (o9 `1 ), o2 = (o9 `2 ) as Element of C1 by MCART_1: 10;

          reconsider o1, o2 as Object of C1;

          o9 = [o1, o2] by MCART_1: 21;

          

          then x = [ [o1, o2], ((A . (o1,o2)) --> m)] by A4

          .= [ [o1, o2], ( <^o1, o2^> --> m)] by ALTCAT_1:def 1;

          hence thesis;

        end;

        (B . (o,o)) <> {} by A1, ALTCAT_1:def 1;

        then

        reconsider M as MSUnTrans of f, A, B by A2, Th18;

        take FunctorStr (# f, M #);

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: FUNCTOR0:21

    

     Th21: for C1,C2 be non empty AltGraph, o2 be Object of C2 st <^o2, o2^> <> {} holds for m be Morphism of o2, o2, o1 be Object of C1 holds ((C1 --> m) . o1) = o2

    proof

      let C1,C2 be non empty AltGraph, o2 be Object of C2 such that

       A1: <^o2, o2^> <> {} ;

      let m be Morphism of o2, o2, o1 be Object of C1;

      

       A2: [o1, o1] in [:the carrier of C1, the carrier of C1:] by ZFMISC_1: 87;

      

      thus ((C1 --> m) . o1) = ((( [:the carrier of C1, the carrier of C1:] --> [o2, o2]) . (o1,o1)) `1 ) by A1, Def17

      .= ( [o2, o2] `1 ) by A2, FUNCOP_1: 7

      .= o2;

    end;

    registration

      let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph;

      let o be Object of C2, m be Morphism of o, o;

      cluster (C1 --> m) -> Covariant Contravariant feasible;

      coherence

      proof

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

        then

         A1: the ObjectMap of (C1 --> m) = ( [:the carrier of C1, the carrier of C1:] --> [o, o]) by Def17;

        hence the ObjectMap of (C1 --> m) is Covariant Contravariant by Th15;

        let o1,o2 be Object of C1 such that <^o1, o2^> <> {} ;

         [o1, o2] in [:the carrier of C1, the carrier of C1:] by ZFMISC_1: 87;

        then (the Arrows of C2 . (the ObjectMap of (C1 --> m) . (o1,o2))) = (the Arrows of C2 . (o,o)) by A1, FUNCOP_1: 7;

        hence thesis by ALTCAT_2:def 6;

      end;

    end

    registration

      let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph;

      cluster feasible Covariant Contravariant for FunctorStr over C1, C2;

      existence

      proof

        set o = the Object of C2;

        set m = the Morphism of o, o;

        take (C1 --> m);

        thus thesis;

      end;

    end

    theorem :: FUNCTOR0:22

    

     Th22: for C1,C2 be non empty AltGraph, F be Covariant FunctorStr over C1, C2, o1,o2 be Object of C1 holds (the ObjectMap of F . (o1,o2)) = [(F . o1), (F . o2)]

    proof

      let C1,C2 be non empty AltGraph, F be Covariant FunctorStr over C1, C2, o1,o2 be Object of C1;

      the ObjectMap of F is Covariant by Def12;

      then

      consider f be Function of the carrier of C1, the carrier of C2 such that

       A1: the ObjectMap of F = [:f, f:];

      

       A2: (F . o1) = ( [(f . o1), (f . o1)] `1 ) by A1, FUNCT_3: 75

      .= (f . o1);

      (F . o2) = ( [(f . o2), (f . o2)] `1 ) by A1, FUNCT_3: 75

      .= (f . o2);

      hence thesis by A1, A2, FUNCT_3: 75;

    end;

    definition

      let C1,C2 be non empty AltGraph;

      let F be Covariant FunctorStr over C1, C2;

      :: original: feasible

      redefine

      :: FUNCTOR0:def18

      attr F is feasible means

      : Def18: for o1,o2 be Object of C1 st <^o1, o2^> <> {} holds <^(F . o1), (F . o2)^> <> {} ;

      compatibility

      proof

        hereby

          assume

           A1: F is feasible;

          let o1,o2 be Object of C1;

          assume

           A2: <^o1, o2^> <> {} ;

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

          .= (the Arrows of C2 . (the ObjectMap of F . (o1,o2))) by Th22;

          hence <^(F . o1), (F . o2)^> <> {} by A1, A2;

        end;

        assume

         A3: for o1,o2 be Object of C1 st <^o1, o2^> <> {} holds <^(F . o1), (F . o2)^> <> {} ;

        let o1,o2 be Object of C1;

        assume

         A4: <^o1, o2^> <> {} ;

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

        .= (the Arrows of C2 . (the ObjectMap of F . (o1,o2))) by Th22;

        hence thesis by A3, A4;

      end;

    end

    theorem :: FUNCTOR0:23

    

     Th23: for C1,C2 be non empty AltGraph, F be Contravariant FunctorStr over C1, C2, o1,o2 be Object of C1 holds (the ObjectMap of F . (o1,o2)) = [(F . o2), (F . o1)]

    proof

      let C1,C2 be non empty AltGraph, F be Contravariant FunctorStr over C1, C2, o1,o2 be Object of C1;

      the ObjectMap of F is Contravariant by Def13;

      then

      consider f be Function of the carrier of C1, the carrier of C2 such that

       A1: the ObjectMap of F = ( ~ [:f, f:]);

      

       A2: ( dom [:f, f:]) = [:the carrier of C1, the carrier of C1:] by FUNCT_2:def 1;

      then [o1, o1] in ( dom [:f, f:]) by ZFMISC_1: 87;

      

      then

       A3: (F . o1) = (( [:f, f:] . (o1,o1)) `1 ) by A1, FUNCT_4:def 2

      .= ( [(f . o1), (f . o1)] `1 ) by FUNCT_3: 75

      .= (f . o1);

       [o2, o2] in ( dom [:f, f:]) by A2, ZFMISC_1: 87;

      

      then

       A4: (F . o2) = (( [:f, f:] . (o2,o2)) `1 ) by A1, FUNCT_4:def 2

      .= ( [(f . o2), (f . o2)] `1 ) by FUNCT_3: 75

      .= (f . o2);

       [o2, o1] in ( dom [:f, f:]) by A2, ZFMISC_1: 87;

      

      hence (the ObjectMap of F . (o1,o2)) = ( [:f, f:] . (o2,o1)) by A1, FUNCT_4:def 2

      .= [(F . o2), (F . o1)] by A3, A4, FUNCT_3: 75;

    end;

    definition

      let C1,C2 be non empty AltGraph;

      let F be Contravariant FunctorStr over C1, C2;

      :: original: feasible

      redefine

      :: FUNCTOR0:def19

      attr F is feasible means

      : Def19: for o1,o2 be Object of C1 st <^o1, o2^> <> {} holds <^(F . o2), (F . o1)^> <> {} ;

      compatibility

      proof

        hereby

          assume

           A1: F is feasible;

          let o1,o2 be Object of C1;

          assume

           A2: <^o1, o2^> <> {} ;

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

          .= (the Arrows of C2 . (the ObjectMap of F . (o1,o2))) by Th23;

          hence <^(F . o2), (F . o1)^> <> {} by A1, A2;

        end;

        assume

         A3: for o1,o2 be Object of C1 st <^o1, o2^> <> {} holds <^(F . o2), (F . o1)^> <> {} ;

        let o1,o2 be Object of C1;

        assume

         A4: <^o1, o2^> <> {} ;

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

        .= (the Arrows of C2 . (the ObjectMap of F . (o1,o2))) by Th23;

        hence thesis by A3, A4;

      end;

    end

    registration

      let C1,C2 be AltGraph;

      let F be FunctorStr over C1, C2;

      cluster the MorphMap of F -> Function-yielding;

      coherence ;

    end

    registration

      cluster non empty reflexive for AltCatStr;

      existence

      proof

        set C = the category;

        take C;

        thus thesis;

      end;

    end

    definition

      let C1,C2 be with_units non empty AltCatStr;

      let F be FunctorStr over C1, C2;

      :: FUNCTOR0:def20

      attr F is id-preserving means

      : Def20: for o be Object of C1 holds (( Morph-Map (F,o,o)) . ( idm o)) = ( idm (F . o));

    end

    theorem :: FUNCTOR0:24

    

     Th24: for C1,C2 be non empty AltGraph, o2 be Object of C2 st <^o2, o2^> <> {} holds for m be Morphism of o2, o2, o,o9 be Object of C1, f be Morphism of o, o9 st <^o, o9^> <> {} holds (( Morph-Map ((C1 --> m),o,o9)) . f) = m

    proof

      let C1,C2 be non empty AltGraph, o2 be Object of C2 such that

       A1: <^o2, o2^> <> {} ;

      let m be Morphism of o2, o2, o,o9 be Object of C1, f be Morphism of o, o9 such that

       A2: <^o, o9^> <> {} ;

      set X = the set of all [ [o1, o19], ( <^o1, o19^> --> m)] where o1 be Object of C1, o19 be Object of C1;

      set Y = the set of all [ [o1, o19], ((the Arrows of C1 . (o1,o19)) --> m)] where o1 be Element of C1, o19 be Element of C1;

      

       A3: X c= Y

      proof

        let e be object;

        assume e in X;

        then

        consider o1,o19 be Object of C1 such that

         A4: e = [ [o1, o19], ( <^o1, o19^> --> m)];

        e = [ [o1, o19], ((the Arrows of C1 . (o1,o19)) --> m)] by A4, ALTCAT_1:def 1;

        hence thesis;

      end;

      

       A5: Y c= X

      proof

        let e be object;

        assume e in Y;

        then

        consider o1,o19 be Element of C1 such that

         A6: e = [ [o1, o19], ((the Arrows of C1 . (o1,o19)) --> m)];

        reconsider o1, o19 as Object of C1;

        e = [ [o1, o19], ( <^o1, o19^> --> m)] by A6, ALTCAT_1:def 1;

        hence thesis;

      end;

      defpred P[ set, set] means not contradiction;

      deffunc F( Element of C1, Element of C1) = ((the Arrows of C1 . ($1,$2)) --> m);

      the MorphMap of (C1 --> m) = X by A1, Def17;

      then

       A7: the MorphMap of (C1 --> m) = { [ [o1, o19], F(o1,o19)] where o1 be Element of C1, o19 be Element of C1 : P[o1, o19] } by A3, A5;

      

       A8: P[o, o9];

      ( Morph-Map ((C1 --> m),o,o9)) = (the MorphMap of (C1 --> m) . (o,o9))

      .= F(o,o9) from ValOnPair( A7, A8);

      

      hence (( Morph-Map ((C1 --> m),o,o9)) . f) = (( <^o, o9^> --> m) . f) by ALTCAT_1:def 1

      .= m by A2, FUNCOP_1: 7;

    end;

    registration

      cluster with_units -> reflexive for non empty AltCatStr;

      coherence ;

    end

    registration

      let C1,C2 be with_units non empty AltCatStr;

      let o2 be Object of C2;

      cluster (C1 --> ( idm o2)) -> id-preserving;

      coherence

      proof

        let o1 be Object of C1;

        

         A1: <^o2, o2^> <> {} by ALTCAT_2:def 7;

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

        

        hence (( Morph-Map ((C1 --> ( idm o2)),o1,o1)) . ( idm o1)) = ( idm o2) by A1, Th24

        .= ( idm ((C1 --> ( idm o2)) . o1)) by A1, Th21;

      end;

    end

    registration

      let C1 be non empty AltGraph;

      let C2 be non empty reflexive AltGraph;

      let o2 be Object of C2;

      let m be Morphism of o2, o2;

      cluster (C1 --> m) -> reflexive;

      coherence

      proof

        let o be Object of C1;

        

         A1: [o, o] in [:the carrier of C1, the carrier of C1:] by ZFMISC_1: 87;

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

        

        then

         A2: (the ObjectMap of (C1 --> m) . (o,o)) = (( [:the carrier of C1, the carrier of C1:] --> [o2, o2]) . [o, o]) by Def17

        .= [o2, o2] by A1, FUNCOP_1: 7;

        thus thesis by A2;

      end;

    end

    registration

      let C1 be non empty AltGraph;

      let C2 be non empty reflexive AltGraph;

      cluster feasible reflexive for FunctorStr over C1, C2;

      existence

      proof

        set o2 = the Object of C2, m = the Morphism of o2, o2;

        take (C1 --> m);

        thus thesis;

      end;

    end

    registration

      let C1,C2 be with_units non empty AltCatStr;

      cluster id-preserving feasible reflexive strict for FunctorStr over C1, C2;

      existence

      proof

        set o2 = the Object of C2;

        take (C1 --> ( idm o2));

        thus thesis;

      end;

    end

    definition

      let C1,C2 be non empty AltCatStr;

      let F be FunctorStr over C1, C2;

      :: FUNCTOR0:def21

      attr F is comp-preserving means for o1,o2,o3 be Object of C1 st <^o1, o2^> <> {} & <^o2, o3^> <> {} holds for f be Morphism of o1, o2, g be Morphism of o2, o3 holds ex f9 be Morphism of (F . o1), (F . o2), g9 be Morphism of (F . o2), (F . o3) st f9 = (( Morph-Map (F,o1,o2)) . f) & g9 = (( Morph-Map (F,o2,o3)) . g) & (( Morph-Map (F,o1,o3)) . (g * f)) = (g9 * f9);

    end

    definition

      let C1,C2 be non empty AltCatStr;

      let F be FunctorStr over C1, C2;

      :: FUNCTOR0:def22

      attr F is comp-reversing means for o1,o2,o3 be Object of C1 st <^o1, o2^> <> {} & <^o2, o3^> <> {} holds for f be Morphism of o1, o2, g be Morphism of o2, o3 holds ex f9 be Morphism of (F . o2), (F . o1), g9 be Morphism of (F . o3), (F . o2) st f9 = (( Morph-Map (F,o1,o2)) . f) & g9 = (( Morph-Map (F,o2,o3)) . g) & (( Morph-Map (F,o1,o3)) . (g * f)) = (f9 * g9);

    end

    definition

      let C1 be non empty transitive AltCatStr;

      let C2 be non empty reflexive AltCatStr;

      let F be Covariant feasible FunctorStr over C1, C2;

      :: original: comp-preserving

      redefine

      :: FUNCTOR0:def23

      attr F is comp-preserving means for o1,o2,o3 be Object of C1 st <^o1, o2^> <> {} & <^o2, o3^> <> {} holds for f be Morphism of o1, o2, g be Morphism of o2, o3 holds (F . (g * f)) = ((F . g) * (F . f));

      compatibility

      proof

        hereby

          assume

           A1: F is comp-preserving;

          let o1,o2,o3 be Object of C1 such that

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

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

          let f be Morphism of o1, o2, g be Morphism of o2, o3;

          consider f9 be Morphism of (F . o1), (F . o2), g9 be Morphism of (F . o2), (F . o3) such that

           A4: f9 = (( Morph-Map (F,o1,o2)) . f) and

           A5: g9 = (( Morph-Map (F,o2,o3)) . g) and

           A6: (( Morph-Map (F,o1,o3)) . (g * f)) = (g9 * f9) by A1, A2, A3;

          

           A7: <^(F . o1), (F . o2)^> <> {} by A2, Def18;

          

           A8: <^(F . o2), (F . o3)^> <> {} by A3, Def18;

          

           A9: f9 = (F . f) by A2, A4, A7, Def15;

          

           A10: g9 = (F . g) by A3, A5, A8, Def15;

          

           A11: <^o1, o3^> <> {} by A2, A3, ALTCAT_1:def 2;

          then <^(F . o1), (F . o3)^> <> {} by Def18;

          hence (F . (g * f)) = ((F . g) * (F . f)) by A6, A9, A10, A11, Def15;

        end;

        assume

         A12: for o1,o2,o3 be Object of C1 st <^o1, o2^> <> {} & <^o2, o3^> <> {} holds for f be Morphism of o1, o2, g be Morphism of o2, o3 holds (F . (g * f)) = ((F . g) * (F . f));

        let o1,o2,o3 be Object of C1 such that

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

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

        let f be Morphism of o1, o2, g be Morphism of o2, o3;

        

         A15: <^(F . o1), (F . o2)^> <> {} by A13, Def18;

        then

        reconsider f9 = (( Morph-Map (F,o1,o2)) . f) as Morphism of (F . o1), (F . o2) by A13, FUNCT_2: 5;

        

         A16: <^(F . o2), (F . o3)^> <> {} by A14, Def18;

        then

        reconsider g9 = (( Morph-Map (F,o2,o3)) . g) as Morphism of (F . o2), (F . o3) by A14, FUNCT_2: 5;

        take f9, g9;

        thus f9 = (( Morph-Map (F,o1,o2)) . f) & g9 = (( Morph-Map (F,o2,o3)) . g);

        

         A17: f9 = (F . f) by A13, A15, Def15;

        

         A18: g9 = (F . g) by A14, A16, Def15;

        

         A19: <^o1, o3^> <> {} by A13, A14, ALTCAT_1:def 2;

        then <^(F . o1), (F . o3)^> <> {} by Def18;

        

        hence (( Morph-Map (F,o1,o3)) . (g * f)) = (F . (g * f)) by A19, Def15

        .= (g9 * f9) by A12, A13, A14, A17, A18;

      end;

    end

    definition

      let C1 be non empty transitive AltCatStr;

      let C2 be non empty reflexive AltCatStr;

      let F be Contravariant feasible FunctorStr over C1, C2;

      :: original: comp-reversing

      redefine

      :: FUNCTOR0:def24

      attr F is comp-reversing means for o1,o2,o3 be Object of C1 st <^o1, o2^> <> {} & <^o2, o3^> <> {} holds for f be Morphism of o1, o2, g be Morphism of o2, o3 holds (F . (g * f)) = ((F . f) * (F . g));

      compatibility

      proof

        hereby

          assume

           A1: F is comp-reversing;

          let o1,o2,o3 be Object of C1 such that

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

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

          let f be Morphism of o1, o2, g be Morphism of o2, o3;

          consider f9 be Morphism of (F . o2), (F . o1), g9 be Morphism of (F . o3), (F . o2) such that

           A4: f9 = (( Morph-Map (F,o1,o2)) . f) and

           A5: g9 = (( Morph-Map (F,o2,o3)) . g) and

           A6: (( Morph-Map (F,o1,o3)) . (g * f)) = (f9 * g9) by A1, A2, A3;

          

           A7: <^(F . o2), (F . o1)^> <> {} by A2, Def19;

          

           A8: <^(F . o3), (F . o2)^> <> {} by A3, Def19;

          

           A9: f9 = (F . f) by A2, A4, A7, Def16;

          

           A10: g9 = (F . g) by A3, A5, A8, Def16;

          

           A11: <^o1, o3^> <> {} by A2, A3, ALTCAT_1:def 2;

          then <^(F . o3), (F . o1)^> <> {} by Def19;

          hence (F . (g * f)) = ((F . f) * (F . g)) by A6, A9, A10, A11, Def16;

        end;

        assume

         A12: for o1,o2,o3 be Object of C1 st <^o1, o2^> <> {} & <^o2, o3^> <> {} holds for f be Morphism of o1, o2, g be Morphism of o2, o3 holds (F . (g * f)) = ((F . f) * (F . g));

        let o1,o2,o3 be Object of C1 such that

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

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

        let f be Morphism of o1, o2, g be Morphism of o2, o3;

        

         A15: <^(F . o2), (F . o1)^> <> {} by A13, Def19;

        then

        reconsider f9 = (( Morph-Map (F,o1,o2)) . f) as Morphism of (F . o2), (F . o1) by A13, FUNCT_2: 5;

        

         A16: <^(F . o3), (F . o2)^> <> {} by A14, Def19;

        then

        reconsider g9 = (( Morph-Map (F,o2,o3)) . g) as Morphism of (F . o3), (F . o2) by A14, FUNCT_2: 5;

        take f9, g9;

        thus f9 = (( Morph-Map (F,o1,o2)) . f) & g9 = (( Morph-Map (F,o2,o3)) . g);

        

         A17: f9 = (F . f) by A13, A15, Def16;

        

         A18: g9 = (F . g) by A14, A16, Def16;

        

         A19: <^o1, o3^> <> {} by A13, A14, ALTCAT_1:def 2;

        then <^(F . o3), (F . o1)^> <> {} by Def19;

        

        hence (( Morph-Map (F,o1,o3)) . (g * f)) = (F . (g * f)) by A19, Def16

        .= (f9 * g9) by A12, A13, A14, A17, A18;

      end;

    end

    theorem :: FUNCTOR0:25

    

     Th25: for C1 be non empty AltGraph, C2 be non empty reflexive AltGraph, o2 be Object of C2, m be Morphism of o2, o2, F be Covariant feasible FunctorStr over C1, C2 st F = (C1 --> m) holds for o,o9 be Object of C1, f be Morphism of o, o9 st <^o, o9^> <> {} holds (F . f) = m

    proof

      let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph, o2 be Object of C2;

      

       A1: <^o2, o2^> <> {} by ALTCAT_2:def 7;

      let m be Morphism of o2, o2, F be Covariant feasible FunctorStr over C1, C2 such that

       A2: F = (C1 --> m);

      let o,o9 be Object of C1, f be Morphism of o, o9;

      assume

       A3: <^o, o9^> <> {} ;

      then <^(F . o), (F . o9)^> <> {} by Def18;

      

      hence (F . f) = (( Morph-Map (F,o,o9)) . f) by A3, Def15

      .= m by A1, A2, A3, Th24;

    end;

    theorem :: FUNCTOR0:26

    

     Th26: for C1 be non empty AltGraph, C2 be non empty reflexive AltGraph, o2 be Object of C2, m be Morphism of o2, o2, o,o9 be Object of C1, f be Morphism of o, o9 st <^o, o9^> <> {} holds ((C1 --> m) . f) = m

    proof

      let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph, o2 be Object of C2;

      

       A1: <^o2, o2^> <> {} by ALTCAT_2:def 7;

      let m be Morphism of o2, o2;

      set F = (C1 --> m);

      let o,o9 be Object of C1, f be Morphism of o, o9;

      assume

       A2: <^o, o9^> <> {} ;

      then <^(F . o9), (F . o)^> <> {} by Def19;

      

      hence (F . f) = (( Morph-Map (F,o,o9)) . f) by A2, Def16

      .= m by A1, A2, Th24;

    end;

    registration

      let C1 be non empty transitive AltCatStr, C2 be with_units non empty AltCatStr;

      let o be Object of C2;

      cluster (C1 --> ( idm o)) -> comp-preserving comp-reversing;

      coherence

      proof

        set F = (C1 --> ( idm o));

        reconsider G = F as Covariant feasible FunctorStr over C1, C2;

        

         A1: <^o, o^> <> {} by ALTCAT_2:def 7;

        G is comp-preserving

        proof

          let o1,o2,o3 be Object of C1;

          assume that

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

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

          

           A4: <^o1, o3^> <> {} by A2, A3, ALTCAT_1:def 2;

          let f be Morphism of o1, o2, g be Morphism of o2, o3;

          

           A5: (G . g) = ( idm o) by A3, Th25;

          

           A6: (G . f) = ( idm o) by A2, Th25;

          

           A7: (G . o1) = o by A1, Th21;

          

           A8: (G . o2) = o by A1, Th21;

          

           A9: (G . o3) = o by A1, Th21;

          

          thus (G . (g * f)) = ( idm o) by A4, Th25

          .= ((G . g) * (G . f)) by A1, A5, A6, A7, A8, A9, ALTCAT_1: 20;

        end;

        hence F is comp-preserving;

        let o1,o2,o3 be Object of C1;

        assume that

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

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

        

         A12: <^o1, o3^> <> {} by A10, A11, ALTCAT_1:def 2;

        let f be Morphism of o1, o2, g be Morphism of o2, o3;

        

         A13: (F . g) = ( idm o) by A11, Th26;

        

         A14: (F . f) = ( idm o) by A10, Th26;

        

         A15: (F . o1) = o by A1, Th21;

        

         A16: (F . o2) = o by A1, Th21;

        

         A17: (F . o3) = o by A1, Th21;

        

        thus (F . (g * f)) = ( idm o) by A12, Th26

        .= ((F . f) * (F . g)) by A1, A13, A14, A15, A16, A17, ALTCAT_1: 20;

      end;

    end

    definition

      let C1 be transitive with_units non empty AltCatStr, C2 be with_units non empty AltCatStr;

      :: FUNCTOR0:def25

      mode Functor of C1,C2 -> FunctorStr over C1, C2 means

      : Def25: it is feasible id-preserving & (it is Covariant comp-preserving or it is Contravariant comp-reversing);

      existence

      proof

        set o = the Object of C2;

        take (C1 --> ( idm o));

        thus thesis;

      end;

    end

    definition

      let C1 be transitive with_units non empty AltCatStr, C2 be with_units non empty AltCatStr, F be Functor of C1, C2;

      :: FUNCTOR0:def26

      attr F is covariant means

      : Def26: F is Covariant comp-preserving;

      :: FUNCTOR0:def27

      attr F is contravariant means

      : Def27: F is Contravariant comp-reversing;

    end

    definition

      let A be AltCatStr, B be SubCatStr of A;

      :: FUNCTOR0:def28

      func incl B -> strict FunctorStr over B, A means

      : Def28: the ObjectMap of it = ( id [:the carrier of B, the carrier of B:]) & the MorphMap of it = ( id the Arrows of B);

      existence

      proof

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

        then

        reconsider CC = [:the carrier of B, the carrier of B:] as Subset of [:the carrier of A, the carrier of A:] by ZFMISC_1: 96;

        set OM = ( id [:the carrier of B, the carrier of B:]);

        OM = ( incl CC);

        then

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

        set MM = ( id the Arrows of B);

        MM is MSUnTrans of OM, the Arrows of B, the Arrows of A

        proof

          per cases ;

            case [:the carrier of A, the carrier of A:] <> {} ;

            then

            reconsider I29 = [:the carrier of A, the carrier of A:] as non empty set;

            reconsider B9 = the Arrows of A as ManySortedSet of I29;

            reconsider f9 = OM as Function of [:the carrier of B, the carrier of B:], I29;

            take I29, B9, f9;

            thus OM = f9 & the Arrows of A = B9;

            thus MM is ManySortedFunction of the Arrows of B, (B9 * f9)

            proof

              let i be object;

              assume

               A1: i in [:the carrier of B, the carrier of B:];

              then

               A2: (MM . i) is Function of (the Arrows of B . i), (the Arrows of B . i) by PBOOLE:def 15;

              

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

              ((B9 * f9) . i) = (B9 . (f9 . i)) by A1, FUNCT_2: 15

              .= (the Arrows of A . i) by A1, FUNCT_1: 18;

              then (the Arrows of B . i) c= ((B9 * f9) . i) by A1, A3, ALTCAT_2:def 2;

              hence thesis by A2, FUNCT_2: 7;

            end;

          end;

            case [:the carrier of A, the carrier of A:] = {} ;

            then CC = {} ;

            hence thesis;

          end;

        end;

        then

        reconsider MM as MSUnTrans of OM, the Arrows of B, the Arrows of A;

        take FunctorStr (# OM, MM #);

        thus thesis;

      end;

      correctness ;

    end

    definition

      let A be AltGraph;

      :: FUNCTOR0:def29

      func id A -> strict FunctorStr over A, A means

      : Def29: the ObjectMap of it = ( id [:the carrier of A, the carrier of A:]) & the MorphMap of it = ( id the Arrows of A);

      existence

      proof

        reconsider OM = ( id [:the carrier of A, the carrier of A:]) as bifunction of the carrier of A, the carrier of A;

        set MM = ( id the Arrows of A);

        MM is MSUnTrans of OM, the Arrows of A, the Arrows of A

        proof

          per cases ;

            case [:the carrier of A, the carrier of A:] <> {} ;

            then

            reconsider I29 = [:the carrier of A, the carrier of A:] as non empty set;

            reconsider A9 = the Arrows of A as ManySortedSet of I29;

            reconsider f9 = OM as Function of [:the carrier of A, the carrier of A:], I29;

            take I29, A9, f9;

            thus OM = f9 & the Arrows of A = A9;

            thus MM is ManySortedFunction of the Arrows of A, (A9 * f9)

            proof

              let i be object;

              assume

               A1: i in [:the carrier of A, the carrier of A:];

              

              then ((A9 * f9) . i) = (A9 . (f9 . i)) by FUNCT_2: 15

              .= (the Arrows of A . i) by A1, FUNCT_1: 18;

              hence thesis by A1, PBOOLE:def 15;

            end;

          end;

            case [:the carrier of A, the carrier of A:] = {} ;

            hence thesis;

          end;

        end;

        then

        reconsider MM as MSUnTrans of OM, the Arrows of A, the Arrows of A;

        take FunctorStr (# OM, MM #);

        thus thesis;

      end;

      correctness ;

    end

    registration

      let A be AltCatStr, B be SubCatStr of A;

      cluster ( incl B) -> Covariant;

      coherence

      proof

        reconsider b = the carrier of B as Subset of A by ALTCAT_2:def 11;

        ( incl b) = ( id b);

        then

        reconsider f = ( id the carrier of B) as Function of the carrier of B, the carrier of A;

        take f;

        

        thus the ObjectMap of ( incl B) = ( id [:the carrier of B, the carrier of B:]) by Def28

        .= [:f, f:] by FUNCT_3: 69;

      end;

    end

    theorem :: FUNCTOR0:27

    

     Th27: for A be non empty AltCatStr, B be non empty SubCatStr of A, o be Object of B holds (( incl B) . o) = o

    proof

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

      

       A1: [o, o] in [:the carrier of B, the carrier of B:] by ZFMISC_1: 87;

      

      thus (( incl B) . o) = ((( id [:the carrier of B, the carrier of B:]) . [o, o]) `1 ) by Def28

      .= ( [o, o] `1 ) by A1, FUNCT_1: 18

      .= o;

    end;

    theorem :: FUNCTOR0:28

    

     Th28: for A be non empty AltCatStr, B be non empty SubCatStr of A, o1,o2 be Object of B holds <^o1, o2^> c= <^(( incl B) . o1), (( incl B) . o2)^>

    proof

      let A be non empty AltCatStr, B be non empty SubCatStr of A, o1,o2 be Object of B;

      

       A1: [o1, o2] in [:the carrier of B, the carrier of B:] by ZFMISC_1: 87;

      

       A2: <^o1, o2^> = (the Arrows of B . (o1,o2)) by ALTCAT_1:def 1

      .= (the Arrows of B . [o1, o2]);

      

       A3: (( incl B) . o1) = o1 by Th27;

      (( incl B) . o2) = o2 by Th27;

      

      then

       A4: <^(( incl B) . o1), (( incl B) . o2)^> = (the Arrows of A . (o1,o2)) by A3, ALTCAT_1:def 1

      .= (the Arrows of A . [o1, o2]);

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

      hence thesis by A1, A2, A4, ALTCAT_2:def 2;

    end;

    registration

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

      cluster ( incl B) -> feasible;

      coherence by Th28, XBOOLE_1: 3;

    end

    definition

      let A,B be AltGraph, F be FunctorStr over A, B;

      :: FUNCTOR0:def30

      attr F is faithful means the MorphMap of F is "1-1";

    end

    definition

      let A,B be AltGraph, F be FunctorStr over A, B;

      :: FUNCTOR0:def31

      attr F is full means ex B9 be ManySortedSet of [:the carrier of A, the carrier of A:], f be ManySortedFunction of the Arrows of A, B9 st B9 = (the Arrows of B * the ObjectMap of F) & f = the MorphMap of F & f is "onto";

    end

    definition

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

      :: original: full

      redefine

      :: FUNCTOR0:def32

      attr F is full means ex f be ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of F) st f = the MorphMap of F & f is "onto";

      compatibility ;

    end

    definition

      let A,B be AltGraph, F be FunctorStr over A, B;

      :: FUNCTOR0:def33

      attr F is injective means F is one-to-one faithful;

      :: FUNCTOR0:def34

      attr F is surjective means F is full onto;

    end

    definition

      let A,B be AltGraph, F be FunctorStr over A, B;

      :: FUNCTOR0:def35

      attr F is bijective means F is injective surjective;

    end

    registration

      let A,B be transitive with_units non empty AltCatStr;

      cluster strict covariant contravariant feasible for Functor of A, B;

      existence

      proof

        set o = the Object of B;

        reconsider F = (A --> ( idm o)) as Functor of A, B by Def25;

        take F;

        thus thesis;

      end;

    end

    theorem :: FUNCTOR0:29

    

     Th29: for A be non empty AltGraph, o be Object of A holds (( id A) . o) = o

    proof

      let A be non empty AltGraph, o be Object of A;

      

       A1: [o, o] in [:the carrier of A, the carrier of A:] by ZFMISC_1: 87;

      

      thus (( id A) . o) = ((( id [:the carrier of A, the carrier of A:]) . [o, o]) `1 ) by Def29

      .= ( [o, o] `1 ) by A1, FUNCT_1: 18

      .= o;

    end;

    theorem :: FUNCTOR0:30

    

     Th30: for A be non empty AltGraph, o1,o2 be Object of A st <^o1, o2^> <> {} holds for m be Morphism of o1, o2 holds (( Morph-Map (( id A),o1,o2)) . m) = m

    proof

      let A be non empty AltGraph, o1,o2 be Object of A such that <^o1, o2^> <> {} ;

      let m be Morphism of o1, o2;

      

       A1: [o1, o2] in [:the carrier of A, the carrier of A:] by ZFMISC_1: 87;

      ( Morph-Map (( id A),o1,o2)) = (( id the Arrows of A) . [o1, o2]) by Def29;

      

      hence (( Morph-Map (( id A),o1,o2)) . m) = (( id (the Arrows of A . (o1,o2))) . m) by A1, MSUALG_3:def 1

      .= (( id <^o1, o2^>) . m) by ALTCAT_1:def 1

      .= m;

    end;

    registration

      let A be non empty AltGraph;

      cluster ( id A) -> feasible Covariant;

      coherence

      proof

        thus ( id A) is feasible

        proof

          let o1,o2 be Object of A;

          

           A1: [o1, o2] in [:the carrier of A, the carrier of A:] by ZFMISC_1: 87;

          (the ObjectMap of ( id A) . (o1,o2)) = (( id [:the carrier of A, the carrier of A:]) . [o1, o2]) by Def29

          .= [o1, o2] by A1, FUNCT_1: 18;

          

          then (the Arrows of A . (the ObjectMap of ( id A) . (o1,o2))) = (the Arrows of A . (o1,o2))

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

          hence thesis;

        end;

        thus ( id A) is Covariant

        proof

          take I = ( id the carrier of A);

          

          thus the ObjectMap of ( id A) = ( id [:the carrier of A, the carrier of A:]) by Def29

          .= [:I, I:] by FUNCT_3: 69;

        end;

      end;

    end

    registration

      let A be non empty AltGraph;

      cluster Covariant feasible for FunctorStr over A, A;

      existence

      proof

        take ( id A);

        thus thesis;

      end;

    end

    theorem :: FUNCTOR0:31

    

     Th31: for A be non empty AltGraph, o1,o2 be Object of A st <^o1, o2^> <> {} holds for F be Covariant feasible FunctorStr over A, A st F = ( id A) holds for m be Morphism of o1, o2 holds (F . m) = m

    proof

      let A be non empty AltGraph, o1,o2 be Object of A such that

       A1: <^o1, o2^> <> {} ;

      let F be Covariant feasible FunctorStr over A, A such that

       A2: F = ( id A);

      let m be Morphism of o1, o2;

       <^(F . o1), (F . o2)^> <> {} by A1, Def18;

      

      hence (F . m) = (( Morph-Map (F,o1,o2)) . m) by A1, Def15

      .= m by A1, A2, Th30;

    end;

    registration

      let A be transitive with_units non empty AltCatStr;

      cluster ( id A) -> id-preserving comp-preserving;

      coherence

      proof

        thus ( id A) is id-preserving

        proof

          let o be Object of A;

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

          

          hence (( Morph-Map (( id A),o,o)) . ( idm o)) = ( idm o) by Th30

          .= ( idm (( id A) . o)) by Th29;

        end;

        set F = ( id A);

        F is comp-preserving

        proof

          let o1,o2,o3 be Object of A such that

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

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

          let f be Morphism of o1, o2, g be Morphism of o2, o3;

          

           A3: <^o1, o3^> <> {} by A1, A2, ALTCAT_1:def 2;

          

           A4: (F . o1) = o1 by Th29;

          

           A5: (F . o2) = o2 by Th29;

          

           A6: (F . o3) = o3 by Th29;

          

           A7: (F . g) = g by A2, Th31;

          (F . f) = f by A1, Th31;

          hence thesis by A3, A4, A5, A6, A7, Th31;

        end;

        hence thesis;

      end;

    end

    definition

      let A be transitive with_units non empty AltCatStr;

      :: original: id

      redefine

      func id A -> strict covariant Functor of A, A ;

      coherence by Def25, Def26;

    end

    registration

      let A be AltGraph;

      cluster ( id A) -> bijective;

      coherence

      proof

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

        

         A1: the ObjectMap of ( id A) = ( id CC) by Def29;

        hence ( id A) is one-to-one;

        thus ( id A) is faithful

        proof

          per cases ;

            suppose

             A2: the carrier of A <> {} ;

            let i be set, f be Function such that

             A3: i in ( dom the MorphMap of ( id A)) and

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

            consider o1,o2 be Element of A such that

             A5: i = [o1, o2] by A2, A3, DOMAIN_1: 1;

            reconsider o1, o2 as Object of A;

            

             A6: [o1, o2] in [:the carrier of A, the carrier of A:] by A2, ZFMISC_1: 87;

            f = (( id the Arrows of A) . (o1,o2)) by A4, A5, Def29

            .= ( id (the Arrows of A . [o1, o2])) by A6, MSUALG_3:def 1;

            hence thesis;

          end;

            suppose

             A7: the carrier of A = {} ;

            let i be set, f be Function such that

             A8: i in ( dom the MorphMap of ( id A)) and (the MorphMap of ( id A) . i) = f;

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

            .= {} by A7, ZFMISC_1: 90;

            hence thesis by A8;

          end;

        end;

        thus ( id A) is full

        proof

          per cases ;

            suppose A is non empty;

            then

            reconsider A as non empty AltGraph;

            ( id A) is full

            proof

              reconsider f = the MorphMap of ( id A) as ManySortedFunction of the Arrows of A, (the Arrows of A * the ObjectMap of ( id A)) by Def4;

              take f;

              thus f = the MorphMap of ( id A);

              let i be set;

              assume

               A9: i in [:the carrier of A, the carrier of A:];

              then

              consider o1,o2 be Element of A such that

               A10: i = [o1, o2] by DOMAIN_1: 1;

              reconsider o1, o2 as Object of A;

              

               A11: [o1, o2] in [:the carrier of A, the carrier of A:] by ZFMISC_1: 87;

              

               A12: ( dom the ObjectMap of ( id A)) = CC by A1;

              (f . i) = (( id the Arrows of A) . (o1,o2)) by A10, Def29

              .= ( id (the Arrows of A . [o1, o2])) by A11, MSUALG_3:def 1;

              

              hence ( rng (f . i)) = (the Arrows of A . [o1, o2])

              .= (the Arrows of A . (the ObjectMap of ( id A) . i)) by A1, A9, A10, FUNCT_1: 18

              .= ((the Arrows of A * the ObjectMap of ( id A)) . i) by A9, A12, FUNCT_1: 13;

            end;

            hence thesis;

          end;

            suppose A is empty;

            then

             A13: the carrier of A = {} ;

            the ObjectMap of ( id A) = ( id [:the carrier of A, the carrier of A:]) by Def29;

            then

            reconsider B = (the Arrows of A * the ObjectMap of ( id A)) as ManySortedSet of [:the carrier of A, the carrier of A:] by Th2;

            reconsider f = the MorphMap of ( id A) as ManySortedSet of [:the carrier of A, the carrier of A:];

            f is ManySortedFunction of the Arrows of A, B

            proof

              let i be object;

              thus thesis by A13, ZFMISC_1: 90;

            end;

            then

            reconsider f as ManySortedFunction of the Arrows of A, B;

            take B, f;

            thus B = (the Arrows of A * the ObjectMap of ( id A)) & f = the MorphMap of ( id A);

            let i be set;

            thus thesis by A13, ZFMISC_1: 90;

          end;

        end;

        the ObjectMap of ( id A) is onto by A1;

        hence ( id A) is onto;

      end;

    end

    begin

    definition

      let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;

      let F be feasible FunctorStr over C1, C2, G be FunctorStr over C2, C3;

      :: FUNCTOR0:def36

      func G * F -> strict FunctorStr over C1, C3 means

      : Def36: the ObjectMap of it = (the ObjectMap of G * the ObjectMap of F) & the MorphMap of it = ((the MorphMap of G * the ObjectMap of F) ** the MorphMap of F);

      existence

      proof

        reconsider O = (the ObjectMap of G * the ObjectMap of F) as bifunction of the carrier of C1, the carrier of C3;

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

        reconsider H = (the MorphMap of G * the ObjectMap of F) as MSUnTrans of O, (the Arrows of C2 * the ObjectMap of F), the Arrows of C3 by Th17;

        for ii be set st ii in I1 & ((the Arrows of C2 * the ObjectMap of F) . ii) = {} holds (the Arrows of C1 . ii) = {} or ((the Arrows of C3 * O) . ii) = {}

        proof

          let ii be set such that

           A1: ii in I1 and

           A2: ((the Arrows of C2 * the ObjectMap of F) . ii) = {} ;

          

           A3: ( dom the ObjectMap of F) = I1 by FUNCT_2:def 1;

          reconsider o1 = (ii `1 ), o2 = (ii `2 ) as Object of C1 by A1, MCART_1: 10;

          ii = [o1, o2] by A1, MCART_1: 21;

          then

           A4: (the Arrows of C2 . (the ObjectMap of F . (o1,o2))) = {} by A1, A2, A3, FUNCT_1: 13;

          (the Arrows of C1 . ii) = (the Arrows of C1 . (o1,o2)) by A1, MCART_1: 21

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

          .= {} by A4, Def11;

          hence thesis;

        end;

        then

        reconsider M = (H ** the MorphMap of F) as MSUnTrans of O, the Arrows of C1, the Arrows of C3 by Th19;

        take FunctorStr (# O, M #);

        thus thesis;

      end;

      correctness ;

    end

    registration

      let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;

      let F be Covariant feasible FunctorStr over C1, C2, G be Covariant FunctorStr over C2, C3;

      cluster (G * F) -> Covariant;

      correctness

      proof

        the ObjectMap of F is Covariant by Def12;

        then

        consider f be Function of the carrier of C1, the carrier of C2 such that

         A1: the ObjectMap of F = [:f, f:];

        the ObjectMap of G is Covariant by Def12;

        then

        consider g be Function of the carrier of C2, the carrier of C3 such that

         A2: the ObjectMap of G = [:g, g:];

        take (g * f);

        

        thus the ObjectMap of (G * F) = (the ObjectMap of G * the ObjectMap of F) by Def36

        .= [:(g * f), (g * f):] by A1, A2, FUNCT_3: 71;

      end;

    end

    registration

      let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;

      let F be Contravariant feasible FunctorStr over C1, C2, G be Covariant FunctorStr over C2, C3;

      cluster (G * F) -> Contravariant;

      correctness

      proof

        the ObjectMap of F is Contravariant by Def13;

        then

        consider f be Function of the carrier of C1, the carrier of C2 such that

         A1: the ObjectMap of F = ( ~ [:f, f:]);

        the ObjectMap of G is Covariant by Def12;

        then

        consider g be Function of the carrier of C2, the carrier of C3 such that

         A2: the ObjectMap of G = [:g, g:];

        take (g * f);

        

        thus the ObjectMap of (G * F) = (the ObjectMap of G * the ObjectMap of F) by Def36

        .= ( ~ ( [:g, g:] * [:f, f:])) by A1, A2, ALTCAT_2: 2

        .= ( ~ [:(g * f), (g * f):]) by FUNCT_3: 71;

      end;

    end

    registration

      let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;

      let F be Covariant feasible FunctorStr over C1, C2, G be Contravariant FunctorStr over C2, C3;

      cluster (G * F) -> Contravariant;

      correctness

      proof

        the ObjectMap of F is Covariant by Def12;

        then

        consider f be Function of the carrier of C1, the carrier of C2 such that

         A1: the ObjectMap of F = [:f, f:];

        the ObjectMap of G is Contravariant by Def13;

        then

        consider g be Function of the carrier of C2, the carrier of C3 such that

         A2: the ObjectMap of G = ( ~ [:g, g:]);

        take (g * f);

        

        thus the ObjectMap of (G * F) = (the ObjectMap of G * the ObjectMap of F) by Def36

        .= ( ~ ( [:g, g:] * [:f, f:])) by A1, A2, ALTCAT_2: 3

        .= ( ~ [:(g * f), (g * f):]) by FUNCT_3: 71;

      end;

    end

    registration

      let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;

      let F be Contravariant feasible FunctorStr over C1, C2, G be Contravariant FunctorStr over C2, C3;

      cluster (G * F) -> Covariant;

      correctness

      proof

        the ObjectMap of F is Contravariant by Def13;

        then

        consider f be Function of the carrier of C1, the carrier of C2 such that

         A1: the ObjectMap of F = ( ~ [:f, f:]);

        the ObjectMap of G is Contravariant by Def13;

        then

        consider g be Function of the carrier of C2, the carrier of C3 such that

         A2: the ObjectMap of G = ( ~ [:g, g:]);

        take (g * f);

        

        thus the ObjectMap of (G * F) = (the ObjectMap of G * the ObjectMap of F) by Def36

        .= ( ~ (( ~ [:g, g:]) * [:f, f:])) by A1, A2, ALTCAT_2: 2

        .= ( ~ ( ~ ( [:g, g:] * [:f, f:]))) by ALTCAT_2: 3

        .= ( [:g, g:] * [:f, f:]) by FUNCT_4: 53

        .= [:(g * f), (g * f):] by FUNCT_3: 71;

      end;

    end

    registration

      let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;

      let F be feasible FunctorStr over C1, C2, G be feasible FunctorStr over C2, C3;

      cluster (G * F) -> feasible;

      coherence

      proof

        let o1,o2 be Object of C1 such that

         A1: <^o1, o2^> <> {} ;

        reconsider p1 = ((the ObjectMap of F . (o1,o2)) `1 ), p2 = ((the ObjectMap of F . (o1,o2)) `2 ) as Element of C2 by MCART_1: 10;

        reconsider p1, p2 as Object of C2;

         [o1, o2] in [:the carrier of C1, the carrier of C1:] by ZFMISC_1: 87;

        then

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

        

         A3: (the ObjectMap of F . (o1,o2)) = [p1, p2] by MCART_1: 21;

        

         A4: (the ObjectMap of (G * F) . (o1,o2)) = ((the ObjectMap of G * the ObjectMap of F) . [o1, o2]) by Def36

        .= (the ObjectMap of G . (p1,p2)) by A2, A3, FUNCT_1: 13;

         <^p1, p2^> = (the Arrows of C2 . (p1,p2)) by ALTCAT_1:def 1

        .= (the Arrows of C2 . (the ObjectMap of F . (o1,o2))) by MCART_1: 21;

        then <^p1, p2^> <> {} by A1, Def11;

        hence thesis by A4, Def11;

      end;

    end

    theorem :: FUNCTOR0:32

    for C1 be non empty AltGraph, C2,C3,C4 be non empty reflexive AltGraph, F be feasible FunctorStr over C1, C2, G be feasible FunctorStr over C2, C3, H be FunctorStr over C3, C4 holds ((H * G) * F) = (H * (G * F))

    proof

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

      

       A1: the ObjectMap of ((H * G) * F) = (the ObjectMap of (H * G) * the ObjectMap of F) by Def36

      .= ((the ObjectMap of H * the ObjectMap of G) * the ObjectMap of F) by Def36

      .= (the ObjectMap of H * (the ObjectMap of G * the ObjectMap of F)) by RELAT_1: 36

      .= (the ObjectMap of H * the ObjectMap of (G * F)) by Def36

      .= the ObjectMap of (H * (G * F)) by Def36;

      the MorphMap of ((H * G) * F) = ((the MorphMap of (H * G) * the ObjectMap of F) ** the MorphMap of F) by Def36

      .= ((((the MorphMap of H * the ObjectMap of G) ** the MorphMap of G) * the ObjectMap of F) ** the MorphMap of F) by Def36

      .= ((((the MorphMap of H * the ObjectMap of G) * the ObjectMap of F) ** (the MorphMap of G * the ObjectMap of F)) ** the MorphMap of F) by Th12

      .= (((the MorphMap of H * (the ObjectMap of G * the ObjectMap of F)) ** (the MorphMap of G * the ObjectMap of F)) ** the MorphMap of F) by RELAT_1: 36

      .= (((the MorphMap of H * the ObjectMap of (G * F)) ** (the MorphMap of G * the ObjectMap of F)) ** the MorphMap of F) by Def36

      .= ((the MorphMap of H * the ObjectMap of (G * F)) ** ((the MorphMap of G * the ObjectMap of F) ** the MorphMap of F)) by PBOOLE: 140

      .= ((the MorphMap of H * the ObjectMap of (G * F)) ** the MorphMap of (G * F)) by Def36

      .= the MorphMap of (H * (G * F)) by Def36;

      hence thesis by A1;

    end;

    theorem :: FUNCTOR0:33

    

     Th33: for C1 be non empty AltCatStr, C2,C3 be non empty reflexive AltCatStr, F be feasible reflexive FunctorStr over C1, C2, G be FunctorStr over C2, C3, o be Object of C1 holds ((G * F) . o) = (G . (F . o))

    proof

      let C1 be non empty AltCatStr, C2,C3 be non empty reflexive AltCatStr, F be feasible reflexive FunctorStr over C1, C2, G be FunctorStr over C2, C3, o be Object of C1;

      ( dom the ObjectMap of F) = [:the carrier of C1, the carrier of C1:] by FUNCT_2:def 1;

      then

       A1: [o, o] in ( dom the ObjectMap of F) by ZFMISC_1: 87;

      

      thus ((G * F) . o) = (((the ObjectMap of G * the ObjectMap of F) . (o,o)) `1 ) by Def36

      .= ((the ObjectMap of G . (the ObjectMap of F . [o, o])) `1 ) by A1, FUNCT_1: 13

      .= (G . (F . o)) by Def10;

    end;

    theorem :: FUNCTOR0:34

    

     Th34: for C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph, F be feasible reflexive FunctorStr over C1, C2, G be FunctorStr over C2, C3, o be Object of C1 holds ( Morph-Map ((G * F),o,o)) = (( Morph-Map (G,(F . o),(F . o))) * ( Morph-Map (F,o,o)))

    proof

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

      

       A1: ( dom the MorphMap of G) = [:the carrier of C2, the carrier of C2:] by PARTFUN1:def 2;

      ( rng the ObjectMap of F) c= [:the carrier of C2, the carrier of C2:];

      

      then ( dom (the MorphMap of G * the ObjectMap of F)) = ( dom the ObjectMap of F) by A1, RELAT_1: 27

      .= [:the carrier of C1, the carrier of C1:] by FUNCT_2:def 1;

      then

       A2: [o, o] in ( dom (the MorphMap of G * the ObjectMap of F)) by ZFMISC_1: 87;

      ( dom the MorphMap of F) = [:the carrier of C1, the carrier of C1:] by PARTFUN1:def 2;

      then [o, o] in ( dom the MorphMap of F) by ZFMISC_1: 87;

      then [o, o] in (( dom (the MorphMap of G * the ObjectMap of F)) /\ ( dom the MorphMap of F)) by A2, XBOOLE_0:def 4;

      then

       A3: [o, o] in ( dom ((the MorphMap of G * the ObjectMap of F) ** the MorphMap of F)) by PBOOLE:def 19;

      

       A4: ((the MorphMap of G * the ObjectMap of F) . [o, o]) = (the MorphMap of G . (the ObjectMap of F . (o,o))) by A2, FUNCT_1: 12

      .= ( Morph-Map (G,(F . o),(F . o))) by Def10;

      

      thus ( Morph-Map ((G * F),o,o)) = (((the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o,o)) by Def36

      .= (( Morph-Map (G,(F . o),(F . o))) * ( Morph-Map (F,o,o))) by A3, A4, PBOOLE:def 19;

    end;

    registration

      let C1,C2,C3 be with_units non empty AltCatStr;

      let F be id-preserving feasible reflexive FunctorStr over C1, C2;

      let G be id-preserving FunctorStr over C2, C3;

      cluster (G * F) -> id-preserving;

      coherence

      proof

        let o be Object of C1;

        

         A1: [o, o] in [:the carrier of C1, the carrier of C1:] by ZFMISC_1: 87;

        then [o, o] in ( dom the ObjectMap of F) by FUNCT_2:def 1;

        

        then ((the Arrows of C2 * the ObjectMap of F) . [o, o]) = (the Arrows of C2 . (the ObjectMap of F . (o,o))) by FUNCT_1: 13

        .= (the Arrows of C2 . ((F . o),(F . o))) by Def10

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

        then

         A2: ((the Arrows of C2 * the ObjectMap of F) . [o, o]) <> {} by ALTCAT_2:def 7;

        the MorphMap of F is ManySortedFunction of the Arrows of C1, (the Arrows of C2 * the ObjectMap of F) by Def4;

        then ( Morph-Map (F,o,o)) is Function of (the Arrows of C1 . [o, o]), ((the Arrows of C2 * the ObjectMap of F) . [o, o]) by A1, PBOOLE:def 15;

        

        then

         A3: ( dom ( Morph-Map (F,o,o))) = (the Arrows of C1 . (o,o)) by A2, FUNCT_2:def 1

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

        

        thus (( Morph-Map ((G * F),o,o)) . ( idm o)) = ((( Morph-Map (G,(F . o),(F . o))) * ( Morph-Map (F,o,o))) . ( idm o)) by Th34

        .= (( Morph-Map (G,(F . o),(F . o))) . (( Morph-Map (F,o,o)) . ( idm o))) by A3, ALTCAT_1: 19, FUNCT_1: 13

        .= (( Morph-Map (G,(F . o),(F . o))) . ( idm (F . o))) by Def20

        .= ( idm (G . (F . o))) by Def20

        .= ( idm ((G * F) . o)) by Th33;

      end;

    end

    definition

      let A,C be non empty reflexive AltCatStr;

      let B be non empty SubCatStr of A;

      let F be FunctorStr over A, C;

      :: FUNCTOR0:def37

      func F | B -> FunctorStr over B, C equals (F * ( incl B));

      correctness ;

    end

    begin

    definition

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

      assume

       A1: F is bijective;

      :: FUNCTOR0:def38

      func F " -> strict FunctorStr over B, A means

      : Def38: the ObjectMap of it = (the ObjectMap of F " ) & ex f be ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of F) st f = the MorphMap of F & the MorphMap of it = ((f "" ) * (the ObjectMap of F " ));

      existence

      proof

        set OF = the ObjectMap of F;

        F is injective by A1;

        then F is one-to-one;

        then

         A2: OF is one-to-one;

        F is surjective by A1;

        then F is onto;

        then OF is onto;

        then

         A3: ( rng OF) = [:the carrier of B, the carrier of B:];

        then

        reconsider OM = (the ObjectMap of F " ) as bifunction of the carrier of B, the carrier of A by A2, FUNCT_2: 25;

        reconsider f = the MorphMap of F as ManySortedFunction of the Arrows of A, (the Arrows of B * OF) by Def4;

        ((the Arrows of B * OF) * OM) = (the Arrows of B * (OF * OM)) by RELAT_1: 36

        .= (the Arrows of B * ( id [:the carrier of B, the carrier of B:])) by A2, A3, FUNCT_2: 29

        .= the Arrows of B by Th2;

        then ((f "" ) * OM) is ManySortedFunction of the Arrows of B, (the Arrows of A * OM) by ALTCAT_2: 5;

        then

        reconsider MM = ((f "" ) * OM) as MSUnTrans of OM, the Arrows of B, the Arrows of A by Def4;

        take G = FunctorStr (# OM, MM #);

        thus the ObjectMap of G = (OF " );

        take f;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: FUNCTOR0:35

    

     Th35: for A,B be transitive with_units non empty AltCatStr, F be feasible FunctorStr over A, B st F is bijective holds (F " ) is bijective feasible

    proof

      let A,B be transitive with_units non empty AltCatStr;

      let F be feasible FunctorStr over A, B such that

       A1: F is bijective;

      set G = (F " );

      

       A2: the ObjectMap of G = (the ObjectMap of F " ) by A1, Def38;

      

       A3: F is injective by A1;

      then F is one-to-one;

      then

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

      hence the ObjectMap of G is one-to-one by A2;

      F is faithful by A3;

      then

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

      

       A6: F is surjective by A1;

      then F is onto;

      then

       A7: the ObjectMap of F is onto;

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

       A8: h = the MorphMap of F and

       A9: the MorphMap of G = ((h "" ) * (the ObjectMap of F " )) by A1, Def38;

      F is full by A6;

      then

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

      set AA = [:the carrier of A, the carrier of A:], BB = [:the carrier of B, the carrier of B:];

      

       A11: ( rng the ObjectMap of F) = BB by A7;

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

      f is "1-1"

      proof

        let i be set, g be Function such that

         A12: i in ( dom f) and

         A13: (f . i) = g;

        i in BB by A12;

        then

         A14: i in ( dom (the ObjectMap of F " )) by A4, A11, FUNCT_1: 33;

        then ((the ObjectMap of F " ) . i) in ( rng (the ObjectMap of F " )) by FUNCT_1:def 3;

        then

         A15: ((the ObjectMap of F " ) . i) in ( dom the ObjectMap of F) by A4, FUNCT_1: 33;

        then ((the ObjectMap of F " ) . i) in AA;

        then ((the ObjectMap of F " ) . i) in ( dom h) by PARTFUN1:def 2;

        then

         A16: (h . ((the ObjectMap of F " ) . i)) is one-to-one by A5, A8;

        g = ((h "" ) . ((the ObjectMap of F " ) . i)) by A9, A13, A14, FUNCT_1: 13

        .= ((h . ((the ObjectMap of F " ) . i)) " ) by A5, A8, A10, A15, MSUALG_3:def 4;

        hence thesis by A16;

      end;

      hence the MorphMap of G is "1-1";

      thus G is full

      proof

        take f;

        thus f = the MorphMap of G;

        let i be set;

        assume

         A17: i in BB;

        then

         A18: i in ( dom the ObjectMap of G) by FUNCT_2:def 1;

        

         A19: i in ( dom (the ObjectMap of F " )) by A4, A11, A17, FUNCT_1: 33;

        then ((the ObjectMap of F " ) . i) in ( rng (the ObjectMap of F " )) by FUNCT_1:def 3;

        then

         A20: ((the ObjectMap of F " ) . i) in ( dom the ObjectMap of F) by A4, FUNCT_1: 33;

        then ((the ObjectMap of F " ) . i) in AA;

        then (the ObjectMap of G . i) in ( dom h) by A2, PARTFUN1:def 2;

        then

         A21: (h . (the ObjectMap of G . i)) is one-to-one by A5, A8;

        set j = (the ObjectMap of G . i);

        

         A22: (h . j) is Function of (the Arrows of A . j), ((the Arrows of B * the ObjectMap of F) . j) by A2, A20, PBOOLE:def 15;

        consider o1,o2 be Element of A such that

         A23: j = [o1, o2] by A2, A20, DOMAIN_1: 1;

        reconsider o1, o2 as Object of A;

         A24:

        now

          assume (the Arrows of A . j) <> {} ;

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

          then <^o1, o2^> <> {} by ALTCAT_1:def 1;

          then (the Arrows of B . (the ObjectMap of F . (o1,o2))) <> {} by Def11;

          hence ((the Arrows of B * the ObjectMap of F) . j) <> {} by A2, A20, A23, FUNCT_1: 13;

        end;

        (f . i) = ((h "" ) . ((the ObjectMap of F " ) . i)) by A9, A19, FUNCT_1: 13

        .= ((h . ((the ObjectMap of F " ) . i)) " ) by A5, A8, A10, A20, MSUALG_3:def 4;

        

        hence ( rng (f . i)) = ( dom (h . (the ObjectMap of G . i))) by A2, A21, FUNCT_1: 33

        .= (the Arrows of A . (the ObjectMap of G . i)) by A22, A24, FUNCT_2:def 1

        .= ((the Arrows of A * the ObjectMap of G) . i) by A18, FUNCT_1: 13;

      end;

      

      thus ( rng the ObjectMap of G) = ( dom the ObjectMap of F) by A2, A4, FUNCT_1: 33

      .= AA by FUNCT_2:def 1;

      let o1,o2 be Object of B;

      assume <^o1, o2^> <> {} ;

      then

       A25: (the Arrows of B . (o1,o2)) <> {} by ALTCAT_1:def 1;

      

       A26: [o1, o2] in BB by ZFMISC_1: 87;

      then

      consider p1,p2 be Element of A such that

       A27: (the ObjectMap of G . [o1, o2]) = [p1, p2] by DOMAIN_1: 1, FUNCT_2: 5;

      reconsider p1, p2 as Object of A;

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

      

      then

       A28: (the ObjectMap of F . (p1,p2)) = ((the ObjectMap of F * the ObjectMap of G) . [o1, o2]) by A27, FUNCT_1: 13

      .= (( id BB) . [o1, o2]) by A2, A4, A11, FUNCT_1: 39

      .= [o1, o2] by A26, FUNCT_1: 18;

      assume

       A29: (the Arrows of A . (the ObjectMap of G . (o1,o2))) = {} ;

      

       A30: [p1, p2] in AA by ZFMISC_1: 87;

      then

       A31: [p1, p2] in ( dom the ObjectMap of F) by FUNCT_2:def 1;

      (h . [p1, p2]) is Function of (the Arrows of A . [p1, p2]), ((the Arrows of B * the ObjectMap of F) . [p1, p2]) by A30, PBOOLE:def 15;

      

      then {} = ( rng (h . [p1, p2])) by A27, A29

      .= ((the Arrows of B * the ObjectMap of F) . [p1, p2]) by A8, A10, A30

      .= (the Arrows of B . [o1, o2]) by A28, A31, FUNCT_1: 13;

      hence contradiction by A25;

    end;

    theorem :: FUNCTOR0:36

    

     Th36: for A,B be transitive with_units non empty AltCatStr, F be feasible reflexive FunctorStr over A, B st F is bijective coreflexive holds (F " ) is reflexive

    proof

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

       A1: F is bijective and

       A2: F is coreflexive;

      set G = (F " );

      

       A3: the ObjectMap of G = (the ObjectMap of F " ) by A1, Def38;

      let o be Object of B;

      

       A4: ( dom the ObjectMap of F) = [:the carrier of A, the carrier of A:] by FUNCT_2:def 1;

      consider p be Object of A such that

       A5: o = (F . p) by A2, Th20;

      F is injective by A1;

      then F is one-to-one;

      then

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

      

       A7: [p, p] in ( dom the ObjectMap of F) by A4, ZFMISC_1: 87;

      

       A8: (G . (F . p)) = ((G * F) . p) by Th33

      .= (((the ObjectMap of G * the ObjectMap of F) . (p,p)) `1 ) by Def36

      .= ((( id ( dom the ObjectMap of F)) . [p, p]) `1 ) by A3, A6, FUNCT_1: 39

      .= ( [p, p] `1 ) by A7, FUNCT_1: 18

      .= p;

      

      thus (the ObjectMap of G . (o,o)) = (the ObjectMap of G . (the ObjectMap of F . (p,p))) by A5, Def10

      .= ((the ObjectMap of G * the ObjectMap of F) . [p, p]) by A7, FUNCT_1: 13

      .= (( id ( dom the ObjectMap of F)) . [p, p]) by A3, A6, FUNCT_1: 39

      .= [(G . o), (G . o)] by A5, A7, A8, FUNCT_1: 18;

    end;

    theorem :: FUNCTOR0:37

    

     Th37: for A,B be transitive with_units non empty AltCatStr, F be feasible reflexive id-preserving FunctorStr over A, B st F is bijective coreflexive holds (F " ) is id-preserving

    proof

      let A,B be transitive with_units non empty AltCatStr, F be feasible reflexive id-preserving FunctorStr over A, B such that

       A1: F is bijective coreflexive;

      set G = (F " );

      reconsider H = G as feasible reflexive FunctorStr over B, A by A1, Th35, Th36;

      

       A2: the ObjectMap of G = (the ObjectMap of F " ) by A1, Def38;

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

       A3: f = the MorphMap of F and

       A4: the MorphMap of G = ((f "" ) * (the ObjectMap of F " )) by A1, Def38;

      let o be Object of B;

      

       A5: F is injective by A1;

      then F is one-to-one;

      then

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

      F is faithful by A5;

      then

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

      F is surjective by A1;

      then F is full;

      then

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

      

       A9: [(G . o), (G . o)] in [:the carrier of A, the carrier of A:] by ZFMISC_1: 87;

      

       A10: [o, o] in [:the carrier of B, the carrier of B:] by ZFMISC_1: 87;

      then

       A11: [o, o] in ( dom the ObjectMap of G) by FUNCT_2:def 1;

      

       A12: (the ObjectMap of (F * H) . (o,o)) = ((the ObjectMap of F * the ObjectMap of H) . [o, o]) by Def36

      .= ((the ObjectMap of F * (the ObjectMap of F " )) . [o, o]) by A1, Def38

      .= (( id ( rng the ObjectMap of F)) . [o, o]) by A6, FUNCT_1: 39

      .= (( id ( dom the ObjectMap of G)) . [o, o]) by A2, A6, FUNCT_1: 33

      .= (( id [:the carrier of B, the carrier of B:]) . [o, o]) by FUNCT_2:def 1

      .= [o, o] by A10, FUNCT_1: 18;

      

       A13: (F . (G . o)) = ((F * H) . o) by Th33

      .= o by A12;

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

      then [(G . o), (G . o)] in ( dom the MorphMap of F) by ZFMISC_1: 87;

      then

       A14: ( Morph-Map (F,(G . o),(G . o))) is one-to-one by A7;

       [(G . o), (G . o)] in ( dom the ObjectMap of F) by A9, FUNCT_2:def 1;

      

      then ((the Arrows of B * the ObjectMap of F) . [(G . o), (G . o)]) = (the Arrows of B . (the ObjectMap of F . ((G . o),(G . o)))) by FUNCT_1: 13

      .= (the Arrows of B . ((F . (G . o)),(F . (G . o)))) by Def10;

      then

       A15: ((the Arrows of B * the ObjectMap of F) . [(G . o), (G . o)]) <> {} by ALTCAT_2:def 6;

      ( Morph-Map (F,(G . o),(G . o))) is Function of (the Arrows of A . [(G . o), (G . o)]), ((the Arrows of B * the ObjectMap of F) . [(G . o), (G . o)]) by A3, A9, PBOOLE:def 15;

      

      then

       A16: ( dom ( Morph-Map (F,(G . o),(G . o)))) = (the Arrows of A . ((G . o),(G . o))) by A15, FUNCT_2:def 1

      .= <^(G . o), (G . o)^> by ALTCAT_1:def 1;

      ((the Arrows of A * the ObjectMap of G) . [o, o]) = (the Arrows of A . (the ObjectMap of H . (o,o))) by A11, FUNCT_1: 13

      .= (the Arrows of A . ((G . o),(G . o))) by Def10;

      then

       A17: ((the Arrows of A * the ObjectMap of G) . [o, o]) <> {} by ALTCAT_2:def 6;

      the MorphMap of G is ManySortedFunction of the Arrows of B, (the Arrows of A * the ObjectMap of G) by Def4;

      then ( Morph-Map (G,o,o)) is Function of (the Arrows of B . [o, o]), ((the Arrows of A * the ObjectMap of G) . [o, o]) by A10, PBOOLE:def 15;

      

      then

       A18: ( dom ( Morph-Map (G,o,o))) = (the Arrows of B . (o,o)) by A17, FUNCT_2:def 1

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

      then

       A19: ( idm o) in ( dom ( Morph-Map (G,o,o))) by ALTCAT_1: 19;

      

       A20: ( Morph-Map (G,o,o)) = ((f "" ) . (the ObjectMap of G . (o,o))) by A2, A4, A11, FUNCT_1: 13

      .= ((f "" ) . [(H . o), (H . o)]) by Def10

      .= (( Morph-Map (F,(G . o),(G . o))) " ) by A3, A7, A8, A9, MSUALG_3:def 4;

      (( Morph-Map (G,o,o)) . ( idm o)) in ( rng ( Morph-Map (G,o,o))) by A19, FUNCT_1:def 3;

      then

       A21: (( Morph-Map (G,o,o)) . ( idm o)) in ( dom ( Morph-Map (F,(G . o),(G . o)))) by A14, A20, FUNCT_1: 33;

      (( Morph-Map (F,(G . o),(G . o))) . (( Morph-Map (G,o,o)) . ( idm o))) = ((( Morph-Map (F,(G . o),(G . o))) * ( Morph-Map (G,o,o))) . ( idm o)) by A18, ALTCAT_1: 19, FUNCT_1: 13

      .= (( id ( rng ( Morph-Map (F,(G . o),(G . o))))) . ( idm o)) by A14, A20, FUNCT_1: 39

      .= (( id ( dom ( Morph-Map (G,o,o)))) . ( idm o)) by A14, A20, FUNCT_1: 33

      .= ( idm (F . (G . o))) by A13, A18

      .= (( Morph-Map (F,(G . o),(G . o))) . ( idm (G . o))) by Def20;

      hence thesis by A14, A16, A21;

    end;

    theorem :: FUNCTOR0:38

    

     Th38: for A,B be transitive with_units non empty AltCatStr, F be feasible FunctorStr over A, B st F is bijective Covariant holds (F " ) is Covariant

    proof

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

      assume

       A1: F is bijective Covariant;

      then F is injective;

      then F is one-to-one;

      then

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

      F is surjective by A1;

      then F is onto;

      then

       A3: the ObjectMap of F is onto;

      the ObjectMap of F is Covariant by A1;

      then

      consider f be Function of the carrier of A, the carrier of B such that

       A4: the ObjectMap of F = [:f, f:];

      

       A5: f is one-to-one by A2, A4, Th7;

      then

       A6: ( dom (f " )) = ( rng f) by FUNCT_1: 33;

      

       A7: ( rng (f " )) = ( dom f) by A5, FUNCT_1: 33;

      

       A8: ( rng [:f, f:]) = [:the carrier of B, the carrier of B:] by A3, A4;

      ( rng [:f, f:]) = [:( rng f), ( rng f):] by FUNCT_3: 67;

      then ( rng f) = the carrier of B by A8, ZFMISC_1: 92;

      then

      reconsider g = (f " ) as Function of the carrier of B, the carrier of A by A6, A7, FUNCT_2:def 1, RELSET_1: 4;

      take g;

      ( [:f, f:] " ) = [:g, g:] by A5, Th6;

      hence thesis by A1, A4, Def38;

    end;

    theorem :: FUNCTOR0:39

    

     Th39: for A,B be transitive with_units non empty AltCatStr, F be feasible FunctorStr over A, B st F is bijective Contravariant holds (F " ) is Contravariant

    proof

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

      assume

       A1: F is bijective Contravariant;

      then F is injective;

      then F is one-to-one;

      then

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

      F is surjective by A1;

      then F is onto;

      then

       A3: the ObjectMap of F is onto;

      the ObjectMap of F is Contravariant by A1;

      then

      consider f be Function of the carrier of A, the carrier of B such that

       A4: the ObjectMap of F = ( ~ [:f, f:]);

       [:f, f:] is one-to-one by A2, A4, Th9;

      then

       A5: f is one-to-one by Th7;

      then

       A6: ( dom (f " )) = ( rng f) by FUNCT_1: 33;

      

       A7: ( rng (f " )) = ( dom f) by A5, FUNCT_1: 33;

       [:f, f:] is onto by A3, A4, Th13;

      then

       A8: ( rng [:f, f:]) = [:the carrier of B, the carrier of B:];

      ( rng [:f, f:]) = [:( rng f), ( rng f):] by FUNCT_3: 67;

      then ( rng f) = the carrier of B by A8, ZFMISC_1: 92;

      then

      reconsider g = (f " ) as Function of the carrier of B, the carrier of A by A6, A7, FUNCT_2:def 1, RELSET_1: 4;

      take g;

      

       A9: ( [:f, f:] " ) = [:g, g:] by A5, Th6;

      

      thus the ObjectMap of (F " ) = (the ObjectMap of F " ) by A1, Def38

      .= ( ~ [:g, g:]) by A4, A5, A9, Th10;

    end;

    theorem :: FUNCTOR0:40

    

     Th40: for A,B be transitive with_units non empty AltCatStr, F be feasible reflexive FunctorStr over A, B st F is bijective coreflexive Covariant holds for o1,o2 be Object of B, m be Morphism of o1, o2 st <^o1, o2^> <> {} holds (( Morph-Map (F,((F " ) . o1),((F " ) . o2))) . (( Morph-Map ((F " ),o1,o2)) . m)) = m

    proof

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

       A1: F is bijective coreflexive Covariant;

      set G = (F " );

      

       A2: G is Covariant by A1, Th38;

      reconsider H = G as feasible reflexive FunctorStr over B, A by A1, Th35, Th36;

      

       A3: the ObjectMap of G = (the ObjectMap of F " ) by A1, Def38;

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

       A4: f = the MorphMap of F and

       A5: the MorphMap of G = ((f "" ) * (the ObjectMap of F " )) by A1, Def38;

      F is injective by A1;

      then F is faithful;

      then

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

      F is surjective by A1;

      then F is full;

      then

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

      let o1,o2 be Object of B, m be Morphism of o1, o2 such that

       A8: <^o1, o2^> <> {} ;

      

       A9: [(G . o1), (G . o2)] in [:the carrier of A, the carrier of A:] by ZFMISC_1: 87;

      

       A10: [o1, o2] in [:the carrier of B, the carrier of B:] by ZFMISC_1: 87;

      then

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

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

      then [(G . o1), (G . o2)] in ( dom the MorphMap of F) by ZFMISC_1: 87;

      then

       A12: ( Morph-Map (F,(G . o1),(G . o2))) is one-to-one by A6;

      ((the Arrows of A * the ObjectMap of G) . [o1, o2]) = (the Arrows of A . (the ObjectMap of H . (o1,o2))) by A11, FUNCT_1: 13

      .= (the Arrows of A . ((H . o1),(H . o2))) by A2, Th22

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

      then

       A13: ((the Arrows of A * the ObjectMap of G) . [o1, o2]) <> {} by A2, A8, Def18;

      the MorphMap of G is ManySortedFunction of the Arrows of B, (the Arrows of A * the ObjectMap of G) by Def4;

      then ( Morph-Map (G,o1,o2)) is Function of (the Arrows of B . [o1, o2]), ((the Arrows of A * the ObjectMap of G) . [o1, o2]) by A10, PBOOLE:def 15;

      

      then

       A14: ( dom ( Morph-Map (G,o1,o2))) = (the Arrows of B . (o1,o2)) by A13, FUNCT_2:def 1

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

      

       A15: ( Morph-Map (G,o1,o2)) = ((f "" ) . (the ObjectMap of G . (o1,o2))) by A3, A5, A11, FUNCT_1: 13

      .= ((f "" ) . [(H . o1), (H . o2)]) by A2, Th22

      .= (( Morph-Map (F,(G . o1),(G . o2))) " ) by A4, A6, A7, A9, MSUALG_3:def 4;

      

      thus (( Morph-Map (F,(G . o1),(G . o2))) . (( Morph-Map (G,o1,o2)) . m)) = ((( Morph-Map (F,(G . o1),(G . o2))) * ( Morph-Map (G,o1,o2))) . m) by A8, A14, FUNCT_1: 13

      .= (( id ( rng ( Morph-Map (F,(G . o1),(G . o2))))) . m) by A12, A15, FUNCT_1: 39

      .= (( id ( dom ( Morph-Map (G,o1,o2)))) . m) by A12, A15, FUNCT_1: 33

      .= m by A14;

    end;

    theorem :: FUNCTOR0:41

    

     Th41: for A,B be transitive with_units non empty AltCatStr, F be feasible reflexive FunctorStr over A, B st F is bijective coreflexive Contravariant holds for o1,o2 be Object of B, m be Morphism of o1, o2 st <^o1, o2^> <> {} holds (( Morph-Map (F,((F " ) . o2),((F " ) . o1))) . (( Morph-Map ((F " ),o1,o2)) . m)) = m

    proof

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

       A1: F is bijective coreflexive Contravariant;

      set G = (F " );

      

       A2: G is Contravariant by A1, Th39;

      reconsider H = G as feasible reflexive FunctorStr over B, A by A1, Th35, Th36;

      

       A3: the ObjectMap of G = (the ObjectMap of F " ) by A1, Def38;

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

       A4: f = the MorphMap of F and

       A5: the MorphMap of G = ((f "" ) * (the ObjectMap of F " )) by A1, Def38;

      F is injective by A1;

      then F is faithful;

      then

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

      F is surjective by A1;

      then F is full;

      then

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

      let o1,o2 be Object of B, m be Morphism of o1, o2 such that

       A8: <^o1, o2^> <> {} ;

      

       A9: [(G . o2), (G . o1)] in [:the carrier of A, the carrier of A:] by ZFMISC_1: 87;

      

       A10: [o1, o2] in [:the carrier of B, the carrier of B:] by ZFMISC_1: 87;

      then

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

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

      then [(G . o2), (G . o1)] in ( dom the MorphMap of F) by ZFMISC_1: 87;

      then

       A12: ( Morph-Map (F,(G . o2),(G . o1))) is one-to-one by A6;

      ((the Arrows of A * the ObjectMap of G) . [o1, o2]) = (the Arrows of A . (the ObjectMap of H . (o1,o2))) by A11, FUNCT_1: 13

      .= (the Arrows of A . ((H . o2),(H . o1))) by A2, Th23

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

      then

       A13: ((the Arrows of A * the ObjectMap of G) . [o1, o2]) <> {} by A2, A8, Def19;

      the MorphMap of G is ManySortedFunction of the Arrows of B, (the Arrows of A * the ObjectMap of G) by Def4;

      then ( Morph-Map (G,o1,o2)) is Function of (the Arrows of B . [o1, o2]), ((the Arrows of A * the ObjectMap of G) . [o1, o2]) by A10, PBOOLE:def 15;

      

      then

       A14: ( dom ( Morph-Map (G,o1,o2))) = (the Arrows of B . (o1,o2)) by A13, FUNCT_2:def 1

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

      

       A15: ( Morph-Map (G,o1,o2)) = ((f "" ) . (the ObjectMap of G . (o1,o2))) by A3, A5, A11, FUNCT_1: 13

      .= ((f "" ) . [(H . o2), (H . o1)]) by A2, Th23

      .= (( Morph-Map (F,(G . o2),(G . o1))) " ) by A4, A6, A7, A9, MSUALG_3:def 4;

      

      thus (( Morph-Map (F,((F " ) . o2),((F " ) . o1))) . (( Morph-Map ((F " ),o1,o2)) . m)) = ((( Morph-Map (F,(G . o2),(G . o1))) * ( Morph-Map (G,o1,o2))) . m) by A8, A14, FUNCT_1: 13

      .= (( id ( rng ( Morph-Map (F,(G . o2),(G . o1))))) . m) by A12, A15, FUNCT_1: 39

      .= (( id ( dom ( Morph-Map (G,o1,o2)))) . m) by A12, A15, FUNCT_1: 33

      .= m by A14;

    end;

    theorem :: FUNCTOR0:42

    

     Th42: for A,B be transitive with_units non empty AltCatStr, F be feasible reflexive FunctorStr over A, B st F is bijective comp-preserving Covariant coreflexive holds (F " ) is comp-preserving

    proof

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

       A1: F is bijective comp-preserving Covariant coreflexive;

      set G = (F " );

      

       A2: G is Covariant by A1, Th38;

      reconsider H = G as feasible reflexive FunctorStr over B, A by A1, Th35, Th36;

      

       A3: the ObjectMap of G = (the ObjectMap of F " ) by A1, Def38;

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

       A4: ff = the MorphMap of F and

       A5: the MorphMap of G = ((ff "" ) * (the ObjectMap of F " )) by A1, Def38;

      

       A6: F is injective by A1;

      then F is one-to-one;

      then

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

      F is faithful by A6;

      then

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

      F is surjective by A1;

      then F is full;

      then

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

      let o1,o2,o3 be Object of B;

      assume

       A10: <^o1, o2^> <> {} ;

      then

       A11: <^(H . o1), (H . o2)^> <> {} by A2, Def18;

      assume

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

      then

       A13: <^(H . o2), (H . o3)^> <> {} by A2, Def18;

      

       A14: <^o1, o3^> <> {} by A10, A12, ALTCAT_1:def 2;

      then

       A15: <^(H . o1), (H . o3)^> <> {} by A2, Def18;

      then

       A16: <^(F . (G . o1)), (F . (G . o3))^> <> {} by A1, Def18;

      let f be Morphism of o1, o2, g be Morphism of o2, o3;

      reconsider K = G as Covariant FunctorStr over B, A by A1, Th38;

      (K . f) = (( Morph-Map (K,o1,o2)) . f) by A10, A11, Def15;

      then

      reconsider f9 = (( Morph-Map (K,o1,o2)) . f) as Morphism of (G . o1), (G . o2);

      (K . g) = (( Morph-Map (K,o2,o3)) . g) by A12, A13, Def15;

      then

      reconsider g9 = (( Morph-Map (K,o2,o3)) . g) as Morphism of (G . o2), (G . o3);

      take f9, g9;

      thus f9 = (( Morph-Map (G,o1,o2)) . f);

      thus g9 = (( Morph-Map (G,o2,o3)) . g);

      consider f99 be Morphism of (F . (G . o1)), (F . (G . o2)), g99 be Morphism of (F . (G . o2)), (F . (G . o3)) such that

       A17: f99 = (( Morph-Map (F,(G . o1),(G . o2))) . f9) and

       A18: g99 = (( Morph-Map (F,(G . o2),(G . o3))) . g9) and

       A19: (( Morph-Map (F,(G . o1),(G . o3))) . (g9 * f9)) = (g99 * f99) by A1, A11, A13;

      

       A20: g = g99 by A1, A12, A18, Th40;

      

       A21: f = f99 by A1, A10, A17, Th40;

      

       A22: [(G . o1), (G . o3)] in [:the carrier of A, the carrier of A:] by ZFMISC_1: 87;

      

       A23: [o1, o3] in [:the carrier of B, the carrier of B:] by ZFMISC_1: 87;

      then

       A24: [o1, o3] in ( dom the ObjectMap of G) by FUNCT_2:def 1;

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

      then [(G . o1), (G . o3)] in ( dom the MorphMap of F) by ZFMISC_1: 87;

      then

       A25: ( Morph-Map (F,(G . o1),(G . o3))) is one-to-one by A8;

       [(G . o1), (G . o3)] in ( dom the ObjectMap of F) by A22, FUNCT_2:def 1;

      

      then

       A26: ((the Arrows of B * the ObjectMap of F) . [(G . o1), (G . o3)]) = (the Arrows of B . (the ObjectMap of F . ((G . o1),(G . o3)))) by FUNCT_1: 13

      .= (the Arrows of B . ((F . (G . o1)),(F . (G . o3)))) by A1, Th22

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

      ( Morph-Map (F,(G . o1),(G . o3))) is Function of (the Arrows of A . [(G . o1), (G . o3)]), ((the Arrows of B * the ObjectMap of F) . [(G . o1), (G . o3)]) by A4, A22, PBOOLE:def 15;

      

      then

       A27: ( dom ( Morph-Map (F,(G . o1),(G . o3)))) = (the Arrows of A . ((G . o1),(G . o3))) by A16, A26, FUNCT_2:def 1

      .= <^(G . o1), (G . o3)^> by ALTCAT_1:def 1;

      

       A28: ((the Arrows of A * the ObjectMap of G) . [o1, o3]) = (the Arrows of A . (the ObjectMap of H . (o1,o3))) by A24, FUNCT_1: 13

      .= (the Arrows of A . ((G . o1),(G . o3))) by A2, Th22

      .= <^(G . o1), (G . o3)^> by ALTCAT_1:def 1;

      the MorphMap of G is ManySortedFunction of the Arrows of B, (the Arrows of A * the ObjectMap of G) by Def4;

      then ( Morph-Map (G,o1,o3)) is Function of (the Arrows of B . [o1, o3]), ((the Arrows of A * the ObjectMap of G) . [o1, o3]) by A23, PBOOLE:def 15;

      

      then

       A29: ( dom ( Morph-Map (G,o1,o3))) = (the Arrows of B . (o1,o3)) by A15, A28, FUNCT_2:def 1

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

      

       A30: ( Morph-Map (G,o1,o3)) = ((ff "" ) . (the ObjectMap of G . (o1,o3))) by A3, A5, A24, FUNCT_1: 13

      .= ((ff "" ) . [(H . o1), (H . o3)]) by A2, Th22

      .= (( Morph-Map (F,(G . o1),(G . o3))) " ) by A4, A8, A9, A22, MSUALG_3:def 4;

      

       A31: the ObjectMap of (F * H) = (the ObjectMap of F * the ObjectMap of H) by Def36

      .= (the ObjectMap of F * (the ObjectMap of F " )) by A1, Def38

      .= ( id ( rng the ObjectMap of F)) by A7, FUNCT_1: 39

      .= ( id ( dom the ObjectMap of G)) by A3, A7, FUNCT_1: 33

      .= ( id [:the carrier of B, the carrier of B:]) by FUNCT_2:def 1;

       [o1, o1] in [:the carrier of B, the carrier of B:] by ZFMISC_1: 87;

      then

       A32: (the ObjectMap of (F * H) . (o1,o1)) = [o1, o1] by A31, FUNCT_1: 18;

      

       A33: (F . (G . o1)) = ((F * H) . o1) by Th33

      .= o1 by A32;

       [o2, o2] in [:the carrier of B, the carrier of B:] by ZFMISC_1: 87;

      then

       A34: (the ObjectMap of (F * H) . (o2,o2)) = [o2, o2] by A31, FUNCT_1: 18;

      

       A35: (F . (G . o2)) = ((F * H) . o2) by Th33

      .= o2 by A34;

       [o3, o3] in [:the carrier of B, the carrier of B:] by ZFMISC_1: 87;

      then

       A36: (the ObjectMap of (F * H) . (o3,o3)) = [o3, o3] by A31, FUNCT_1: 18;

      

       A37: (F . (G . o3)) = ((F * H) . o3) by Th33

      .= o3 by A36;

      (( Morph-Map (G,o1,o3)) . (g * f)) in ( rng ( Morph-Map (G,o1,o3))) by A14, A29, FUNCT_1:def 3;

      then

       A38: (( Morph-Map (G,o1,o3)) . (g * f)) in ( dom ( Morph-Map (F,(G . o1),(G . o3)))) by A25, A30, FUNCT_1: 33;

      (( Morph-Map (F,(G . o1),(G . o3))) . (( Morph-Map (G,o1,o3)) . (g * f))) = (( Morph-Map (F,(G . o1),(G . o3))) . (g9 * f9)) by A1, A14, A19, A20, A21, A33, A35, A37, Th40;

      hence thesis by A25, A27, A38;

    end;

    theorem :: FUNCTOR0:43

    

     Th43: for A,B be transitive with_units non empty AltCatStr, F be feasible reflexive FunctorStr over A, B st F is bijective comp-reversing Contravariant coreflexive holds (F " ) is comp-reversing

    proof

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

       A1: F is bijective comp-reversing Contravariant coreflexive;

      set G = (F " );

      

       A2: G is Contravariant by A1, Th39;

      reconsider H = G as feasible reflexive FunctorStr over B, A by A1, Th35, Th36;

      

       A3: the ObjectMap of G = (the ObjectMap of F " ) by A1, Def38;

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

       A4: ff = the MorphMap of F and

       A5: the MorphMap of G = ((ff "" ) * (the ObjectMap of F " )) by A1, Def38;

      

       A6: F is injective by A1;

      then F is one-to-one;

      then

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

      F is faithful by A6;

      then

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

      F is surjective by A1;

      then F is full;

      then

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

      let o1,o2,o3 be Object of B;

      assume

       A10: <^o1, o2^> <> {} ;

      then

       A11: <^(H . o2), (H . o1)^> <> {} by A2, Def19;

      assume

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

      then

       A13: <^(H . o3), (H . o2)^> <> {} by A2, Def19;

      

       A14: <^o1, o3^> <> {} by A10, A12, ALTCAT_1:def 2;

      then

       A15: <^(H . o3), (H . o1)^> <> {} by A2, Def19;

      then

       A16: <^(F . (G . o1)), (F . (G . o3))^> <> {} by A1, Def19;

      let f be Morphism of o1, o2, g be Morphism of o2, o3;

      reconsider K = G as Contravariant FunctorStr over B, A by A1, Th39;

      (K . f) = (( Morph-Map (K,o1,o2)) . f) by A10, A11, Def16;

      then

      reconsider f9 = (( Morph-Map (K,o1,o2)) . f) as Morphism of (G . o2), (G . o1);

      (K . g) = (( Morph-Map (K,o2,o3)) . g) by A12, A13, Def16;

      then

      reconsider g9 = (( Morph-Map (K,o2,o3)) . g) as Morphism of (G . o3), (G . o2);

      take f9, g9;

      thus f9 = (( Morph-Map (G,o1,o2)) . f);

      thus g9 = (( Morph-Map (G,o2,o3)) . g);

      consider g99 be Morphism of (F . (G . o2)), (F . (G . o3)), f99 be Morphism of (F . (G . o1)), (F . (G . o2)) such that

       A17: g99 = (( Morph-Map (F,(G . o3),(G . o2))) . g9) and

       A18: f99 = (( Morph-Map (F,(G . o2),(G . o1))) . f9) and

       A19: (( Morph-Map (F,(G . o3),(G . o1))) . (f9 * g9)) = (g99 * f99) by A1, A11, A13;

      

       A20: g = g99 by A1, A12, A17, Th41;

      

       A21: f = f99 by A1, A10, A18, Th41;

      

       A22: [(G . o3), (G . o1)] in [:the carrier of A, the carrier of A:] by ZFMISC_1: 87;

      

       A23: [o1, o3] in [:the carrier of B, the carrier of B:] by ZFMISC_1: 87;

      then

       A24: [o1, o3] in ( dom the ObjectMap of G) by FUNCT_2:def 1;

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

      then [(G . o3), (G . o1)] in ( dom the MorphMap of F) by ZFMISC_1: 87;

      then

       A25: ( Morph-Map (F,(G . o3),(G . o1))) is one-to-one by A8;

       [(G . o3), (G . o1)] in ( dom the ObjectMap of F) by A22, FUNCT_2:def 1;

      

      then

       A26: ((the Arrows of B * the ObjectMap of F) . [(G . o3), (G . o1)]) = (the Arrows of B . (the ObjectMap of F . ((G . o3),(G . o1)))) by FUNCT_1: 13

      .= (the Arrows of B . ((F . (G . o1)),(F . (G . o3)))) by A1, Th23

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

      ( Morph-Map (F,(G . o3),(G . o1))) is Function of (the Arrows of A . [(G . o3), (G . o1)]), ((the Arrows of B * the ObjectMap of F) . [(G . o3), (G . o1)]) by A4, A22, PBOOLE:def 15;

      

      then

       A27: ( dom ( Morph-Map (F,(G . o3),(G . o1)))) = (the Arrows of A . ((G . o3),(G . o1))) by A16, A26, FUNCT_2:def 1

      .= <^(G . o3), (G . o1)^> by ALTCAT_1:def 1;

      

       A28: ((the Arrows of A * the ObjectMap of G) . [o1, o3]) = (the Arrows of A . (the ObjectMap of H . (o1,o3))) by A24, FUNCT_1: 13

      .= (the Arrows of A . ((G . o3),(G . o1))) by A2, Th23

      .= <^(G . o3), (G . o1)^> by ALTCAT_1:def 1;

      the MorphMap of G is ManySortedFunction of the Arrows of B, (the Arrows of A * the ObjectMap of G) by Def4;

      then ( Morph-Map (G,o1,o3)) is Function of (the Arrows of B . [o1, o3]), ((the Arrows of A * the ObjectMap of G) . [o1, o3]) by A23, PBOOLE:def 15;

      

      then

       A29: ( dom ( Morph-Map (G,o1,o3))) = (the Arrows of B . (o1,o3)) by A15, A28, FUNCT_2:def 1

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

      

       A30: ( Morph-Map (G,o1,o3)) = ((ff "" ) . (the ObjectMap of G . (o1,o3))) by A3, A5, A24, FUNCT_1: 13

      .= ((ff "" ) . [(H . o3), (H . o1)]) by A2, Th23

      .= (( Morph-Map (F,(G . o3),(G . o1))) " ) by A4, A8, A9, A22, MSUALG_3:def 4;

      

       A31: the ObjectMap of (F * H) = (the ObjectMap of F * the ObjectMap of H) by Def36

      .= (the ObjectMap of F * (the ObjectMap of F " )) by A1, Def38

      .= ( id ( rng the ObjectMap of F)) by A7, FUNCT_1: 39

      .= ( id ( dom the ObjectMap of G)) by A3, A7, FUNCT_1: 33

      .= ( id [:the carrier of B, the carrier of B:]) by FUNCT_2:def 1;

       [o1, o1] in [:the carrier of B, the carrier of B:] by ZFMISC_1: 87;

      then

       A32: (the ObjectMap of (F * H) . (o1,o1)) = [o1, o1] by A31, FUNCT_1: 18;

      

       A33: (F . (G . o1)) = ((F * H) . o1) by Th33

      .= o1 by A32;

       [o2, o2] in [:the carrier of B, the carrier of B:] by ZFMISC_1: 87;

      then

       A34: (the ObjectMap of (F * H) . (o2,o2)) = [o2, o2] by A31, FUNCT_1: 18;

      

       A35: (F . (G . o2)) = ((F * H) . o2) by Th33

      .= o2 by A34;

       [o3, o3] in [:the carrier of B, the carrier of B:] by ZFMISC_1: 87;

      then

       A36: (the ObjectMap of (F * H) . (o3,o3)) = [o3, o3] by A31, FUNCT_1: 18;

      

       A37: (F . (G . o3)) = ((F * H) . o3) by Th33

      .= o3 by A36;

      (( Morph-Map (G,o1,o3)) . (g * f)) in ( rng ( Morph-Map (G,o1,o3))) by A14, A29, FUNCT_1:def 3;

      then

       A38: (( Morph-Map (G,o1,o3)) . (g * f)) in ( dom ( Morph-Map (F,(G . o3),(G . o1)))) by A25, A30, FUNCT_1: 33;

      (( Morph-Map (F,(G . o3),(G . o1))) . (( Morph-Map (G,o1,o3)) . (g * f))) = (( Morph-Map (F,(G . o3),(G . o1))) . (f9 * g9)) by A1, A14, A19, A20, A21, A33, A35, A37, Th41;

      hence thesis by A25, A27, A38;

    end;

    registration

      let C1 be 1-sorted, C2 be non empty 1-sorted;

      cluster Covariant -> reflexive for BimapStr over C1, C2;

      coherence

      proof

        let M be BimapStr over C1, C2;

        assume M is Covariant;

        then the ObjectMap of M is Covariant;

        then ex f be Function of the carrier of C1, the carrier of C2 st the ObjectMap of M = [:f, f:];

        hence (the ObjectMap of M .: ( id the carrier of C1)) c= ( id the carrier of C2) by Th14;

      end;

    end

    registration

      let C1 be 1-sorted, C2 be non empty 1-sorted;

      cluster Contravariant -> reflexive for BimapStr over C1, C2;

      coherence

      proof

        let M be BimapStr over C1, C2;

        assume M is Contravariant;

        then the ObjectMap of M is Contravariant;

        then

        consider f be Function of the carrier of C1, the carrier of C2 such that

         A1: the ObjectMap of M = ( ~ [:f, f:]);

        (( ~ [:f, f:]) .: ( id the carrier of C1)) = ( [:f, f:] .: ( id the carrier of C1)) by Th3;

        hence (the ObjectMap of M .: ( id the carrier of C1)) c= ( id the carrier of C2) by A1, Th14;

      end;

    end

    theorem :: FUNCTOR0:44

    

     Th44: for C1,C2 be 1-sorted, M be BimapStr over C1, C2 st M is Covariant onto holds M is coreflexive

    proof

      let C1,C2 be 1-sorted;

      let M be BimapStr over C1, C2;

      assume

       A1: M is Covariant onto;

      then the ObjectMap of M is Covariant;

      then

      consider f be Function of the carrier of C1, the carrier of C2 such that

       A2: the ObjectMap of M = [:f, f:];

      the ObjectMap of M is onto by A1;

      then f is onto by A2, Th4;

      hence ( id the carrier of C2) c= (the ObjectMap of M .: ( id the carrier of C1)) by A2, Th11;

    end;

    theorem :: FUNCTOR0:45

    

     Th45: for C1,C2 be 1-sorted, M be BimapStr over C1, C2 st M is Contravariant onto holds M is coreflexive

    proof

      let C1,C2 be 1-sorted;

      let M be BimapStr over C1, C2;

      assume

       A1: M is Contravariant onto;

      then the ObjectMap of M is Contravariant;

      then

      consider f be Function of the carrier of C1, the carrier of C2 such that

       A2: the ObjectMap of M = ( ~ [:f, f:]);

      the ObjectMap of M is onto by A1;

      then [:f, f:] is onto by A2, Th13;

      then

       A3: f is onto by Th4;

      (the ObjectMap of M .: ( id the carrier of C1)) = ( [:f, f:] .: ( id the carrier of C1)) by A2, Th3;

      hence ( id the carrier of C2) c= (the ObjectMap of M .: ( id the carrier of C1)) by A3, Th11;

    end;

    registration

      let C1 be transitive with_units non empty AltCatStr, C2 be with_units non empty AltCatStr;

      cluster covariant -> reflexive for Functor of C1, C2;

      coherence ;

    end

    registration

      let C1 be transitive with_units non empty AltCatStr, C2 be with_units non empty AltCatStr;

      cluster contravariant -> reflexive for Functor of C1, C2;

      coherence ;

    end

    theorem :: FUNCTOR0:46

    

     Th46: for C1 be transitive with_units non empty AltCatStr, C2 be with_units non empty AltCatStr, F be Functor of C1, C2 st F is covariant onto holds F is coreflexive by Th44;

    theorem :: FUNCTOR0:47

    

     Th47: for C1 be transitive with_units non empty AltCatStr, C2 be with_units non empty AltCatStr, F be Functor of C1, C2 st F is contravariant onto holds F is coreflexive by Th45;

    theorem :: FUNCTOR0:48

    

     Th48: for A,B be transitive with_units non empty AltCatStr, F be covariant Functor of A, B st F is bijective holds ex G be Functor of B, A st G = (F " ) & G is bijective covariant

    proof

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

      assume

       A1: F is bijective;

      then F is injective;

      then F is one-to-one;

      then

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

      

       A3: F is feasible by Def25;

      then

       A4: (F " ) is bijective feasible by A1, Th35;

      

       A5: F is id-preserving by Def25;

      

       A6: F is comp-preserving by Def26;

      F is surjective by A1;

      then

       A7: F is onto;

      then

       A8: the ObjectMap of F is onto;

      

       A9: F is Covariant by Def26;

      

       A10: F is coreflexive by A7, Th46;

      

       A11: (F " ) is Covariant

      proof

        F is Covariant by Def26;

        then the ObjectMap of F is Covariant;

        then

        consider f be Function of the carrier of A, the carrier of B such that

         A12: the ObjectMap of F = [:f, f:];

        

         A13: f is one-to-one by A2, A12, Th7;

        then

         A14: ( dom (f " )) = ( rng f) by FUNCT_1: 33;

        

         A15: ( rng (f " )) = ( dom f) by A13, FUNCT_1: 33;

        

         A16: ( rng [:f, f:]) = [:the carrier of B, the carrier of B:] by A8, A12;

        ( rng [:f, f:]) = [:( rng f), ( rng f):] by FUNCT_3: 67;

        then ( rng f) = the carrier of B by A16, ZFMISC_1: 92;

        then

        reconsider g = (f " ) as Function of the carrier of B, the carrier of A by A14, A15, FUNCT_2:def 1, RELSET_1: 4;

        take g;

        ( [:f, f:] " ) = [:g, g:] by A13, Th6;

        hence thesis by A1, A12, Def38;

      end;

      

       A17: (F " ) is id-preserving by A1, A3, A5, A10, Th37;

      (F " ) is comp-preserving by A1, A3, A6, A9, A10, Th42;

      then

      reconsider G = (F " ) as Functor of B, A by A4, A11, A17, Def25;

      take G;

      thus G = (F " );

      thus G is bijective by A1, A3, Th35;

      thus G is Covariant by A11;

      thus thesis by A1, A3, A6, A9, A10, Th42;

    end;

    theorem :: FUNCTOR0:49

    

     Th49: for A,B be transitive with_units non empty AltCatStr, F be contravariant Functor of A, B st F is bijective holds ex G be Functor of B, A st G = (F " ) & G is bijective contravariant

    proof

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

      assume

       A1: F is bijective;

      then F is injective;

      then F is one-to-one;

      then

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

      

       A3: F is feasible by Def25;

      then

       A4: (F " ) is bijective feasible by A1, Th35;

      

       A5: F is id-preserving by Def25;

      

       A6: F is comp-reversing by Def27;

      F is surjective by A1;

      then

       A7: F is onto;

      then

       A8: the ObjectMap of F is onto;

      

       A9: F is Contravariant by Def27;

      

       A10: F is coreflexive by A7, Th47;

      

       A11: (F " ) is Contravariant

      proof

        F is Contravariant by Def27;

        then the ObjectMap of F is Contravariant;

        then

        consider f be Function of the carrier of A, the carrier of B such that

         A12: the ObjectMap of F = ( ~ [:f, f:]);

         [:f, f:] is one-to-one by A2, A12, Th9;

        then

         A13: f is one-to-one by Th7;

        then

         A14: ( dom (f " )) = ( rng f) by FUNCT_1: 33;

        

         A15: ( rng (f " )) = ( dom f) by A13, FUNCT_1: 33;

         [:f, f:] is onto by A8, A12, Th13;

        then

         A16: ( rng [:f, f:]) = [:the carrier of B, the carrier of B:];

        ( rng [:f, f:]) = [:( rng f), ( rng f):] by FUNCT_3: 67;

        then ( rng f) = the carrier of B by A16, ZFMISC_1: 92;

        then

        reconsider g = (f " ) as Function of the carrier of B, the carrier of A by A14, A15, FUNCT_2:def 1, RELSET_1: 4;

        take g;

        

         A17: ( [:f, f:] " ) = [:g, g:] by A13, Th6;

        

        thus the ObjectMap of (F " ) = (the ObjectMap of F " ) by A1, Def38

        .= ( ~ [:g, g:]) by A12, A13, A17, Th10;

      end;

      

       A18: (F " ) is id-preserving by A1, A3, A5, A10, Th37;

      (F " ) is comp-reversing by A1, A3, A6, A9, A10, Th43;

      then

      reconsider G = (F " ) as Functor of B, A by A4, A11, A18, Def25;

      take G;

      thus G = (F " );

      thus G is bijective by A1, A3, Th35;

      thus G is Contravariant by A11;

      thus thesis by A1, A3, A6, A9, A10, Th43;

    end;

    definition

      let A,B be transitive with_units non empty AltCatStr;

      :: FUNCTOR0:def39

      pred A,B are_isomorphic means ex F be Functor of A, B st F is bijective covariant;

      reflexivity

      proof

        let A be transitive with_units non empty AltCatStr;

        take ( id A);

        thus thesis;

      end;

      symmetry

      proof

        let A,B be transitive with_units non empty AltCatStr;

        given F be Functor of A, B such that

         A1: F is bijective covariant;

        consider G be Functor of B, A such that G = (F " ) and

         A2: G is bijective covariant by A1, Th48;

        take G;

        thus thesis by A2;

      end;

      :: FUNCTOR0:def40

      pred A,B are_anti-isomorphic means ex F be Functor of A, B st F is bijective contravariant;

      symmetry

      proof

        let A,B be transitive with_units non empty AltCatStr;

        given F be Functor of A, B such that

         A3: F is bijective contravariant;

        consider G be Functor of B, A such that G = (F " ) and

         A4: G is bijective contravariant by A3, Th49;

        take G;

        thus thesis by A4;

      end;

    end