let C be Category; for f, g being Morphism of C st dom g = cod f holds
SliceContraFunctor (g (*) f) = (SliceContraFunctor f) * (SliceContraFunctor g)
let f, g be Morphism of C; ( dom g = cod f implies SliceContraFunctor (g (*) f) = (SliceContraFunctor f) * (SliceContraFunctor g) )
assume A1:
dom g = cod f
; SliceContraFunctor (g (*) f) = (SliceContraFunctor f) * (SliceContraFunctor g)
then A2:
cod (g (*) f) = cod g
by CAT_1:17;
set A1 = (dom f) -SliceCat C;
set A2 = (cod f) -SliceCat C;
set A3 = (cod g) -SliceCat C;
reconsider F = SliceContraFunctor f as Functor of (cod f) -SliceCat C,(dom f) -SliceCat C ;
reconsider G = SliceContraFunctor g as Functor of (cod g) -SliceCat C,(cod f) -SliceCat C by A1;
reconsider FG = SliceContraFunctor (g (*) f) as Functor of (cod g) -SliceCat C,(dom f) -SliceCat C by A1, A2, CAT_1:17;
now for m being Morphism of ((cod g) -SliceCat C) holds (F * G) . m = FG . mlet m be
Morphism of
((cod g) -SliceCat C);
(F * G) . m = FG . mA3:
G . m = [[((m `11) (*) g),((m `12) (*) g)],(m `2)]
by Def14;
then A4:
(G . m) `11 = (m `11) (*) g
by MCART_1:85;
A5:
(G . m) `12 = (m `12) (*) g
by A3, MCART_1:85;
A6:
(G . m) `2 = m `2
by A3;
A7:
cod g = dom (m `11)
by Th24;
A8:
cod g = dom (m `12)
by Th24;
A9:
(m `11) (*) (g (*) f) = ((m `11) (*) g) (*) f
by A1, A7, CAT_1:18;
A10:
(m `12) (*) (g (*) f) = ((m `12) (*) g) (*) f
by A1, A8, CAT_1:18;
thus (F * G) . m =
F . (G . m)
by FUNCT_2:15
.=
[[(((m `11) (*) g) (*) f),(((m `12) (*) g) (*) f)],(m `2)]
by A4, A5, A6, Def14
.=
FG . m
by A2, A9, A10, Def14
;
verum end;
hence
SliceContraFunctor (g (*) f) = (SliceContraFunctor f) * (SliceContraFunctor g)
by FUNCT_2:63; verum