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