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 :: thesis: for f being Morphism of A holds F1 . f = F2 . f
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;
set a = dom f;
set b = cod f;
Hom ((dom f),(cod f)) <> {} by CAT_1:2;
hence F1 . f = F2 . f9 by A1
.= F2 . f ;
:: thesis: verum
end;
hence F1 = F2 ; :: thesis: verum