theorem Th8: :: FUNCTOR3:8

for A being non empty AltCatStr
for B, C being non empty reflexive AltCatStr
for F being feasible Covariant 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 * F) . m = N . (F . m)