let A be non empty transitive AltCatStr ; :: thesis: for B, C being non empty with_units AltCatStr

for F being feasible Contravariant FunctorStr over A,B

for G being FunctorStr over B,C

for o, o1 being Object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))

let B, C be non empty with_units AltCatStr ; :: thesis: for F being feasible Contravariant FunctorStr over A,B

for G being FunctorStr over B,C

for o, o1 being Object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))

let F be feasible Contravariant FunctorStr over A,B; :: thesis: for G being FunctorStr over B,C

for o, o1 being Object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))

let G be FunctorStr over B,C; :: thesis: for o, o1 being Object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))

let o, o1 be Object of A; :: thesis: Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))

( dom the MorphMap of G = [: the carrier of B, the carrier of B:] & rng the ObjectMap of F c= [: the carrier of B, the carrier of B:] ) by PARTFUN1:def 2;

then dom ( the MorphMap of G * the ObjectMap of F) = dom the ObjectMap of F by RELAT_1:27

.= [: the carrier of A, the carrier of A:] by FUNCT_2:def 1 ;

then A1: [o,o1] in dom ( the MorphMap of G * the ObjectMap of F) by ZFMISC_1:87;

then A2: ( the MorphMap of G * the ObjectMap of F) . [o,o1] = the MorphMap of G . ( the ObjectMap of F . (o,o1)) by FUNCT_1:12

.= Morph-Map (G,(F . o1),(F . o)) by FUNCTOR0:23 ;

dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def 2;

then [o,o1] in dom the MorphMap of F by ZFMISC_1:87;

then [o,o1] in (dom ( the MorphMap of G * the ObjectMap of F)) /\ (dom the MorphMap of F) by A1, XBOOLE_0:def 4;

then A3: [o,o1] in dom (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) by PBOOLE:def 19;

thus Morph-Map ((G * F),o,o1) = (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o,o1) by FUNCTOR0:def 36

.= (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1)) by A3, A2, PBOOLE:def 19 ; :: thesis: verum

for F being feasible Contravariant FunctorStr over A,B

for G being FunctorStr over B,C

for o, o1 being Object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))

let B, C be non empty with_units AltCatStr ; :: thesis: for F being feasible Contravariant FunctorStr over A,B

for G being FunctorStr over B,C

for o, o1 being Object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))

let F be feasible Contravariant FunctorStr over A,B; :: thesis: for G being FunctorStr over B,C

for o, o1 being Object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))

let G be FunctorStr over B,C; :: thesis: for o, o1 being Object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))

let o, o1 be Object of A; :: thesis: Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))

( dom the MorphMap of G = [: the carrier of B, the carrier of B:] & rng the ObjectMap of F c= [: the carrier of B, the carrier of B:] ) by PARTFUN1:def 2;

then dom ( the MorphMap of G * the ObjectMap of F) = dom the ObjectMap of F by RELAT_1:27

.= [: the carrier of A, the carrier of A:] by FUNCT_2:def 1 ;

then A1: [o,o1] in dom ( the MorphMap of G * the ObjectMap of F) by ZFMISC_1:87;

then A2: ( the MorphMap of G * the ObjectMap of F) . [o,o1] = the MorphMap of G . ( the ObjectMap of F . (o,o1)) by FUNCT_1:12

.= Morph-Map (G,(F . o1),(F . o)) by FUNCTOR0:23 ;

dom the MorphMap of F = [: the carrier of A, the carrier of A:] by PARTFUN1:def 2;

then [o,o1] in dom the MorphMap of F by ZFMISC_1:87;

then [o,o1] in (dom ( the MorphMap of G * the ObjectMap of F)) /\ (dom the MorphMap of F) by A1, XBOOLE_0:def 4;

then A3: [o,o1] in dom (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) by PBOOLE:def 19;

thus Morph-Map ((G * F),o,o1) = (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o,o1) by FUNCTOR0:def 36

.= (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1)) by A3, A2, PBOOLE:def 19 ; :: thesis: verum