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