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