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:42;
A3: dom (g * f) = dom f by A1, CAT_1:42;

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:19;
then A5: ( Hom (dom g),a = {} implies Hom (cod g),a = {} ) by CAT_1:52;
Hom (dom f),(cod f) <> {} by CAT_1:19;
then A6: ( Hom (dom f),a = {} implies Hom (cod f),a = {} ) by CAT_1:52;
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:18;
A10: (hom g,a) . x in Hom (cod f),a by A1, A4, A8, CAT_1:52, FUNCT_2:7;
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:43
.= g9 * f by A8, Def21
.= (hom f,a) . g9 by A10, Def21
.= ((hom f,a) * (hom g,a)) . x by A7, A8, FUNCT_1:22 ; :: thesis: verum

end;

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