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 :: thesis: ( dom (hom (f,g)) = Hom ((cod f),(dom g)) & 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 ) )
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 ; :: 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 ;
then A5: dom (h (*) f) = dom f by CAT_1:17;
A6: cod h = dom g by ;
then cod (h (*) f) = dom g by ;
then A7: h (*) f in Hom ((dom f),(dom g)) by A5;
thus (hom (f,g)) . x = (g (*) h) (*) f by
.= g (*) (h (*) f) by
.= (hom ((dom f),g)) . (h (*) f) by
.= (hom ((dom f),g)) . ((hom (f,(dom g))) . h) by
.= ((hom ((dom f),g)) * (hom (f,(dom g)))) . x by ; :: thesis: verum
end;
hence hom (f,g) = (hom ((dom f),g)) * (hom (f,(dom g))) ; :: thesis: verum