theorem Th63: :: CAT_1:68

for C, D being Category
for T being Functor of C,D
for c being Object of C holds T . (id c) = id ((Obj T) . c)