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 & cod (g * f) = cod g ) by CAT_1:42;
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 A2;

now

let m be Morphism of (C -SliceCat (dom f)); :: thesis: (G * (SliceFunctor f)) . m = GF . m
(SliceFunctor f) . m = [[(f * (m `11 )),(f * (m `12 ))],(m `2 )] by Def13;
then A3: ( ((SliceFunctor f) . m) `11 = f * (m `11 ) & ((SliceFunctor f) . m) `12 = f * (m `12 ) & ((SliceFunctor f) . m) `2 = m `2 ) by MCART_1:7, MCART_1:89;
( dom f = cod (m `11 ) & dom f = cod (m `12 ) ) by Th23;
then A4: ( g * (f * (m `11 )) = (g * f) * (m `11 ) & g * (f * (m `12 )) = (g * f) * (m `12 ) ) by A1, CAT_1:43;
thus (G * (SliceFunctor f)) . m = G . ((SliceFunctor f) . m) by FUNCT_2:21
.= [[(g * (f * (m `11 ))),(g * (f * (m `12 )))],(m `2 )] by A1, A3, Def13
.= GF . m by A2, A4, Def13 ; :: thesis: verum

end;

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