let C be Category; :: thesis: for a being Object of C
for g, f being Morphism of C st dom g = cod f holds
hom ((g * f),a) = (hom (f,a)) * (hom (g,a))
let a be Object of C; :: thesis: for g, f being Morphism of C st dom g = cod f holds
hom ((g * f),a) = (hom (f,a)) * (hom (g,a))
let g, f be Morphism of C; :: thesis: ( dom g = cod f implies hom ((g * f),a) = (hom (f,a)) * (hom (g,a)) )
assume A1: dom g = cod f ; :: thesis: hom ((g * f),a) = (hom (f,a)) * (hom (g,a))
then A2: cod (g * f) = cod g by CAT_1:17;
A3: dom (g * f) = dom f by A1, CAT_1:17;

now

set h = hom ((g * f),a);
set h2 = hom (g,a);
set h1 = hom (f,a);
A4: Hom ((dom g),(cod g)) <> {} by CAT_1:2;
then A5: ( Hom ((dom g),a) = {} implies Hom ((cod g),a) = {} ) by CAT_1:24;
Hom ((dom f),(cod f)) <> {} by CAT_1:2;
then A6: ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) by CAT_1:24;
hence dom (hom ((g * f),a)) = Hom ((cod g),a) by A1, A3, A2, A5, FUNCT_2:def 1; :: thesis: ( dom ((hom (f,a)) * (hom (g,a))) = Hom ((cod g),a) & ( for x being set st x in Hom ((cod g),a) holds
(hom ((g * f),a)) . x = ((hom (f,a)) * (hom (g,a))) . x ) )
thus A7: dom ((hom (f,a)) * (hom (g,a))) = Hom ((cod g),a) by A1, A6, A5, FUNCT_2:def 1; :: thesis: for x being set st x in Hom ((cod g),a) holds
(hom ((g * f),a)) . x = ((hom (f,a)) * (hom (g,a))) . x
let x be set ; :: thesis: ( x in Hom ((cod g),a) implies (hom ((g * f),a)) . x = ((hom (f,a)) * (hom (g,a))) . x )
assume A8: x in Hom ((cod g),a) ; :: thesis: (hom ((g * f),a)) . x = ((hom (f,a)) * (hom (g,a))) . x
then reconsider f9 = x as Morphism of C ;
A9: dom f9 = cod g by A8, CAT_1:1;
A10: (hom (g,a)) . x in Hom ((cod f),a) by A1, A4, A8, CAT_1:24, FUNCT_2:5;
then reconsider g9 = (hom (g,a)) . x as Morphism of C ;
thus (hom ((g * f),a)) . x = f9 * (g * f) by A2, A8, Def21
.= (f9 * g) * f by A1, A9, CAT_1:18
.= g9 * f by A8, Def21
.= (hom (f,a)) . g9 by A10, Def21
.= ((hom (f,a)) * (hom (g,a))) . x by A7, A8, FUNCT_1:12 ; :: thesis: verum

end;

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