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

now

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

end;

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