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

now

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

end;

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