theorem Th16: :: NATTRA_1:20

for A, B being Category
for F being Functor of A,B
for a being Object of A holds (id F) . a = id (F . a)