theorem Th17: :: ISOCAT_2:19

for A, B, C being Category
for F being Functor of [:A,B:],C
for g, f being Morphism of A st dom g = cod f holds
for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds
F ?- (g (*) f) = (F ?- g) `*` t