let C be non empty composable with_identities CategoryStr ; :: thesis: for a being Object of C holds a in Hom (a,a)
let a be Object of C; :: thesis: a in Hom (a,a)
a in Ob C ;
then reconsider f = a as morphism of C ;
f is identity by CAT_6:22;
then ( dom f = f & cod f = f ) by Th6;
hence a in Hom (a,a) ; :: thesis: verum