:: deftheorem defines @ ZMODUL02:def 30 :
for R being Ring
for V being LeftMod of R
for e being Element of LinComb V holds @ e = e;