theorem Th4: :: FUNCTOR2:4

for A, B being non empty transitive with_units AltCatStr
for F being Functor of A,B
for a being Object of A holds (idt F) ! a = idm (F . a)