:: deftheorem defines dom GRCAT_1:def 2 :
for C being Category
for O being non empty Subset of the carrier of C holds dom O = the Source of C | (Morphs O);