theorem LMBASE2: :: ZMODLAT2:3

for K being Ring
for V being LeftMod of K
for b being FinSequence of V st b is one-to-one holds
( rng b is linearly-independent iff 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) )