theorem Th29: :: OPPCAT_1:31

for C, D being Category
for S being Contravariant_Functor of C,D
for c being Object of C holds S . (id c) = id ((Obj S) . c)