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) <> {} ;

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

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

end;

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