for A, B being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds
t1 = t2