let A be non empty transitive AltCatStr ; :: thesis: for B, C being non empty with_units AltCatStr
for F being feasible Contravariant FunctorStr of A,B
for G being FunctorStr of 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 of A,B
for G being FunctorStr of 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 of A,B; :: thesis: for G being FunctorStr of 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 of 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 4;
then dom (the MorphMap of G * the ObjectMap of F) = dom the ObjectMap of F by RELAT_1:46
.= [: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:106;
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:22
.= Morph-Map G,(F . o1),(F . o) by FUNCTOR0:24 ;
dom the MorphMap of F = [:the carrier of A,the carrier of A:] by PARTFUN1:def 4;
then [o,o1] in dom the MorphMap of F by ZFMISC_1:106;
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 24;
thus Morph-Map (G * F),o,o1 = ((the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . o,o1 by FUNCTOR0:def 37
.= (Morph-Map G,(F . o1),(F . o)) * (Morph-Map F,o,o1) by A3, A2, PBOOLE:def 24 ; :: thesis: verum