theorem
for
A,
B,
C being
Category for
F1,
F2,
F3 being
Functor of
A,
B for
G1,
G2,
G3 being
Functor of
B,
C for
s being
natural_transformation of
F1,
F2 for
s9 being
natural_transformation of
F2,
F3 for
t being
natural_transformation of
G1,
G2 for
t9 being
natural_transformation of
G2,
G3 st
F1 is_naturally_transformable_to F2 &
F2 is_naturally_transformable_to F3 &
G1 is_naturally_transformable_to G2 &
G2 is_naturally_transformable_to G3 holds
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)