let C, D be Category; :: thesis: for F being Functor of C,D
for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp
let F be Functor of C,D; :: thesis: for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp
let c be Object of C; :: thesis: (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp
*' F is Contravariant_Functor of C opp ,D by Th55;
hence (Obj ((*' F) *')) . (c opp) = ((Obj (*' F)) . (c opp)) opp by Th43
.= ((Obj F) . (opp (c opp))) opp by Th38
.= ((Obj F) . c) opp ;
:: thesis: verum