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 f9 = f as Morphism of dom f, cod f by CAT_1:4;
A2: Hom ((dom f),(cod f)) <> {} by CAT_1:2;
hence F1 . f = F1 . f9 by Def1
.= F2 . f9 by A1, A2
.= F2 . f by A2, Def1 ;
:: thesis: verum

end;

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