theorem Th23: :: ISOCAT_2:25

for A, B, C being Category
for F1, F2, F3 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t1 being natural_transformation of F1,F2
for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1)