theorem :: ISOCAT_1:40

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