:: deftheorem defines @ RLVECT_2:def 16 :
for V being RealLinearSpace
for L being Linear_Combination of V holds @ L = L;