theorem :: OPPCAT_1:38

for B, C being Category
for S being Contravariant_Functor of C opp ,B holds /* S is Functor of C,B