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