theorem Th28: :: OPPCAT_1:30

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