let K be Ring; :: thesis: 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) ) ) )
let V be LeftMod of K; :: thesis: 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) ) ) )
let A be finite Subset of V; :: thesis: ( 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) ) ) )

hereby :: thesis: ( 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) ) ) implies A is linearly-independent )

assume AS: A is linearly-independent ; :: thesis: ex b being FinSequence of the carrier 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) ) )
rng (canFS A) = A by FUNCT_2:def 3;
then reconsider b = canFS A as FinSequence of the carrier of V by FINSEQ_1:def 4;
take b = b; :: thesis: ( 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) ) )
thus b is one-to-one ; :: thesis: ( 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) ) )
thus rng b = A by FUNCT_2:def 3; :: thesis: 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)
hence 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) by LMBASE2, AS; :: thesis: verum

end;

given b being FinSequence of V such that A1: ( 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) ) ) ; :: thesis: A is linearly-independent
thus A is linearly-independent by A1, LMBASE2; :: thesis: verum