:: deftheorem defines = CONVEX4:def 7 :
for V being non empty addLoopStr
for L1, L2 being C_Linear_Combination of V holds
( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v );