:: deftheorem defines - RLVECT_2:def 13 :
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);