theorem Th12: :: ALTCAT_2:12

for C being Category
for i being Object of C holds id i in (the_hom_sets_of C) . (i,i)