set C1 = (cod f) -SliceCat C;
set C2 = (dom f) -SliceCat C;
deffunc H₁( Morphism of ((cod f) -SliceCat C)) -> Element of the carrier' of [:[:C,C:],C:] = [[(($1 `11) (*) f),(($1 `12) (*) f)],($1 `2)];
consider F being Function of the carrier' of ((cod f) -SliceCat C), the carrier' of [:[:C,C:],C:] such that
A51: for m being Morphism of ((cod f) -SliceCat C) holds F . m = H₁(m) from FUNCT_2:sch 4();
A52: dom F = the carrier' of ((cod f) -SliceCat C) by FUNCT_2:def 1;
rng F c= the carrier' of ((dom f) -SliceCat C)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in the carrier' of ((dom f) -SliceCat C) )
assume x in rng F ; :: thesis: x in the carrier' of ((dom f) -SliceCat C)
then consider m being object such that
A53: m in dom F and
A54: x = F . m by FUNCT_1:def 3;
reconsider m = m as Morphism of ((cod f) -SliceCat C) by A53;
A55: x = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] by A51, A54;
A56: dom (m `2) = cod (m `11) by Th31;
A57: m `12 = (m `2) (*) (m `11) by Th31;
A58: dom (m `11) = cod f by Th24;
A59: (m `11) (*) f in (dom f) Hom by Th28;
A60: (m `12) (*) f in (dom f) Hom by Th28;
A61: cod ((m `11) (*) f) = dom (m `2) by A56, A58, CAT_1:17;
(m `12) (*) f = (m `2) (*) ((m `11) (*) f) by A56, A57, A58, CAT_1:18;
then x is Morphism of ((dom f) -SliceCat C) by A55, A59, A60, A61, Def12;
hence x in the carrier' of ((dom f) -SliceCat C) ; :: thesis: verum

end;

then reconsider F = F as Function of the carrier' of ((cod f) -SliceCat C), the carrier' of ((dom f) -SliceCat C) by A52, FUNCT_2:def 1, RELSET_1:4;

A62: now :: thesis: for c being Object of ((cod f) -SliceCat C) ex d being Object of ((dom f) -SliceCat C) st F . (id c) = id d

let c be Object of ((cod f) -SliceCat C); :: thesis: ex d being Object of ((dom f) -SliceCat C) st F . (id c) = id d
reconsider g = c as Element of (cod f) Hom by Def12;
reconsider h = g (*) f as Element of (dom f) Hom by Th28;
reconsider d = h as Object of ((dom f) -SliceCat C) by Def12;
take d = d; :: thesis: F . (id c) = id d
A63: id c = [[c,c],(id (cod g))] by Th32;
A64: id d = [[d,d],(id (cod h))] by Th32;
A65: (id c) `11 = c by A63, MCART_1:85;
A66: (id c) `12 = c by A63, MCART_1:85;
A67: (id c) `2 = id (cod g) by A63;
A68: dom g = cod f by Th24;
thus F . (id c) = [[h,h],((id c) `2)] by A51, A65, A66
.= id d by A64, A67, A68, CAT_1:17 ; :: thesis: verum

end;

A69: now :: thesis: for m being Morphism of ((cod f) -SliceCat C) holds
( F . (id (dom m)) = id (dom (F . m)) & F . (id (cod m)) = id (cod (F . m)) )

let m be Morphism of ((cod f) -SliceCat C); :: thesis: ( F . (id (dom m)) = id (dom (F . m)) & F . (id (cod m)) = id (cod (F . m)) )
reconsider g1 = (m `11) (*) f, g2 = (m `12) (*) f as Element of (dom f) Hom by Th28;
A70: cod f = dom (m `11) by Th24;
A71: cod f = dom (m `12) by Th24;
F . m = [[g1,g2],(m `2)] by A51;
then dom (F . m) = [[g1,g2],(m `2)] `11 by Th31
.= g1 by MCART_1:85 ;
then A72: id (dom (F . m)) = [[g1,g1],(id (cod g1))] by Th32;
dom m = m `11 by Th31;
then A73: id (dom m) = [[(m `11),(m `11)],(id (cod (m `11)))] by Th32;
then A74: (id (dom m)) `11 = m `11 by MCART_1:85;
A75: (id (dom m)) `12 = m `11 by A73, MCART_1:85;
(id (dom m)) `2 = id (cod (m `11)) by A73;
hence F . (id (dom m)) = [[g1,g1],(id (cod (m `11)))] by A51, A74, A75
.= id (dom (F . m)) by A70, A72, CAT_1:17 ;
:: thesis: F . (id (cod m)) = id (cod (F . m))
F . m = [[g1,g2],(m `2)] by A51;
then cod (F . m) = [[g1,g2],(m `2)] `12 by Th31
.= g2 by MCART_1:85 ;
then A76: id (cod (F . m)) = [[g2,g2],(id (cod g2))] by Th32;
cod m = m `12 by Th31;
then A77: id (cod m) = [[(m `12),(m `12)],(id (cod (m `12)))] by Th32;
then A78: (id (cod m)) `11 = m `12 by MCART_1:85;
A79: (id (cod m)) `12 = m `12 by A77, MCART_1:85;
(id (cod m)) `2 = id (cod (m `12)) by A77;
hence F . (id (cod m)) = [[g2,g2],(id (cod (m `12)))] by A51, A78, A79
.= id (cod (F . m)) by A71, A76, CAT_1:17 ;
:: thesis: verum

end;

now :: thesis: for f1, f2 being Morphism of ((cod f) -SliceCat C) st dom f2 = cod f1 holds
F . (f2 (*) f1) = (F . f2) (*) (F . f1)

let f1, f2 be Morphism of ((cod f) -SliceCat C); :: thesis: ( dom f2 = cod f1 implies F . (f2 (*) f1) = (F . f2) (*) (F . f1) )
consider a1, b1 being Element of (cod f) Hom , g1 being Morphism of C such that
A80: f1 = [[a1,b1],g1] and
dom g1 = cod a1 and
g1 (*) a1 = b1 by Def12;
consider a2, b2 being Element of (cod f) Hom , g2 being Morphism of C such that
A81: f2 = [[a2,b2],g2] and
dom g2 = cod a2 and
g2 (*) a2 = b2 by Def12;
A82: dom f2 = f2 `11 by Th2;
A83: cod f1 = f1 `12 by Th2;
A84: dom f2 = a2 by A81, A82, MCART_1:85;
A85: cod f1 = b1 by A80, A83, MCART_1:85;
reconsider ha1 = a1 (*) f, ha2 = a2 (*) f, hb1 = b1 (*) f, hb2 = b2 (*) f as Element of (dom f) Hom by Th28;
A86: f1 `11 = a1 by A80, MCART_1:85;
A87: f1 `12 = b1 by A80, MCART_1:85;
A88: f1 `2 = g1 by A80;
A89: f2 `11 = a2 by A81, MCART_1:85;
A90: f2 `12 = b2 by A81, MCART_1:85;
A91: f2 `2 = g2 by A81;
A92: F . f1 = [[ha1,hb1],g1] by A51, A86, A87, A88;
A93: F . f2 = [[ha2,hb2],g2] by A51, A89, A90, A91;
assume A94: dom f2 = cod f1 ; :: thesis: F . (f2 (*) f1) = (F . f2) (*) (F . f1)
then A95: f2 (*) f1 = [[a1,b2],(g2 (*) g1)] by A80, A81, A84, A85, Def12;
A96: (F . f2) (*) (F . f1) = [[ha1,hb2],(g2 (*) g1)] by A84, A85, A92, A93, A94, Def12;
A97: (f2 (*) f1) `11 = a1 by A95, MCART_1:85;
A98: (f2 (*) f1) `12 = b2 by A95, MCART_1:85;
(f2 (*) f1) `2 = g2 (*) g1 by A95;
hence F . (f2 (*) f1) = (F . f2) (*) (F . f1) by A51, A96, A97, A98; :: thesis: verum

end;

then reconsider F = F as Functor of (cod f) -SliceCat C,(dom f) -SliceCat C by A62, A69, CAT_1:61;
take F ; :: thesis: for m being Morphism of ((cod f) -SliceCat C) holds F . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)]
thus for m being Morphism of ((cod f) -SliceCat C) holds F . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] by A51; :: thesis: verum