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