let C be Category; for a being Object of C
for g, f 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; for g, f being Morphism of C st dom g = cod f holds
hom (a,(g * f)) = (hom (a,g)) * (hom (a,f))
let g, f be Morphism of C; ( dom g = cod f implies hom (a,(g * f)) = (hom (a,g)) * (hom (a,f)) )
assume A1:
dom g = cod f
; 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 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;
( dom ((hom (a,g)) * (hom (a,f))) = Hom (a,(dom f)) & ( for x being set 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;
for x being set st x in Hom (a,(dom f)) holds
(hom (a,(g * f))) . x = ((hom (a,g)) * (hom (a,f))) . xlet x be
set ;
( 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))
;
(hom (a,(g * f))) . x = ((hom (a,g)) * (hom (a,f))) . xthen 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, Def20
.=
g * (f * f9)
by A1, A9, CAT_1:18
.=
g * g9
by A8, Def20
.=
(hom (a,g)) . g9
by A10, Def20
.=
((hom (a,g)) * (hom (a,f))) . x
by A7, A8, FUNCT_1:12
;
verum end;
hence
hom (a,(g * f)) = (hom (a,g)) * (hom (a,f))
by FUNCT_1:2; verum