theorem Th4: :: ALTCAT_3:4

for C being category
for o being Object of C holds (idm o) " = idm o