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