let a be Object of (EnsCat A); :: according to YELLOW18:def 10 :: thesis: idm a = id (the_carrier_of a)
thus idm a = id a by Th31
.= id (the_carrier_of a) by Th32 ; :: thesis: verum