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

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

assume BS: A is linearly-independent ; :: thesis: 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 = {}
let L be Linear_Combination of A; :: thesis: ( ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) implies Carrier L = {} )
given F being FinSequence of the carrier of V such that BS2: ( F is one-to-one & rng F = A & Sum (L (#) F) = 0. V ) ; :: thesis: Carrier L = {}
reconsider B = Carrier L as finite Subset of V ;
set F0 = canFS B;
BS3: rng (canFS B) = B by FUNCT_2:def 3;
rng (canFS B) c= the carrier of V by TARSKI:def 3;
then reconsider F0 = canFS B as FinSequence of the carrier of V by FINSEQ_1:def 4;
reconsider C = A \ B as finite Subset of V ;
set G0 = canFS C;
BS4: rng (canFS C) = C by FUNCT_2:def 3;
rng (canFS C) c= the carrier of V by TARSKI:def 3;
then reconsider G0 = canFS C as FinSequence of the carrier of V by FINSEQ_1:def 4;
BS5: (rng F0) /\ (rng G0) = B /\ (A \ B) by BS3, FUNCT_2:def 3
.= (B /\ A) \ B by XBOOLE_1:49
.= {} by XBOOLE_1:37, XBOOLE_1:17 ;
then BS6: F0 ^ G0 is one-to-one by LMBASE2A;
BS7: rng (F0 ^ G0) = B \/ (A \ B) by BS3, BS4, BS5, LMBASE2A
.= A \/ B by XBOOLE_1:39
.= A by VECTSP_6:def 4, XBOOLE_1:12 ;
(rng G0) /\ (Carrier L) = {} by BS5, FUNCT_2:def 3;
then BS10: L (#) G0 = (dom G0) --> (0. V) by LMBASE2C;
then aa: dom (L (#) G0) = dom G0 by FUNCOP_1:13;
BS12: Sum (L (#) F) = Sum (L (#) (F0 ^ G0)) by EQSUMLF, BS6, BS7, BS2
.= Sum ((L (#) F0) ^ (L (#) G0)) by VECTSP_6:13
.= (Sum (L (#) F0)) + (Sum (L (#) G0)) by RLVECT_1:41
.= (Sum (L (#) F0)) + (0. V) by BS10, LMBASE2D, aa
.= Sum (L (#) F0) ;
Sum L = 0. V by BS2, BS3, BS12, VECTSP_6:def 6;
hence Carrier L = {} by VECTSP_7:def 1, BS; :: thesis: verum

end;

assume AS: 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 = {} ; :: thesis: A is linearly-independent
for L being Linear_Combination of A st Sum L = 0. V holds
Carrier L = {}

proof

let L be Linear_Combination of A; :: thesis: ( Sum L = 0. V implies Carrier L = {} )
assume BS: Sum L = 0. V ; :: thesis: Carrier L = {}
consider F0 being FinSequence of the carrier of V such that
P3: ( F0 is one-to-one & rng F0 = Carrier L & Sum L = Sum (L (#) F0) ) by VECTSP_6:def 6;
reconsider B = Carrier L as finite Subset of V ;
reconsider C = A \ B as finite Subset of V ;
set G0 = canFS C;
BS4: rng (canFS C) = C by FUNCT_2:def 3;
rng (canFS C) c= the carrier of V by TARSKI:def 3;
then reconsider G0 = canFS C as FinSequence of the carrier of V by FINSEQ_1:def 4;
set F = F0 ^ G0;
BS5: (rng F0) /\ (rng G0) = B /\ (A \ B) by P3, FUNCT_2:def 3
.= (B /\ A) \ B by XBOOLE_1:49
.= {} by XBOOLE_1:37, XBOOLE_1:17 ;
then BS6: F0 ^ G0 is one-to-one by LMBASE2A, P3;
BS7: rng (F0 ^ G0) = B \/ (A \ B) by P3, BS4, BS5, LMBASE2A
.= A \/ B by XBOOLE_1:39
.= A by VECTSP_6:def 4, XBOOLE_1:12 ;
BS10: L (#) G0 = (dom G0) --> (0. V) by BS5, P3, LMBASE2C;
then aa: dom (L (#) G0) = dom G0 by FUNCOP_1:13;
Sum (L (#) (F0 ^ G0)) = Sum ((L (#) F0) ^ (L (#) G0)) by VECTSP_6:13
.= (Sum (L (#) F0)) + (Sum (L (#) G0)) by RLVECT_1:41
.= (Sum (L (#) F0)) + (0. V) by BS10, LMBASE2D, aa
.= Sum (L (#) F0) ;
hence Carrier L = {} by AS, BS, BS6, BS7, P3; :: thesis: verum

end;

hence A is linearly-independent by VECTSP_7:def 1; :: thesis: verum