for C being Category
for f, g being Morphism of C st dom g = cod f holds
SliceContraFunctor (g (*) f) = (SliceContraFunctor f) * (SliceContraFunctor g)