let C be Category; for f, g, f9, g9 being Morphism of C st cod g = dom f & dom g9 = cod f9 holds
hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9))
let f, g, f9, g9 be Morphism of C; ( cod g = dom f & dom g9 = cod f9 implies hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9)) )
assume that
A1:
cod g = dom f
and
A2:
dom g9 = cod f9
; hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9))
A3:
dom (g9 (*) f9) = dom f9
by A2, CAT_1:17;
A4:
cod (f (*) g) = cod f
by A1, CAT_1:17;
A5:
( cod (g9 (*) f9) = cod g9 & dom (f (*) g) = dom g )
by A1, A2, CAT_1:17;
now ( dom (hom ((f (*) g),(g9 (*) f9))) = Hom ((cod f),(dom f9)) & dom ((hom (g,g9)) * (hom (f,f9))) = Hom ((cod f),(dom f9)) & ( for x being object st x in Hom ((cod f),(dom f9)) holds
(hom ((f (*) g),(g9 (*) f9))) . x = ((hom (g,g9)) * (hom (f,f9))) . x ) )set h =
hom (
(f (*) g),
(g9 (*) f9));
set h2 =
hom (
g,
g9);
set h1 =
hom (
f,
f9);
A6:
(
Hom (
(dom f),
(cod f9))
= {} implies
Hom (
(cod f),
(dom f9))
= {} )
by Th50;
A7:
(
Hom (
(dom g),
(cod g9))
= {} implies
Hom (
(cod g),
(dom g9))
= {} )
by Th50;
hence
dom (hom ((f (*) g),(g9 (*) f9))) = Hom (
(cod f),
(dom f9))
by A1, A2, A3, A5, A4, A6, FUNCT_2:def 1;
( dom ((hom (g,g9)) * (hom (f,f9))) = Hom ((cod f),(dom f9)) & ( for x being object st x in Hom ((cod f),(dom f9)) holds
(hom ((f (*) g),(g9 (*) f9))) . x = ((hom (g,g9)) * (hom (f,f9))) . x ) )thus A8:
dom ((hom (g,g9)) * (hom (f,f9))) = Hom (
(cod f),
(dom f9))
by A1, A2, A7, A6, FUNCT_2:def 1;
for x being object st x in Hom ((cod f),(dom f9)) holds
(hom ((f (*) g),(g9 (*) f9))) . x = ((hom (g,g9)) * (hom (f,f9))) . xlet x be
object ;
( x in Hom ((cod f),(dom f9)) implies (hom ((f (*) g),(g9 (*) f9))) . x = ((hom (g,g9)) * (hom (f,f9))) . x )assume A9:
x in Hom (
(cod f),
(dom f9))
;
(hom ((f (*) g),(g9 (*) f9))) . x = ((hom (g,g9)) * (hom (f,f9))) . xthen reconsider k =
x as
Morphism of
C ;
A10:
(hom (f,f9)) . x in Hom (
(cod g),
(dom g9))
by A1, A2, A9, Th50, FUNCT_2:5;
then reconsider l =
(hom (f,f9)) . x as
Morphism of
C ;
A11:
dom k = cod f
by A9, CAT_1:1;
then A12:
cod (k (*) (f (*) g)) = cod k
by A4, CAT_1:17;
A13:
cod k = dom f9
by A9, CAT_1:1;
then A14:
dom (f9 (*) k) = dom k
by CAT_1:17;
then A15:
dom ((f9 (*) k) (*) f) = dom f
by A11, CAT_1:17;
cod (f9 (*) k) = cod f9
by A13, CAT_1:17;
then A16:
cod ((f9 (*) k) (*) f) = cod f9
by A11, A14, CAT_1:17;
thus (hom ((f (*) g),(g9 (*) f9))) . x =
((g9 (*) f9) (*) k) (*) (f (*) g)
by A3, A4, A9, Def22
.=
(g9 (*) f9) (*) (k (*) (f (*) g))
by A3, A4, A13, A11, CAT_1:18
.=
g9 (*) (f9 (*) (k (*) (f (*) g)))
by A2, A13, A12, CAT_1:18
.=
g9 (*) ((f9 (*) k) (*) (f (*) g))
by A4, A13, A11, CAT_1:18
.=
g9 (*) (((f9 (*) k) (*) f) (*) g)
by A1, A11, A14, CAT_1:18
.=
(g9 (*) ((f9 (*) k) (*) f)) (*) g
by A1, A2, A15, A16, CAT_1:18
.=
(g9 (*) l) (*) g
by A9, Def22
.=
(hom (g,g9)) . l
by A10, Def22
.=
((hom (g,g9)) * (hom (f,f9))) . x
by A8, A9, FUNCT_1:12
;
verum end;
hence
hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9))
; verum