theorem Th41: :: OPPCAT_1:43

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