:: deftheorem Def13 defines SliceFunctor CAT_5:def 13 :
for C being Category
for f being Morphism of C
for b₃ being Functor of C -SliceCat (dom f),C -SliceCat (cod f) holds
( b₃ = SliceFunctor f iff for m being Morphism of (C -SliceCat (dom f)) holds b₃ . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] );