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