theorem Th72: :: CAT_1:77

for C being Category
for c being Object of C holds (Obj (id C)) . c = c