:: deftheorem Def10 defines *' OPPCAT_1:def 10 :
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 opp), the carrier' of B holds
( b₄ = *' S iff for f being Morphism of (C opp) holds b₄ . f = S . (opp f) );