theorem Th51: :: ENS_1:52

for C being Category
for f, g being Morphism of C holds [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] is Element of Maps (Hom C)