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

now

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

end;

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