theorem Th6: :: CAT_7:6

for C being composable with_identities CategoryStr
for f being morphism of C st f is identity holds
( dom f = f & cod f = f )