:: deftheorem defines = RLVECT_2:def 9 :
for V being non empty addLoopStr
for L1, L2 being Linear_Combination of V holds
( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v );