theorem Th42: :: RLAFFIN1:42

for V being RealLinearSpace
for A being Subset of V holds
( A is affinely-independent iff for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} )