theorem :: OPPCAT_1:27

for B, C being Category
for S being Function of the carrier' of (C opp), the carrier' of B
for f being Morphism of (C opp) holds (/* S) . (opp f) = S . f