theorem Th34: :: ISOCAT_1:36

for A, B, C being Category
for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
t (#) s = (G2 * s) `*` (t * F1)