:: deftheorem defines dom' MODCAT_1:def 8 :
for R being Ring
for V being LeftMod_DOMAIN of R
for F being Element of Morphs V holds dom' F = dom F;