let C be Category; :: thesis: for a being Element of C st C is pseudo-discrete holds
Hom (a,a) = {(id a)}
let a be Element of C; :: thesis: ( C is pseudo-discrete implies Hom (a,a) = {(id a)} )
assume C is pseudo-discrete ; :: thesis: Hom (a,a) = {(id a)}
then ( Hom (a,a) is trivial & not Hom (a,a) is empty ) ;
then consider m being object such that
A1: Hom (a,a) = {m} by ZFMISC_1:131;
id a in Hom (a,a) by CAT_1:27;
hence Hom (a,a) = {(id a)} by A1, TARSKI:def 1; :: thesis: verum