theorem :: OPPCAT_1:48

for C, D being Category
for S being Function of the carrier' of (C opp), the carrier' of D holds *' (/* S) = S