let C be Category; :: thesis: for f, g being Morphism of C st dom g = cod f holds
SliceFunctor (g * f) = (SliceFunctor g) * (SliceFunctor f)
let f, g be Morphism of C; :: thesis: ( dom g = cod f implies SliceFunctor (g * f) = (SliceFunctor g) * (SliceFunctor f) )
assume A1: dom g = cod f ; :: thesis: SliceFunctor (g * f) = (SliceFunctor g) * (SliceFunctor f)
then A2: dom (g * f) = dom f by CAT_1:17;
set A1 = C -SliceCat (dom f);
set A3 = C -SliceCat (cod g);
set F = SliceFunctor f;
reconsider G = SliceFunctor g as Functor of C -SliceCat (cod f),C -SliceCat (cod g) by A1;
reconsider GF = SliceFunctor (g * f) as Functor of C -SliceCat (dom f),C -SliceCat (cod g) by A1, A2, CAT_1:17;

now

let m be Morphism of (C -SliceCat (dom f)); :: thesis: (G * (SliceFunctor f)) . m = GF . m
A3: (SliceFunctor f) . m = [[(f * (m `11)),(f * (m `12))],(m `2)] by Def13;
then A4: ((SliceFunctor f) . m) `11 = f * (m `11) by MCART_1:85;
A5: ((SliceFunctor f) . m) `12 = f * (m `12) by A3, MCART_1:85;
A6: ((SliceFunctor f) . m) `2 = m `2 by A3, MCART_1:7;
A7: dom f = cod (m `11) by Th23;
A8: dom f = cod (m `12) by Th23;
A9: g * (f * (m `11)) = (g * f) * (m `11) by A1, A7, CAT_1:18;
A10: g * (f * (m `12)) = (g * f) * (m `12) by A1, A8, CAT_1:18;
thus (G * (SliceFunctor f)) . m = G . ((SliceFunctor f) . m) by FUNCT_2:15
.= [[(g * (f * (m `11))),(g * (f * (m `12)))],(m `2)] by A1, A4, A5, A6, Def13
.= GF . m by A2, A9, A10, Def13 ; :: thesis: verum

end;

hence SliceFunctor (g * f) = (SliceFunctor g) * (SliceFunctor f) by FUNCT_2:63; :: thesis: verum