theorem :: ZMODLAT2:4

for K being Ring
for V being LeftMod of K
for A being finite Subset of V holds
( A is linearly-independent iff ex b being FinSequence of V st
( b is one-to-one & rng b = A & ( for r being FinSequence of K
for rb being FinSequence of V st len r = len b & len rb = len b & ( for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) ) & Sum rb = 0. V holds
r = (Seg (len r)) --> (0. K) ) ) )