theorem Th53: :: CAT_1:58

for C being Category
for a being Object of C holds
( dom (id a) = a & cod (id a) = a ) ;