:: deftheorem Def4 defines opp CAT_3:def 4 :
for C being Category
for I being set
for F being Function of I, the carrier' of (C opp)
for b₄ being Function of I, the carrier' of C holds
( b₄ = opp F iff for x being set st x in I holds
b₄ /. x = opp (F /. x) );