:: deftheorem defines ID MODCAT_1:def 10 :
for R being Ring
for V being LeftMod_DOMAIN of R
for G being Element of V holds ID G = ID G;