:: deftheorem defines dom MOD_2:def 3 :
for R being Ring
for f being LModMorphismStr over R holds dom f = the Dom of f;