A1: ( Hom ((dom f),(cod g)) = {} implies Hom ((cod f),(dom g)) = {} ) by Th50;
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 object 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:2;
then ( Hom ((dom f),(dom g)) = {} implies Hom ((cod f),(dom g)) = {} ) by CAT_1:24;
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 object 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 object ; :: 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:1;
then A5: dom (h (*) f) = dom f by CAT_1:17;
A6: cod h = dom g by A3, CAT_1:1;
then cod (h (*) f) = dom g by A4, CAT_1:17;
then A7: h (*) f in Hom ((dom f),(dom g)) by A5;
thus (hom (f,g)) . x = (g (*) h) (*) f by A3, Def22
.= g (*) (h (*) f) by A4, A6, CAT_1:18
.= (hom ((dom f),g)) . (h (*) f) by A7, Def18
.= (hom ((dom f),g)) . ((hom (f,(dom g))) . h) by A3, Def19
.= ((hom ((dom f),g)) * (hom (f,(dom g)))) . x by A2, A3, FUNCT_1:12 ; :: thesis: verum