theorem :: CAT_1:30

for C being Category
for a being Object of C holds (id a) * (id a) = id a ;