let C be Category; :: thesis: 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; :: thesis: ( dom g = cod f implies SliceContraFunctor (g * f) = (SliceContraFunctor f) * (SliceContraFunctor g) )
assume A1: dom g = cod f ; :: thesis: SliceContraFunctor (g * f) = (SliceContraFunctor f) * (SliceContraFunctor g)
then A2: ( dom (g * f) = dom f & cod (g * f) = cod g ) by CAT_1:42;
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 A2;

now

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

end;

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