let B, C, D be Category; for L being Function of the carrier of C,(Funct (B,D))
for M being Function of the carrier of B,(Funct (C,D)) st ( for c being Object of C
for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B
for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) holds
ex S being Functor of [:B,C:],D st
for f being Morphism of B
for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)
deffunc H1( Category) -> set = the carrier' of $1;
let L be Function of the carrier of C,(Funct (B,D)); for M being Function of the carrier of B,(Funct (C,D)) st ( for c being Object of C
for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B
for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) holds
ex S being Functor of [:B,C:],D st
for f being Morphism of B
for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)
let M be Function of the carrier of B,(Funct (C,D)); ( ( for c being Object of C
for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B
for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) implies ex S being Functor of [:B,C:],D st
for f being Morphism of B
for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) )
assume that
A1:
for c being Object of C
for b being Object of B holds (M . b) . (id c) = (L . c) . (id b)
and
A2:
for f being Morphism of B
for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)
; ex S being Functor of [:B,C:],D st
for f being Morphism of B
for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)
deffunc H2( Element of H1(B), Element of H1(C)) -> Element of the carrier' of D = ((L . (cod $2)) . $1) (*) ((M . (dom $1)) . $2);
consider S being Function of [:H1(B),H1(C):],H1(D) such that
A3:
for f being Morphism of B
for g being Morphism of C holds S . (f,g) = H2(f,g)
from BINOP_1:sch 4();
reconsider T = S as Function of H1([:B,C:]),H1(D) ;
now ( ( for bc being Object of [:B,C:] ex d being Object of D st T . (id bc) = id d ) & ( for fg being Morphism of [:B,C:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds
T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1) ) )thus
for
bc being
Object of
[:B,C:] ex
d being
Object of
D st
T . (id bc) = id d
( ( for fg being Morphism of [:B,C:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds
T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1) ) )thus
for
fg being
Morphism of
[:B,C:] holds
(
T . (id (dom fg)) = id (dom (T . fg)) &
T . (id (cod fg)) = id (cod (T . fg)) )
for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds
T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1)proof
let fg be
Morphism of
[:B,C:];
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) )
consider f being
Morphism of
B,
g being
Morphism of
C such that A8:
fg = [f,g]
by DOMAIN_1:1;
set b =
dom f;
set c =
dom g;
set g9 =
id (dom g);
set f9 =
id (dom f);
A9:
Hom (
(dom ((M . (dom f)) . g)),
(dom ((M . (dom f)) . g)))
<> {}
;
id (dom ((L . (cod g)) . f)) =
(L . (cod g)) . (id (dom f))
by CAT_1:63
.=
(M . (dom f)) . (id (cod g))
by A1
.=
id (cod ((M . (dom f)) . g))
by CAT_1:63
;
then A10:
dom ((L . (cod g)) . f) = cod ((M . (dom f)) . g)
by CAT_1:59;
thus T . (id (dom fg)) =
S . (id [(dom f),(dom g)])
by A8, Th22
.=
S . (
(id (dom f)),
(id (dom g)))
by Th25
.=
((L . (cod (id (dom g)))) . (id (dom f))) (*) ((M . (dom (id (dom f)))) . (id (dom g)))
by A3
.=
((L . (dom g)) . (id (dom f))) (*) ((M . (dom (id (dom f)))) . (id (dom g)))
.=
((L . (dom g)) . (id (dom f))) (*) ((M . (dom f)) . (id (dom g)))
.=
((M . (dom f)) . (id (dom g))) (*) ((M . (dom f)) . (id (dom g)))
by A1
.=
(id (dom ((M . (dom f)) . g))) (*) ((M . (dom f)) . (id (dom g)))
by CAT_1:63
.=
(id (dom ((M . (dom f)) . g))) (*) (id (dom ((M . (dom f)) . g)))
by CAT_1:63
.=
(id (dom ((M . (dom f)) . g))) * (id (dom ((M . (dom f)) . g)))
by A9, CAT_1:def 13
.=
id (dom (((L . (cod g)) . f) (*) ((M . (dom f)) . g)))
by A10, CAT_1:17
.=
id (dom (S . (f,g)))
by A3
.=
id (dom (T . fg))
by A8
;
T . (id (cod fg)) = id (cod (T . fg))
set b =
cod f;
set c =
cod g;
set g9 =
id (cod g);
set f9 =
id (cod f);
A11:
Hom (
(cod ((L . (cod g)) . f)),
(cod ((L . (cod g)) . f)))
<> {}
;
thus T . (id (cod fg)) =
S . (id [(cod f),(cod g)])
by A8, Th22
.=
S . (
(id (cod f)),
(id (cod g)))
by Th25
.=
((L . (cod (id (cod g)))) . (id (cod f))) (*) ((M . (dom (id (cod f)))) . (id (cod g)))
by A3
.=
((L . (cod g)) . (id (cod f))) (*) ((M . (dom (id (cod f)))) . (id (cod g)))
.=
((L . (cod g)) . (id (cod f))) (*) ((M . (cod f)) . (id (cod g)))
.=
((L . (cod g)) . (id (cod f))) (*) ((L . (cod g)) . (id (cod f)))
by A1
.=
(id (cod ((L . (cod g)) . f))) (*) ((L . (cod g)) . (id (cod f)))
by CAT_1:63
.=
(id (cod ((L . (cod g)) . f))) (*) (id (cod ((L . (cod g)) . f)))
by CAT_1:63
.=
(id (cod ((L . (cod g)) . f))) * (id (cod ((L . (cod g)) . f)))
by A11, CAT_1:def 13
.=
id (cod (((L . (cod g)) . f) (*) ((M . (dom f)) . g)))
by A10, CAT_1:17
.=
id (cod (S . (f,g)))
by A3
.=
id (cod (T . fg))
by A8
;
verum
end; let fg1,
fg2 be
Morphism of
[:B,C:];
( dom fg2 = cod fg1 implies T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1) )assume A12:
dom fg2 = cod fg1
;
T . (fg2 (*) fg1) = (T . fg2) (*) (T . fg1)consider f1 being
Morphism of
B,
g1 being
Morphism of
C such that A13:
fg1 = [f1,g1]
by DOMAIN_1:1;
consider f2 being
Morphism of
B,
g2 being
Morphism of
C such that A14:
fg2 = [f2,g2]
by DOMAIN_1:1;
A15:
[(cod f1),(cod g1)] = cod fg1
by A13, Th22;
set L1 =
L . (cod g1);
set L2 =
L . (cod g2);
set M1 =
M . (dom f1);
set M2 =
M . (dom f2);
A16:
[(dom f2),(dom g2)] = dom fg2
by A14, Th22;
then A17:
dom f2 = cod f1
by A12, A15, XTUPLE_0:1;
then A18:
dom ((L . (cod g2)) . f2) = cod ((L . (cod g2)) . f1)
by CAT_1:64;
id (dom ((L . (cod g1)) . f1)) =
(L . (cod g1)) . (id (dom f1))
by CAT_1:63
.=
(M . (dom f1)) . (id (cod g1))
by A1
.=
id (cod ((M . (dom f1)) . g1))
by CAT_1:63
;
then A19:
dom ((L . (cod g1)) . f1) = cod ((M . (dom f1)) . g1)
by CAT_1:59;
then A20:
cod (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1)) = cod ((L . (cod g1)) . f1)
by CAT_1:17;
A21:
dom g2 = cod g1
by A12, A16, A15, XTUPLE_0:1;
then A22:
dom ((M . (dom f1)) . g2) = cod ((M . (dom f1)) . g1)
by CAT_1:64;
then A23:
cod (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1)) = cod ((M . (dom f1)) . g2)
by CAT_1:17;
id (dom ((M . (dom f2)) . g2)) =
(M . (dom f2)) . (id (dom g2))
by CAT_1:63
.=
(L . (cod g1)) . (id (cod f1))
by A1, A17, A21
.=
id (cod ((L . (cod g1)) . f1))
by CAT_1:63
;
then A24:
dom ((M . (dom f2)) . g2) = cod ((L . (cod g1)) . f1)
by CAT_1:59;
id (dom ((L . (cod g2)) . f2)) =
(L . (cod g2)) . (id (dom f2))
by CAT_1:63
.=
(M . (dom f2)) . (id (cod g2))
by A1
.=
id (cod ((M . (dom f2)) . g2))
by CAT_1:63
;
then A25:
dom ((L . (cod g2)) . f2) = cod ((M . (dom f2)) . g2)
by CAT_1:59;
set f =
f2 (*) f1;
set g =
g2 (*) g1;
id (dom ((L . (cod g2)) . f1)) =
(L . (cod g2)) . (id (dom f1))
by CAT_1:63
.=
(M . (dom f1)) . (id (cod g2))
by A1
.=
id (cod ((M . (dom f1)) . g2))
by CAT_1:63
;
then A26:
dom ((L . (cod g2)) . f1) = cod ((M . (dom f1)) . g2)
by CAT_1:59;
thus T . (fg2 (*) fg1) =
S . (
(f2 (*) f1),
(g2 (*) g1))
by A12, A13, A14, Th24
.=
((L . (cod (g2 (*) g1))) . (f2 (*) f1)) (*) ((M . (dom (f2 (*) f1))) . (g2 (*) g1))
by A3
.=
((L . (cod g2)) . (f2 (*) f1)) (*) ((M . (dom (f2 (*) f1))) . (g2 (*) g1))
by A21, CAT_1:17
.=
((L . (cod g2)) . (f2 (*) f1)) (*) ((M . (dom f1)) . (g2 (*) g1))
by A17, CAT_1:17
.=
(((L . (cod g2)) . f2) (*) ((L . (cod g2)) . f1)) (*) ((M . (dom f1)) . (g2 (*) g1))
by A17, CAT_1:64
.=
(((L . (cod g2)) . f2) (*) ((L . (cod g2)) . f1)) (*) (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1))
by A21, CAT_1:64
.=
((L . (cod g2)) . f2) (*) (((L . (cod g2)) . f1) (*) (((M . (dom f1)) . g2) (*) ((M . (dom f1)) . g1)))
by A18, A23, A26, CAT_1:18
.=
((L . (cod g2)) . f2) (*) ((((L . (cod g2)) . f1) (*) ((M . (dom f1)) . g2)) (*) ((M . (dom f1)) . g1))
by A22, A26, CAT_1:18
.=
((L . (cod g2)) . f2) (*) ((((M . (dom f2)) . g2) (*) ((L . (cod g1)) . f1)) (*) ((M . (dom f1)) . g1))
by A2, A17, A21
.=
((L . (cod g2)) . f2) (*) (((M . (dom f2)) . g2) (*) (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1)))
by A19, A24, CAT_1:18
.=
(((L . (cod g2)) . f2) (*) ((M . (dom f2)) . g2)) (*) (((L . (cod g1)) . f1) (*) ((M . (dom f1)) . g1))
by A24, A25, A20, CAT_1:18
.=
(((L . (cod g2)) . f2) (*) ((M . (dom f2)) . g2)) (*) (S . (f1,g1))
by A3
.=
(S . (f2,g2)) (*) (T . fg1)
by A3, A13
.=
(T . fg2) (*) (T . fg1)
by A14
;
verum end;
then reconsider T = T as Functor of [:B,C:],D by CAT_1:61;
take
T
; for f being Morphism of B
for g being Morphism of C holds T . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)
thus
for f being Morphism of B
for g being Morphism of C holds T . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)
by A3; verum