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
object ;
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
object such that A3:
m in dom F
and A4:
x = F . m
by FUNCT_1:def 3;
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:17;
f (*) (m `11) = (f (*) (m `12)) (*) (m `2)
by A6, A7, A8, CAT_1:18;
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:4;
A12:
now for c being Object of (C -SliceCat (dom f)) ex d being Object of (C -SliceCat (cod f)) st F . (id c) = id dlet 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:85;
A16:
(id c) `12 = c
by A13, MCART_1:85;
A17:
(id c) `2 = id (dom g)
by A13;
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:17
;
verum end;
A19:
now for m being Morphism of (C -SliceCat (dom f)) holds
( F . (id (dom m)) = id (dom (F . m)) & F . (id (cod m)) = id (cod (F . m)) )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:85
;
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:85;
A25:
(id (dom m)) `12 = m `11
by A23, MCART_1:85;
(id (dom m)) `2 = id (dom (m `11))
by A23;
hence F . (id (dom m)) =
[[g1,g1],(id (dom (m `11)))]
by A1, A24, A25
.=
id (dom (F . m))
by A20, A22, CAT_1:17
;
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:85
;
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:85;
A29:
(id (cod m)) `12 = m `12
by A27, MCART_1:85;
(id (cod m)) `2 = id (dom (m `12))
by A27;
hence F . (id (cod m)) =
[[g2,g2],(id (dom (m `12)))]
by A1, A28, A29
.=
id (cod (F . m))
by A21, A26, CAT_1:17
;
verum end;
now for f1, f2 being Morphism of (C -SliceCat (dom f)) st dom f2 = cod f1 holds
F . (f2 (*) f1) = (F . f2) (*) (F . f1)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:85;
A35:
cod f1 = b1
by A30, A33, MCART_1:85;
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:85;
A37:
f1 `12 = b1
by A30, MCART_1:85;
A38:
f1 `2 = g1
by A30;
A39:
f2 `11 = a2
by A31, MCART_1:85;
A40:
f2 `12 = b2
by A31, MCART_1:85;
A41:
f2 `2 = g2
by A31;
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:85;
A48:
(f2 (*) f1) `12 = b2
by A45, MCART_1:85;
(f2 (*) f1) `2 = g2 (*) g1
by A45;
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:61;
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