for C being category
for D being non empty subcategory of C
for o being Object of D
for o9 being Object of C st o = o9 holds
idm o = idm o9