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