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 Th58;
hence (Obj ((*' F) *' )) . (c opp ) = ((Obj (*' F)) . (c opp )) opp by Th46
.= ((Obj F) . (opp (c opp ))) opp by Th41
.= ((Obj F) . c) opp ;
:: thesis: verum