let C be Category; :: thesis: for a being Object of
for g, f being Morphism of st dom g = cod f holds
hom a,(g * f) = (hom a,g) * (hom a,f)
let a be Object of ; :: thesis: for g, f being Morphism of st dom g = cod f holds
hom a,(g * f) = (hom a,g) * (hom a,f)
let g, f be Morphism of ; :: 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 f' = x as Morphism of ;
A9: cod f' = 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 g' = (hom a,f) . x as Morphism of ;
thus (hom a,(g * f)) . x = (g * f) * f' by A2, A8, Def20
.= g * (f * f') by A1, A9, CAT_1:43
.= g * g' by A8, Def20
.= (hom a,g) . g' 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