theorem Th2: :: YONEDA_1:2
for A being Category
for f being Morphism of A holds <|(cod f),?> is_naturally_transformable_to <|(dom f),?>