let C be Category; :: thesis: for a being Object of C
for f being Morphism of C holds
( hom ((id a),f) = hom (a,f) & hom (f,(id a)) = hom (f,a) )
let a be Object of C; :: thesis: for f being Morphism of C holds
( hom ((id a),f) = hom (a,f) & hom (f,(id a)) = hom (f,a) )
let f be Morphism of C; :: thesis: ( hom ((id a),f) = hom (a,f) & hom (f,(id a)) = hom (f,a) )
A1: cod (id a) = a by CAT_1:19;
A2: dom (id a) = a by CAT_1:19;

now

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

end;

hence hom ((id a),f) = hom (a,f) by FUNCT_1:2; :: thesis: hom (f,(id a)) = hom (f,a)

now

Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) by CAT_1:24;
hence ( dom (hom (f,(id a))) = Hom ((cod f),a) & dom (hom (f,a)) = Hom ((cod f),a) ) by A2, A1, FUNCT_2:def 1; :: thesis: for x being set st x in Hom ((cod f),a) holds
(hom (f,(id a))) . x = (hom (f,a)) . x
let x be set ; :: thesis: ( x in Hom ((cod f),a) implies (hom (f,(id a))) . x = (hom (f,a)) . x )
assume A6: x in Hom ((cod f),a) ; :: thesis: (hom (f,(id a))) . x = (hom (f,a)) . x
then reconsider g = x as Morphism of C ;
A7: cod g = a by A6, CAT_1:1;
thus (hom (f,(id a))) . x = ((id a) * g) * f by A2, A6, Def24
.= g * f by A7, CAT_1:21
.= (hom (f,a)) . x by A6, Def21 ; :: thesis: verum

end;

hence hom (f,(id a)) = hom (f,a) by FUNCT_1:2; :: thesis: verum