:: deftheorem defines - RLVECT_2:def 12 :
for V being RealLinearSpace
for L being Linear_Combination of V holds - L = (- 1) * L;