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

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