for A, B, C, D being Category
for F being Functor of A,B
for G1, G2 being Functor of B,C
for H being Functor of C,D
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
(H * t) * F = H * (t * F)