theorem Th26: :: OPPCAT_1:28

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