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