theorem :: CAT_1:62

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