for A, B being non empty transitive with_units AltCatStr
for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for a being Object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a) by Def5;