:: deftheorem Def6 defines * ISOCAT_1:def 6 :
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 holds t * F = t * (Obj F);