let C, D be Category; :: thesis: for F being Contravariant_Functor of C,D
for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp
let F be Contravariant_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 Functor of C opp ,D by Th53;
hence (Obj ((*' F) *')) . (c opp) = ((Obj (*' F)) . (c opp)) opp by Th40
.= ((Obj F) . (opp (c opp))) opp by Th41
.= ((Obj F) . c) opp ;
:: thesis: verum