let C be Category; :: thesis: for a, c being Object of C holds hom (a,(id c)) = id (Hom (a,c))
let a, c be Object of C; :: thesis: hom (a,(id c)) = id (Hom (a,c))
set A = Hom (a,c);
A1: dom (id c) = c by CAT_1:19;
A2: cod (id c) = c by CAT_1:19;

now

( Hom (a,c) = {} implies Hom (a,c) = {} ) ;
hence dom (hom (a,(id c))) = Hom (a,c) by A1, A2, FUNCT_2:def 1; :: thesis: for x being set st x in Hom (a,c) holds
(hom (a,(id c))) . x = x
let x be set ; :: thesis: ( x in Hom (a,c) implies (hom (a,(id c))) . x = x )
assume A3: x in Hom (a,c) ; :: thesis: (hom (a,(id c))) . x = x
then reconsider g = x as Morphism of C ;
A4: cod g = c by A3, CAT_1:1;
thus (hom (a,(id c))) . x = (id c) * g by A1, A3, Def20
.= x by A4, CAT_1:21 ; :: thesis: verum

end;

hence hom (a,(id c)) = id (Hom (a,c)) by FUNCT_1:17; :: thesis: verum