theorem Th21: :: ISOCAT_1:23

for A, B, C being Category
for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2
for G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a)