let C be Category; :: thesis: for a being Object of C

for f, g being Morphism of C st dom g = cod f holds

hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f))

let a be Object of C; :: thesis: for f, g being Morphism of C st dom g = cod f holds

hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f))

let f, g be Morphism of C; :: thesis: ( dom g = cod f implies hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f)) )

assume A1: dom g = cod f ; :: thesis: hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f))

then A2: dom (g (*) f) = dom f by CAT_1:17;

A3: cod (g (*) f) = cod g by A1, CAT_1:17;

for f, g being Morphism of C st dom g = cod f holds

hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f))

let a be Object of C; :: thesis: for f, g being Morphism of C st dom g = cod f holds

hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f))

let f, g be Morphism of C; :: thesis: ( dom g = cod f implies hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f)) )

assume A1: dom g = cod f ; :: thesis: hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f))

then A2: dom (g (*) f) = dom f by CAT_1:17;

A3: cod (g (*) f) = cod g by A1, CAT_1:17;

now :: thesis: ( dom (hom (a,(g (*) f))) = Hom (a,(dom f)) & dom ((hom (a,g)) * (hom (a,f))) = Hom (a,(dom f)) & ( for x being object st x in Hom (a,(dom f)) holds

(hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . x ) )

hence
hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f))
; :: thesis: verum(hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . x ) )

set h = hom (a,(g (*) f));

set h2 = hom (a,g);

set h1 = hom (a,f);

A4: Hom ((dom f),(cod f)) <> {} by CAT_1:2;

then A5: ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) by CAT_1:24;

Hom ((dom g),(cod g)) <> {} by CAT_1:2;

then A6: ( Hom (a,(cod g)) = {} implies Hom (a,(dom g)) = {} ) by CAT_1:24;

hence dom (hom (a,(g (*) f))) = Hom (a,(dom f)) by A1, A2, A3, A5, FUNCT_2:def 1; :: thesis: ( dom ((hom (a,g)) * (hom (a,f))) = Hom (a,(dom f)) & ( for x being object st x in Hom (a,(dom f)) holds

(hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . x ) )

thus A7: dom ((hom (a,g)) * (hom (a,f))) = Hom (a,(dom f)) by A1, A5, A6, FUNCT_2:def 1; :: thesis: for x being object st x in Hom (a,(dom f)) holds

(hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . x

let x be object ; :: thesis: ( x in Hom (a,(dom f)) implies (hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . x )

assume A8: x in Hom (a,(dom f)) ; :: thesis: (hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . x

then reconsider f9 = x as Morphism of C ;

A9: cod f9 = dom f by A8, CAT_1:1;

A10: (hom (a,f)) . x in Hom (a,(dom g)) by A1, A4, A8, CAT_1:24, FUNCT_2:5;

then reconsider g9 = (hom (a,f)) . x as Morphism of C ;

thus (hom (a,(g (*) f))) . x = (g (*) f) (*) f9 by A2, A8, Def18

.= g (*) (f (*) f9) by A1, A9, CAT_1:18

.= g (*) g9 by A8, Def18

.= (hom (a,g)) . g9 by A10, Def18

.= ((hom (a,g)) * (hom (a,f))) . x by A7, A8, FUNCT_1:12 ; :: thesis: verum

end;set h2 = hom (a,g);

set h1 = hom (a,f);

A4: Hom ((dom f),(cod f)) <> {} by CAT_1:2;

then A5: ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) by CAT_1:24;

Hom ((dom g),(cod g)) <> {} by CAT_1:2;

then A6: ( Hom (a,(cod g)) = {} implies Hom (a,(dom g)) = {} ) by CAT_1:24;

hence dom (hom (a,(g (*) f))) = Hom (a,(dom f)) by A1, A2, A3, A5, FUNCT_2:def 1; :: thesis: ( dom ((hom (a,g)) * (hom (a,f))) = Hom (a,(dom f)) & ( for x being object st x in Hom (a,(dom f)) holds

(hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . x ) )

thus A7: dom ((hom (a,g)) * (hom (a,f))) = Hom (a,(dom f)) by A1, A5, A6, FUNCT_2:def 1; :: thesis: for x being object st x in Hom (a,(dom f)) holds

(hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . x

let x be object ; :: thesis: ( x in Hom (a,(dom f)) implies (hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . x )

assume A8: x in Hom (a,(dom f)) ; :: thesis: (hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . x

then reconsider f9 = x as Morphism of C ;

A9: cod f9 = dom f by A8, CAT_1:1;

A10: (hom (a,f)) . x in Hom (a,(dom g)) by A1, A4, A8, CAT_1:24, FUNCT_2:5;

then reconsider g9 = (hom (a,f)) . x as Morphism of C ;

thus (hom (a,(g (*) f))) . x = (g (*) f) (*) f9 by A2, A8, Def18

.= g (*) (f (*) f9) by A1, A9, CAT_1:18

.= g (*) g9 by A8, Def18

.= (hom (a,g)) . g9 by A10, Def18

.= ((hom (a,g)) * (hom (a,f))) . x by A7, A8, FUNCT_1:12 ; :: thesis: verum