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