:: deftheorem defines @ ZMODUL02:def 31 :
for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V holds @ L = L;