theorem Th27: :: ISOCAT_1:29

for A, B, C, D being Category
for F being Functor of A,B
for G being Functor of B,C
for H1, H2 being Functor of C,D
for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds
(u * G) * F = u * (G * F)