let C be Category; :: thesis: for f, g, f9, g9 being Morphism of C st cod g = dom f & dom g9 = cod f9 holds
hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9))

let f, g, f9, g9 be Morphism of C; :: thesis: ( cod g = dom f & dom g9 = cod f9 implies hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9)) )
assume that
A1: cod g = dom f and
A2: dom g9 = cod f9 ; :: thesis: hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9))
A3: dom (g9 (*) f9) = dom f9 by ;
A4: cod (f (*) g) = cod f by ;
A5: ( cod (g9 (*) f9) = cod g9 & dom (f (*) g) = dom g ) by ;
now :: thesis: ( dom (hom ((f (*) g),(g9 (*) f9))) = Hom ((cod f),(dom f9)) & dom ((hom (g,g9)) * (hom (f,f9))) = Hom ((cod f),(dom f9)) & ( for x being object st x in Hom ((cod f),(dom f9)) holds
(hom ((f (*) g),(g9 (*) f9))) . x = ((hom (g,g9)) * (hom (f,f9))) . x ) )
set h = hom ((f (*) g),(g9 (*) f9));
set h2 = hom (g,g9);
set h1 = hom (f,f9);
A6: ( Hom ((dom f),(cod f9)) = {} implies Hom ((cod f),(dom f9)) = {} ) by Th50;
A7: ( Hom ((dom g),(cod g9)) = {} implies Hom ((cod g),(dom g9)) = {} ) by Th50;
hence dom (hom ((f (*) g),(g9 (*) f9))) = Hom ((cod f),(dom f9)) by ; :: thesis: ( dom ((hom (g,g9)) * (hom (f,f9))) = Hom ((cod f),(dom f9)) & ( for x being object st x in Hom ((cod f),(dom f9)) holds
(hom ((f (*) g),(g9 (*) f9))) . x = ((hom (g,g9)) * (hom (f,f9))) . x ) )

thus A8: dom ((hom (g,g9)) * (hom (f,f9))) = Hom ((cod f),(dom f9)) by ; :: thesis: for x being object st x in Hom ((cod f),(dom f9)) holds
(hom ((f (*) g),(g9 (*) f9))) . x = ((hom (g,g9)) * (hom (f,f9))) . x

let x be object ; :: thesis: ( x in Hom ((cod f),(dom f9)) implies (hom ((f (*) g),(g9 (*) f9))) . x = ((hom (g,g9)) * (hom (f,f9))) . x )
assume A9: x in Hom ((cod f),(dom f9)) ; :: thesis: (hom ((f (*) g),(g9 (*) f9))) . x = ((hom (g,g9)) * (hom (f,f9))) . x
then reconsider k = x as Morphism of C ;
A10: (hom (f,f9)) . x in Hom ((cod g),(dom g9)) by ;
then reconsider l = (hom (f,f9)) . x as Morphism of C ;
A11: dom k = cod f by ;
then A12: cod (k (*) (f (*) g)) = cod k by ;
A13: cod k = dom f9 by ;
then A14: dom (f9 (*) k) = dom k by CAT_1:17;
then A15: dom ((f9 (*) k) (*) f) = dom f by ;
cod (f9 (*) k) = cod f9 by ;
then A16: cod ((f9 (*) k) (*) f) = cod f9 by ;
thus (hom ((f (*) g),(g9 (*) f9))) . x = ((g9 (*) f9) (*) k) (*) (f (*) g) by A3, A4, A9, Def22
.= (g9 (*) f9) (*) (k (*) (f (*) g)) by
.= g9 (*) (f9 (*) (k (*) (f (*) g))) by
.= g9 (*) ((f9 (*) k) (*) (f (*) g)) by
.= g9 (*) (((f9 (*) k) (*) f) (*) g) by
.= (g9 (*) ((f9 (*) k) (*) f)) (*) g by
.= (g9 (*) l) (*) g by
.= (hom (g,g9)) . l by
.= ((hom (g,g9)) * (hom (f,f9))) . x by ; :: thesis: verum
end;
hence hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9)) ; :: thesis: verum