:: deftheorem Def1 defines doms CAT_3:def 1 :
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₄ = doms F iff for x being set st x in I holds
b₄ /. x = dom (F /. x) );