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:
reconsider B = Carrier L as finite Subset of V ;
set F0 = canFS B;
BS3: rng () = B by FUNCT_2:def 3;
rng () 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 () = C by FUNCT_2:def 3;
rng () 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
.= (B /\ A) \ B by XBOOLE_1:49
.= {} by ;
then BS6: F0 ^ G0 is one-to-one by LMBASE2A;
BS7: rng (F0 ^ G0) = B \/ (A \ B) by
.= A \/ B by XBOOLE_1:39
.= A by ;
(rng G0) /\ () = {} by ;
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
.= 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
.= Sum (L (#) F0) ;
Sum L = 0. V by ;
hence Carrier L = {} by ; :: 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:
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:
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 () = C by FUNCT_2:def 3;
rng () 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
.= (B /\ A) \ B by XBOOLE_1:49
.= {} by ;
then BS6: F0 ^ G0 is one-to-one by ;
BS7: rng (F0 ^ G0) = B \/ (A \ B) by
.= A \/ B by XBOOLE_1:39
.= A by ;
BS10: L (#) G0 = (dom G0) --> (0. V) by ;
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
.= 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