for A, B being Category
for F, F1, F2 being Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2
for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F1,F2],t1] holds
g (*) f = [[F,F2],(t1 `*` t)]