let F1, F2 be Functor of (cod f) -SliceCat C,(dom f) -SliceCat C; :: thesis: ( ( for m being Morphism of ((cod f) -SliceCat C) holds F1 . m = [[((m `11 ) * f),((m `12 ) * f)],(m `2 )] ) & ( for m being Morphism of ((cod f) -SliceCat C) holds F2 . m = [[((m `11 ) * f),((m `12 ) * f)],(m `2 )] ) implies F1 = F2 )
assume that
A37: for m being Morphism of ((cod f) -SliceCat C) holds F1 . m = [[((m `11 ) * f),((m `12 ) * f)],(m `2 )] and
A38: for m being Morphism of ((cod f) -SliceCat C) holds F2 . m = [[((m `11 ) * f),((m `12 ) * f)],(m `2 )] ; :: thesis: F1 = F2

now

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

end;

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