:: deftheorem defines linearly-independent RLVECT_3:def 1 :
for V being RealLinearSpace
for A being Subset of V holds
( A is linearly-independent iff for l being Linear_Combination of A st Sum l = 0. V holds
Carrier l = {} );