theorem :: OPPCAT_1:64

for C, D being Category
for F being Contravariant_Functor of C,D holds (*' F) *' is Contravariant_Functor of C opp ,D opp