theorem Th13: :: ALTCAT_4:13

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