theorem :: CAT_1:27

for C being Category
for a being Object of C holds id a in Hom (a,a) by Def3;