theorem :: FUNCTOR0:32

for C1 being non empty AltGraph
for C2, C3, C4 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being feasible FunctorStr over C2,C3
for H being FunctorStr over C3,C4 holds (H * G) * F = H * (G * F)