theorem Th19: :: ISOCAT_2:21

for A, B, C being Category
for F being Functor of [:A,B:],C
for a being Object of A holds (export F) . a is Functor of B,C