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
A99: for m being Morphism of ((cod f) -SliceCat C) holds F1 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] and
A100: for m being Morphism of ((cod f) -SliceCat C) holds F2 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] ; :: thesis: F1 = F2
now :: thesis: for m being Morphism of ((cod f) -SliceCat C) holds F1 . m = F2 . m
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 A99
.= F2 . m by A100 ; :: thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; :: thesis: verum