let C be Category; :: thesis: for a being Object of C
for f, g 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 f, g being Morphism of C st dom g = cod f holds
hom ((g (*) f),a) = (hom (f,a)) * (hom (g,a))

let f, g 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 ;
now :: thesis: ( dom (hom ((g (*) f),a)) = Hom ((cod g),a) & dom ((hom (f,a)) * (hom (g,a))) = Hom ((cod g),a) & ( for x being object st x in Hom ((cod g),a) holds
(hom ((g (*) f),a)) . x = ((hom (f,a)) * (hom (g,a))) . x ) )
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 ; :: thesis: ( dom ((hom (f,a)) * (hom (g,a))) = Hom ((cod g),a) & ( for x being object 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 ; :: thesis: for x being object st x in Hom ((cod g),a) holds
(hom ((g (*) f),a)) . x = ((hom (f,a)) * (hom (g,a))) . x

let x be object ; :: 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 ;
A10: (hom (g,a)) . x in Hom ((cod f),a) by ;
then reconsider g9 = (hom (g,a)) . x as Morphism of C ;
thus (hom ((g (*) f),a)) . x = f9 (*) (g (*) f) by
.= (f9 (*) g) (*) f by
.= g9 (*) f by
.= (hom (f,a)) . g9 by
.= ((hom (f,a)) * (hom (g,a))) . x by ; :: thesis: verum
end;
hence hom ((g (*) f),a) = (hom (f,a)) * (hom (g,a)) ; :: thesis: verum