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