for A, B being Category
for f being Morphism of (Functors (A,B)) ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( F1 is_naturally_transformable_to F2 & dom f = F1 & cod f = F2 & f = [[F1,F2],t] )