let C be Category; 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; 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; ( 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 ( 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 ) )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 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;
for x being object st x in Hom (a,(dom f)) holds
(hom (a,(g (*) f))) . x = ((hom (a,g)) * (hom (a,f))) . xlet x be
object ;
( 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, 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
;
verum end;
hence
hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f))
; verum