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 :: thesis: for m being Morphism of (C -SliceCat (dom f)) holds (G * (SliceFunctor f)) . m = GF . m

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;
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