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:27;

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:5
.= a2 by A2, CAT_1:19 ;
hence id a = g by A2; :: thesis: verum

end;

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