theorem Th37: :: YELLOW18:37

for C being semi-functional para-functional category
for a being Object of C st id (the_carrier_of a) in <^a,a^> holds
idm a = id (the_carrier_of a)