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: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 :: thesis: for m being Morphism of ((cod g) -SliceCat C) holds (F * G) . m = FG . m

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: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 ; :: thesis: verum

end;

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