:: deftheorem defines @ RLVECT_2:def 15 :
for V being RealLinearSpace
for e being Element of LinComb V holds @ e = e;