theorem :: OPPCAT_1:44

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