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 a,(g * f) = (hom a,g) * (hom a,f)
let a be Object of C; :: thesis: for g, f being Morphism of C st dom g = cod f holds
hom a,(g * f) = (hom a,g) * (hom a,f)
let g, f be Morphism of C; :: thesis: ( dom g = cod f implies hom a,(g * f) = (hom a,g) * (hom a,f) )
assume A1: dom g = cod f ; :: thesis: hom a,(g * f) = (hom a,g) * (hom a,f)
then A2: dom (g * f) = dom f by CAT_1:42;
A3: cod (g * f) = cod g by A1, CAT_1:42;

now

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

end;

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