theorem Th47: :: ENS_1:48

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