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 & cod (id c) = c ) by CAT_1:44;

now

( Hom a,c = {} implies Hom a,c = {} ) ;
hence dom (hom a,(id c)) = Hom a,c by A1, 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 A2: x in Hom a,c ; :: thesis: (hom a,(id c)) . x = x
then reconsider g = x as Morphism of C ;
A3: cod g = c by A2, CAT_1:18;
thus (hom a,(id c)) . x = (id c) * g by A1, A2, Def20
.= x by A3, CAT_1:46 ; :: thesis: verum

end;

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