theorem :: OPPCAT_1:37

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