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)}
now :: thesis: for g being Morphism of a,a holds g = id a
let 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;
hence Hom (a,a) = {(id a)} by CAT_1:8; :: thesis: verum