let A be discrete Category; :: thesis: for a being Object of A holds Hom (a,a) = {(id a)}

let a be Object of A; :: thesis: Hom (a,a) = {(id a)}

let a be Object of A; :: thesis: Hom (a,a) = {(id a)}

now :: thesis: for g being Morphism of a,a holds g = id a

hence
Hom (a,a) = {(id a)}
by CAT_1:8; :: thesis: verumlet g be Morphism of a,a; :: thesis: g = id a

( id a in Hom (a,a) & g in Hom (a,a) ) by CAT_1:def 5;

hence g = id a by ZFMISC_1:def 10; :: thesis: verum

end;( id a in Hom (a,a) & g in Hom (a,a) ) by CAT_1:def 5;

hence g = id a by ZFMISC_1:def 10; :: thesis: verum