theorem Th43: :: OPPCAT_1:45

for B, C being Category
for S being Contravariant_Functor of C,B
for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp