theorem Th22: :: CATALG_1:22

for C1, C2 being Category
for F being Functor of C1,C2
for a being Object of C1 holds (Psi F) . (idsym a) = idsym (F . a)