theorem :: CAT_1:70

for C, D being Category
for T being Functor of C,D
for c being Object of C
for d being Object of D st T . (id c) = id d holds
T . c = d by Th62;