theorem Th9: :: FUNCTOR3:9

for A being non empty AltCatStr
for B, C being non empty reflexive AltCatStr
for G being feasible Covariant FunctorStr over B,C
for M being feasible Contravariant FunctorStr over A,B
for o1, o2 being Object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * M) . m = G . (M . m)