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 set ; :: 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 set such that
A3: ( m in dom F & x = F . m ) by FUNCT_1:def 5;
reconsider m = m as Morphism of (C -SliceCat (dom f)) by A3;
A4: x = [[(f * (m `11 )),(f * (m `12 ))],(m `2 )] by A1, A3;
( dom (m `12 ) = cod (m `2 ) & m `11 = (m `12 ) * (m `2 ) & cod (m `12 ) = dom f ) by Th23, Th29;
then ( f * (m `11 ) in Hom (cod f) & f * (m `12 ) in Hom (cod f) & dom (f * (m `12 )) = cod (m `2 ) & f * (m `11 ) = (f * (m `12 )) * (m `2 ) ) by Th27, CAT_1:42, CAT_1:43;
then x is Morphism of (C -SliceCat (cod f)) by A4, 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:11;

A5: now

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
A6: ( id c = [[c,c],(id (dom g))] & id d = [[d,d],(id (dom h))] ) by Th30;
then A7: ( (id c) `11 = c & (id c) `12 = c & (id c) `2 = id (dom g) & (id d) `11 = d & (id d) `12 = d & (id d) `2 = id (dom h) ) by MCART_1:7, MCART_1:89;
A8: cod g = dom f by Th23;
thus F . (id c) = [[h,h],((id c) `2 )] by A1, A7
.= id d by A6, A7, A8, CAT_1:42 ; :: thesis: verum

end;

A9: now

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;
A10: ( dom f = cod (m `11 ) & 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 A11: id (dom (F . m)) = [[g1,g1],(id (dom g1))] by Th30;
dom m = m `11 by Th29;
then id (dom m) = [[(m `11 ),(m `11 )],(id (dom (m `11 )))] by Th30;
then ( (id (dom m)) `11 = m `11 & (id (dom m)) `12 = m `11 & (id (dom m)) `2 = id (dom (m `11 )) ) by MCART_1:7, MCART_1:89;
hence F . (id (dom m)) = [[g1,g1],(id (dom (m `11 )))] by A1
.= id (dom (F . m)) by A10, A11, CAT_1:42 ;
:: 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:89 ;
then A12: id (cod (F . m)) = [[g2,g2],(id (dom g2))] by Th30;
cod m = m `12 by Th29;
then id (cod m) = [[(m `12 ),(m `12 )],(id (dom (m `12 )))] by Th30;
then ( (id (cod m)) `11 = m `12 & (id (cod m)) `12 = m `12 & (id (cod m)) `2 = id (dom (m `12 )) ) by MCART_1:7, MCART_1:89;
hence F . (id (cod m)) = [[g2,g2],(id (dom (m `12 )))] by A1
.= id (cod (F . m)) by A10, A12, CAT_1:42 ;
:: thesis: verum

end;

now

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
A13: ( f1 = [[a1,b1],g1] & dom b1 = cod g1 & a1 = b1 * g1 ) by Def11;
consider a2, b2 being Element of Hom (dom f), g2 being Morphism of C such that
A14: ( f2 = [[a2,b2],g2] & dom b2 = cod g2 & a2 = b2 * g2 ) by Def11;
( dom f2 = f2 `11 & cod f1 = f1 `12 ) by Th2;
then A15: ( dom f2 = a2 & cod f1 = b1 ) by A13, A14, MCART_1:89;
reconsider ha1 = f * a1, ha2 = f * a2, hb1 = f * b1, hb2 = f * b2 as Element of Hom (cod f) by Th27;
( f1 `11 = a1 & f1 `12 = b1 & f1 `2 = g1 & f2 `11 = a2 & f2 `12 = b2 & f2 `2 = g2 ) by A13, A14, MCART_1:7, MCART_1:89;
then A16: ( F . f1 = [[ha1,hb1],g1] & F . f2 = [[ha2,hb2],g2] ) by A1;
assume dom f2 = cod f1 ; :: thesis: F . (f2 * f1) = (F . f2) * (F . f1)
then A17: ( f2 * f1 = [[a1,b2],(g2 * g1)] & (F . f2) * (F . f1) = [[ha1,hb2],(g2 * g1)] ) by A13, A14, A15, A16, Def11;
then ( (f2 * f1) `11 = a1 & (f2 * f1) `12 = b2 & (f2 * f1) `2 = g2 * g1 ) by MCART_1:7, MCART_1:89;
hence F . (f2 * f1) = (F . f2) * (F . f1) by A1, A17; :: thesis: verum

end;

then reconsider F = F as Functor of C -SliceCat (dom f),C -SliceCat (cod f) by A5, A9, CAT_1:96;
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