theorem Th31: :: CAT_8:31

for C being with_identities CategoryStr
for a being Object of C st a is initial holds
for h being Morphism of a,a holds id- a = h