theorem Th33: :: FUNCTOR0:33

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