let A, B be Category; :: thesis: for F being Functor of A,B
for c being Object of A
for d being Object of B st F /. (id c) = id d holds
F . c = d
let F be Functor of A,B; :: thesis: for c being Object of A
for d being Object of B st F /. (id c) = id d holds
F . c = d
let c be Object of A; :: thesis: for d being Object of B st F /. (id c) = id d holds
F . c = d
let d be Object of B; :: thesis: ( F /. (id c) = id d implies F . c = d )
A1: Hom (c,c) <> {} ;
assume F /. (id c) = id d ; :: thesis: F . c = d
then F . (id c) = id d by A1, CAT_3:def 10;
hence F . c = d by CAT_1:70; :: thesis: verum