for F being Field
for V being VectSp of F
for X being Subset of V holds
( X is linearly-independent iff for l1, l2 being Linear_Combination of X st Sum l1 = Sum l2 holds
l1 = l2 )