theorem Th13: :: ISOCAT_2:15

for A, B, C being Category
for F being Functor of [:A,B:],C
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds
( F ?- a is_naturally_transformable_to F ?- b & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a,F ?- b )