theorem Th31: :: YELLOW18:31

for A being non empty set
for a being Object of (EnsCat A) holds idm a = id a