set C1 = C -SliceCat (dom f);
set C2 = C -SliceCat (cod f);
deffunc H₁( 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 = H₁(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 ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in the carrier' of (C -SliceCat (cod f)) )
assume x in rng F ; :: thesis: 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)) ; :: thesis: 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 :: thesis: for c being Object of (C -SliceCat (dom f)) ex d being Object of (C -SliceCat (cod f)) st F . (id c) = id d

let c be Object of (C -SliceCat (dom f)); :: thesis: ex d being Object of (C -SliceCat (cod f)) st F . (id c) = id d
reconsider 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; :: thesis: F . (id c) = id d
A13: 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 ; :: thesis: verum

end;

A19: now :: thesis: 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)); :: thesis: ( 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 ;
:: thesis: 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 ;
:: thesis: verum

end;

now :: thesis: 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)); :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: verum