:: deftheorem defines = VECTSP_6:def 7 :
for GF being non empty ZeroStr
for V being non empty ModuleStr over GF
for L1, L2 being Linear_Combination of V holds
( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v );