theorem LMBASE2X: :: ZMODLAT2:2

for K being Ring
for V being LeftMod of K
for A being finite Subset of V holds
( A is linearly-independent iff for L being Linear_Combination of A st ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) holds
Carrier L = {} )