let F1, F2 be Functor of C -SliceCat (dom f),C -SliceCat (cod f); ( ( for m being Morphism of (C -SliceCat (dom f)) holds F1 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] ) & ( for m being Morphism of (C -SliceCat (dom f)) holds F2 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] ) implies F1 = F2 )
assume that
A49:
for m being Morphism of (C -SliceCat (dom f)) holds F1 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)]
and
A50:
for m being Morphism of (C -SliceCat (dom f)) holds F2 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)]
; F1 = F2
hence
F1 = F2
by FUNCT_2:63; verum