theorem :: FUNCTOR3:42

for A, B being category
for F1, F2, F3 being covariant Functor of A,B
for e being natural_equivalence of F1,F2
for e1 being natural_equivalence of F2,F3
for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
k " = (e ") `*` (e1 ")