let C be Category; :: thesis: for g, f, g9, f9 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 g, f, g9, f9 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 A2, CAT_1:42;
A4: cod (f * g) = cod f by A1, CAT_1:42;
A5: ( cod (g9 * f9) = cod g9 & dom (f * g) = dom g ) by A1, A2, CAT_1:42;

now

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 Th51;
A7: ( Hom (dom g),(cod g9) = {} implies Hom (cod g),(dom g9) = {} ) by Th51;
hence dom (hom (f * g),(g9 * f9)) = Hom (cod f),(dom f9) by A1, A2, A3, A5, A4, A6, FUNCT_2:def 1; :: thesis: ( dom ((hom g,g9) * (hom f,f9)) = Hom (cod f),(dom f9) & ( for x being set 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 A1, A2, A7, A6, FUNCT_2:def 1; :: thesis: for x being set 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 set ; :: 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 A1, A2, A9, Th51, FUNCT_2:7;
then reconsider l = (hom f,f9) . x as Morphism of C ;
A11: dom k = cod f by A9, CAT_1:18;
then A12: cod (k * (f * g)) = cod k by A4, CAT_1:42;
A13: cod k = dom f9 by A9, CAT_1:18;
then A14: dom (f9 * k) = dom k by CAT_1:42;
then A15: dom ((f9 * k) * f) = dom f by A11, CAT_1:42;
cod (f9 * k) = cod f9 by A13, CAT_1:42;
then A16: cod ((f9 * k) * f) = cod f9 by A11, A14, CAT_1:42;
thus (hom (f * g),(g9 * f9)) . x = ((g9 * f9) * k) * (f * g) by A3, A4, A9, Def24
.= (g9 * f9) * (k * (f * g)) by A3, A4, A13, A11, CAT_1:43
.= g9 * (f9 * (k * (f * g))) by A2, A13, A12, CAT_1:43
.= g9 * ((f9 * k) * (f * g)) by A4, A13, A11, CAT_1:43
.= g9 * (((f9 * k) * f) * g) by A1, A11, A14, CAT_1:43
.= (g9 * ((f9 * k) * f)) * g by A1, A2, A15, A16, CAT_1:43
.= (g9 * l) * g by A9, Def24
.= (hom g,g9) . l by A10, Def24
.= ((hom g,g9) * (hom f,f9)) . x by A8, A9, FUNCT_1:22 ; :: thesis: verum

end;

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