:: deftheorem defines - RMOD_4:def 12 :
for R being Ring
for V being RightMod of R
for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);