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

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