let A, B be Category; :: thesis: for F1, F2 being Functor of A,B st ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds F1 . f = F2 . f ) holds
F1 = F2
let F1, F2 be Functor of A,B; :: thesis: ( ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds F1 . f = F2 . f ) implies F1 = F2 )
assume A1: for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds F1 . f = F2 . f ; :: thesis: F1 = F2

now

let f be Morphism of A; :: thesis: F1 . f = F2 . f
reconsider f' = f as Morphism of dom f, cod f by CAT_1:22;
A2: Hom (dom f),(cod f) <> {} by CAT_1:19;
hence F1 . f = F1 . f' by Def1
.= F2 . f' by A1, A2
.= F2 . f by A2, Def1 ;
:: thesis: verum

end;

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