theorem
for
A,
B,
C being
category for
F1,
F2,
F3 being
covariant Functor of
A,
B for
G1,
G2,
G3 being
covariant Functor of
B,
C for
s being
natural_transformation of
G1,
G2 for
s1 being
natural_transformation of
G2,
G3 for
t being
transformation of
F1,
F2 for
t1 being
transformation of
F2,
F3 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
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)