let F1, F2 be Functor of C -SliceCat (dom f),C -SliceCat (cod f); :: thesis: ( ( 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)] ; :: thesis: F1 = F2

now :: thesis: for m being Morphism of (C -SliceCat (dom f)) holds F1 . m = F2 . m

let m be Morphism of (C -SliceCat (dom f)); :: thesis: F1 . m = F2 . m
thus F1 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] by A49
.= F2 . m by A50 ; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:63; :: thesis: verum