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: 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 A1, A2, CAT_1:42;

now

let m be Morphism of ((cod g) -SliceCat C); :: thesis: (F * G) . m = FG . m
A3: G . m = [[((m `11 ) * g),((m `12 ) * g)],(m `2 )] by Def14;
then A4: (G . m) `11 = (m `11 ) * g by MCART_1:89;
A5: (G . m) `12 = (m `12 ) * g by A3, MCART_1:89;
A6: (G . m) `2 = m `2 by A3, MCART_1:7;
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:43;
A10: (m `12 ) * (g * f) = ((m `12 ) * g) * f by A1, A8, 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 A4, A5, A6, Def14
.= FG . m by A2, A9, A10, Def14 ; :: thesis: verum

end;

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