for A being non empty transitive AltCatStr
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))