theorem Th34: :: FUNCTOR0:34

for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being reflexive feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for o being Object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))