:: deftheorem Def8 defines * ISOCAT_1:def 8 :
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 holds t * F = t * F;