theorem Th22: :: ISOCAT_1:24

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