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 Th32
.= id (the_carrier_of a) by Th33 ; :: thesis: verum