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)))

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 ) )

hence
hom (f,g) = (hom ((dom f),g)) * (hom (f,(dom g)))
; :: thesis: verum(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 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

end;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