let C, D be Category; :: thesis: for F being Functor of C,D holds (*' F) *' is Functor of C opp ,D opp
let F be Functor of C,D; :: thesis: (*' F) *' is Functor of C opp ,D opp
*' F is Contravariant_Functor of C opp ,D by Th55;
hence (*' F) *' is Functor of C opp ,D opp by Th54; :: thesis: verum