theorem Th29: :: ISOCAT_1:31

for A, B, C, D being Category
for F1, F2 being Functor of A,B
for G being Functor of B,C
for H being Functor of C,D
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(H * G) * s = H * (G * s)