theorem :: OPPCAT_1:39

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