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) ) ) )

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

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 )

given b being FinSequence of V such that A1:
( b is one-to-one & rng b = A & ( for r being FinSequence of K( 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;( 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

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