theorem
for
A,
B,
C being
category for
F1,
F2 being
covariant Functor of
A,
B for
G1,
G2 being
covariant Functor of
B,
C for
e being
natural_equivalence of
F1,
F2 for
f being
natural_equivalence of
G1,
G2 st
F1,
F2 are_naturally_equivalent &
G1,
G2 are_naturally_equivalent holds
(
G1 * F1,
G2 * F2 are_naturally_equivalent &
f (#) e is
natural_equivalence of
G1 * F1,
G2 * F2 )