:: deftheorem defines - RMOD_4:def 11 :
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds - L = L * (- (1_ R));