:: deftheorem defines linearly-independent VECTSP_7:def 1 :
for GF being non empty doubleLoopStr
for V being non empty ModuleStr over GF
for IT being Subset of V holds
( IT is linearly-independent iff for l being Linear_Combination of IT st Sum l = 0. V holds
Carrier l = {} );