for A, B being Category
for F, F1, F2, F3 being Functor of A,B
for t being natural_transformation of F,F1
for t9 being natural_transformation of F2,F3
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds
( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )