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)}
A1: Hom a,a <> {} by CAT_1:56;

now

let g be Morphism of a,a; :: thesis: id a = g
consider a2 being Object of A such that
A2: g = id a2 by Def19;
a = dom g by A1, CAT_1:23
.= a2 by A2, CAT_1:44 ;
hence id a = g by A2; :: thesis: verum

end;

hence Hom a,a = {(id a)} by CAT_1:26, CAT_1:56; :: thesis: verum