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 Th57;
hence (*' F) *' is Functor of C opp ,D opp by Th56; :: thesis: verum