theorem :: CAT_1:79

for C being Category
for c being Object of C holds (id C) . c = c by Th72;