let C be Category; 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; ( dom g = cod f implies SliceFunctor (g (*) f) = (SliceFunctor g) * (SliceFunctor f) )
assume A1:
dom g = cod f
; 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 for m being Morphism of (C -SliceCat (dom f)) holds (G * (SliceFunctor f)) . m = GF . mlet m be
Morphism of
(C -SliceCat (dom f));
(G * (SliceFunctor f)) . m = GF . mA3:
(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
;
verum end;
hence
SliceFunctor (g (*) f) = (SliceFunctor g) * (SliceFunctor f)
by FUNCT_2:63; verum