theorem :: OPPCAT_1:61

for C, D being Category
for F being Functor of C,D
for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp