for A, B being Category
for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds
for t being natural_equivalence of F1,F2
for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3