set C1 = C -SliceCat (dom f);
set C2 = C -SliceCat (cod f);
deffunc H1( Morphism of (C -SliceCat (dom f))) -> Element of the carrier' of [:[:C,C:],C:] = [[(f * ($1 `11 )),(f * ($1 `12 ))],($1 `2 )];
consider F being Function of the carrier' of (C -SliceCat (dom f)),the carrier' of [:[:C,C:],C:] such that
A1:
for m being Morphism of (C -SliceCat (dom f)) holds F . m = H1(m)
from FUNCT_2:sch 4();
A2:
dom F = the carrier' of (C -SliceCat (dom f))
by FUNCT_2:def 1;
rng F c= the carrier' of (C -SliceCat (cod f))
proof
let x be
set ;
TARSKI:def 3 ( not x in rng F or x in the carrier' of (C -SliceCat (cod f)) )
assume
x in rng F
;
x in the carrier' of (C -SliceCat (cod f))
then consider m being
set such that A3:
m in dom F
and A4:
x = F . m
by FUNCT_1:def 5;
reconsider m =
m as
Morphism of
(C -SliceCat (dom f)) by A3;
A5:
x = [[(f * (m `11 )),(f * (m `12 ))],(m `2 )]
by A1, A4;
A6:
dom (m `12 ) = cod (m `2 )
by Th29;
A7:
m `11 = (m `12 ) * (m `2 )
by Th29;
A8:
cod (m `12 ) = dom f
by Th23;
A9:
f * (m `11 ) in Hom (cod f)
by Th27;
A10:
f * (m `12 ) in Hom (cod f)
by Th27;
A11:
dom (f * (m `12 )) = cod (m `2 )
by A6, A8, CAT_1:42;
f * (m `11 ) = (f * (m `12 )) * (m `2 )
by A6, A7, A8, CAT_1:43;
then
x is
Morphism of
(C -SliceCat (cod f))
by A5, A9, A10, A11, Def11;
hence
x in the
carrier' of
(C -SliceCat (cod f))
;
verum
end;
then reconsider F = F as Function of the carrier' of (C -SliceCat (dom f)),the carrier' of (C -SliceCat (cod f)) by A2, FUNCT_2:def 1, RELSET_1:11;
A12:
now let c be
Object of
(C -SliceCat (dom f));
ex d being Object of (C -SliceCat (cod f)) st F . (id c) = id dreconsider g =
c as
Element of
Hom (dom f) by Def11;
reconsider h =
f * g as
Element of
Hom (cod f) by Th27;
reconsider d =
h as
Object of
(C -SliceCat (cod f)) by Def11;
take d =
d;
F . (id c) = id dA13:
id c = [[c,c],(id (dom g))]
by Th30;
A14:
id d = [[d,d],(id (dom h))]
by Th30;
A15:
(id c) `11 = c
by A13, MCART_1:89;
A16:
(id c) `12 = c
by A13, MCART_1:89;
A17:
(id c) `2 = id (dom g)
by A13, MCART_1:7;
A18:
cod g = dom f
by Th23;
thus F . (id c) =
[[h,h],((id c) `2 )]
by A1, A15, A16
.=
id d
by A14, A17, A18, CAT_1:42
;
verum end;
A19:
now let m be
Morphism of
(C -SliceCat (dom f));
( F . (id (dom m)) = id (dom (F . m)) & F . (id (cod m)) = id (cod (F . m)) )reconsider g1 =
f * (m `11 ),
g2 =
f * (m `12 ) as
Element of
Hom (cod f) by Th27;
A20:
dom f = cod (m `11 )
by Th23;
A21:
dom f = cod (m `12 )
by Th23;
F . m = [[g1,g2],(m `2 )]
by A1;
then dom (F . m) =
[[g1,g2],(m `2 )] `11
by Th29
.=
g1
by MCART_1:89
;
then A22:
id (dom (F . m)) = [[g1,g1],(id (dom g1))]
by Th30;
dom m = m `11
by Th29;
then A23:
id (dom m) = [[(m `11 ),(m `11 )],(id (dom (m `11 )))]
by Th30;
then A24:
(id (dom m)) `11 = m `11
by MCART_1:89;
A25:
(id (dom m)) `12 = m `11
by A23, MCART_1:89;
(id (dom m)) `2 = id (dom (m `11 ))
by A23, MCART_1:7;
hence F . (id (dom m)) =
[[g1,g1],(id (dom (m `11 )))]
by A1, A24, A25
.=
id (dom (F . m))
by A20, A22, CAT_1:42
;
F . (id (cod m)) = id (cod (F . m))
F . m = [[g1,g2],(m `2 )]
by A1;
then cod (F . m) =
[[g1,g2],(m `2 )] `12
by Th29
.=
g2
by MCART_1:89
;
then A26:
id (cod (F . m)) = [[g2,g2],(id (dom g2))]
by Th30;
cod m = m `12
by Th29;
then A27:
id (cod m) = [[(m `12 ),(m `12 )],(id (dom (m `12 )))]
by Th30;
then A28:
(id (cod m)) `11 = m `12
by MCART_1:89;
A29:
(id (cod m)) `12 = m `12
by A27, MCART_1:89;
(id (cod m)) `2 = id (dom (m `12 ))
by A27, MCART_1:7;
hence F . (id (cod m)) =
[[g2,g2],(id (dom (m `12 )))]
by A1, A28, A29
.=
id (cod (F . m))
by A21, A26, CAT_1:42
;
verum end;
now let f1,
f2 be
Morphism of
(C -SliceCat (dom f));
( dom f2 = cod f1 implies F . (f2 * f1) = (F . f2) * (F . f1) )consider a1,
b1 being
Element of
Hom (dom f),
g1 being
Morphism of
C such that A30:
f1 = [[a1,b1],g1]
and
dom b1 = cod g1
and
a1 = b1 * g1
by Def11;
consider a2,
b2 being
Element of
Hom (dom f),
g2 being
Morphism of
C such that A31:
f2 = [[a2,b2],g2]
and
dom b2 = cod g2
and
a2 = b2 * g2
by Def11;
A32:
dom f2 = f2 `11
by Th2;
A33:
cod f1 = f1 `12
by Th2;
A34:
dom f2 = a2
by A31, A32, MCART_1:89;
A35:
cod f1 = b1
by A30, A33, MCART_1:89;
reconsider ha1 =
f * a1,
ha2 =
f * a2,
hb1 =
f * b1,
hb2 =
f * b2 as
Element of
Hom (cod f) by Th27;
A36:
f1 `11 = a1
by A30, MCART_1:89;
A37:
f1 `12 = b1
by A30, MCART_1:89;
A38:
f1 `2 = g1
by A30, MCART_1:7;
A39:
f2 `11 = a2
by A31, MCART_1:89;
A40:
f2 `12 = b2
by A31, MCART_1:89;
A41:
f2 `2 = g2
by A31, MCART_1:7;
A42:
F . f1 = [[ha1,hb1],g1]
by A1, A36, A37, A38;
A43:
F . f2 = [[ha2,hb2],g2]
by A1, A39, A40, A41;
assume A44:
dom f2 = cod f1
;
F . (f2 * f1) = (F . f2) * (F . f1)then A45:
f2 * f1 = [[a1,b2],(g2 * g1)]
by A30, A31, A34, A35, Def11;
A46:
(F . f2) * (F . f1) = [[ha1,hb2],(g2 * g1)]
by A34, A35, A42, A43, A44, Def11;
A47:
(f2 * f1) `11 = a1
by A45, MCART_1:89;
A48:
(f2 * f1) `12 = b2
by A45, MCART_1:89;
(f2 * f1) `2 = g2 * g1
by A45, MCART_1:7;
hence
F . (f2 * f1) = (F . f2) * (F . f1)
by A1, A46, A47, A48;
verum end;
then reconsider F = F as Functor of C -SliceCat (dom f),C -SliceCat (cod f) by A12, A19, CAT_1:96;
take
F
; for m being Morphism of (C -SliceCat (dom f)) holds F . m = [[(f * (m `11 )),(f * (m `12 ))],(m `2 )]
thus
for m being Morphism of (C -SliceCat (dom f)) holds F . m = [[(f * (m `11 )),(f * (m `12 ))],(m `2 )]
by A1; verum