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 )
assume A1: F . (id c) = id d ; :: thesis: F . c = d
Hom c,c <> {} by CAT_1:56;
then F . (id c) = id d by A1, Def1;
hence F . c = d by CAT_1:107; :: thesis: verum