theorem Th7: :: FUNCTOR3:7

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