:: deftheorem Def11 defines *' OPPCAT_1:def 11 :
for C, B being Category
for S being Function of the carrier' of C, the carrier' of B
for b₄ being Function of the carrier' of C, the carrier' of (B opp) holds
( b₄ = S *' iff for f being Morphism of C holds b₄ . f = (S . f) opp );