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
A18: for m being Morphism of (C -SliceCat (dom f)) holds F1 . m = [[(f * (m `11 )),(f * (m `12 ))],(m `2 )] and
A19: for m being Morphism of (C -SliceCat (dom f)) holds F2 . m = [[(f * (m `11 )),(f * (m `12 ))],(m `2 )] ; :: thesis: F1 = F2

now

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 A18
.= F2 . m by A19 ; :: thesis: verum

end;

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