theorem :: OPPCAT_1:29

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