let V be RealLinearSpace; :: thesis: for A being Subset of V st ( for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {} ) holds

for p being VECTOR of V st p in A holds

((- p) + A) \ {(0. V)} is linearly-independent

let A be Subset of V; :: thesis: ( ( for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {} ) implies for p being VECTOR of V st p in A holds

((- p) + A) \ {(0. V)} is linearly-independent )

assume A1: for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {} ; :: thesis: for p being VECTOR of V st p in A holds

((- p) + A) \ {(0. V)} is linearly-independent

let p be Element of V; :: thesis: ( p in A implies ((- p) + A) \ {(0. V)} is linearly-independent )

assume A2: p in A ; :: thesis: ((- p) + A) \ {(0. V)} is linearly-independent

set pA = (- p) + A;

set pA0 = ((- p) + A) \ {(0. V)};

(- p) + p = 0. V by RLVECT_1:5;

then 0. V in (- p) + A by A2;

then A3: (((- p) + A) \ {(0. V)}) \/ {(0. V)} = (- p) + A by ZFMISC_1:116;

let L be Linear_Combination of ((- p) + A) \ {(0. V)}; :: according to RLVECT_3:def 1 :: thesis: ( not Sum L = 0. V or Carrier L = {} )

assume A4: Sum L = 0. V ; :: thesis: Carrier L = {}

reconsider sL = - (sum L) as Real ;

consider Lp being Linear_Combination of {(0. V)} such that

A5: Lp . (0. V) = sL by RLVECT_4:37;

set LLp = L + Lp;

set pLLp = p + (L + Lp);

A6: Carrier Lp c= {(0. V)} by RLVECT_2:def 6;

A7: p + ((- p) + A) = (p + (- p)) + A by Th5

.= (0. V) + A by RLVECT_1:5

.= A by Th6 ;

A8: Carrier (p + (L + Lp)) = p + (Carrier (L + Lp)) by Th16;

A9: Carrier L c= ((- p) + A) \ {(0. V)} by RLVECT_2:def 6;

then ( Carrier (L + Lp) c= (Carrier L) \/ (Carrier Lp) & (Carrier L) \/ (Carrier Lp) c= (((- p) + A) \ {(0. V)}) \/ {(0. V)} ) by A6, RLVECT_2:37, XBOOLE_1:13;

then Carrier (L + Lp) c= (- p) + A by A3;

then Carrier (p + (L + Lp)) c= A by A7, A8, RLTOPSP1:8;

then A10: p + (L + Lp) is Linear_Combination of A by RLVECT_2:def 6;

A11: sum (p + (L + Lp)) = sum (L + Lp) by Th37;

A12: sum (L + Lp) = (sum L) + (sum Lp) by Th34

.= (sum L) + sL by A5, A6, Th32

.= 0 ;

then Sum (p + (L + Lp)) = (0 * p) + (Sum (L + Lp)) by Th39

.= (0. V) + (Sum (L + Lp)) by RLVECT_1:10

.= Sum (L + Lp)

.= (Sum L) + (Sum Lp) by RLVECT_3:1

.= Sum Lp by A4

.= (Lp . (0. V)) * (0. V) by RLVECT_2:32

.= 0. V ;

then Carrier (p + (L + Lp)) = {} by A1, A10, A11, A12;

then A13: p + (L + Lp) = ZeroLC V by RLVECT_2:def 5;

A14: L + Lp = (0. V) + (L + Lp) by Th21

.= ((- p) + p) + (L + Lp) by RLVECT_1:5

.= (- p) + (ZeroLC V) by A13, Th19

.= ZeroLC V by Th20 ;

assume Carrier L <> {} ; :: thesis: contradiction

then consider v being object such that

A15: v in Carrier L by XBOOLE_0:def 1;

reconsider v = v as Element of V by A15;

not v in Carrier Lp by A6, A9, A15, XBOOLE_0:def 5;

then Lp . v = 0 ;

then (L . v) + 0 = (L + Lp) . v by RLVECT_2:def 10

.= 0 by A14, RLVECT_2:20 ;

hence contradiction by A15, RLVECT_2:19; :: thesis: verum

Carrier L = {} ) holds

for p being VECTOR of V st p in A holds

((- p) + A) \ {(0. V)} is linearly-independent

let A be Subset of V; :: thesis: ( ( for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {} ) implies for p being VECTOR of V st p in A holds

((- p) + A) \ {(0. V)} is linearly-independent )

assume A1: for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {} ; :: thesis: for p being VECTOR of V st p in A holds

((- p) + A) \ {(0. V)} is linearly-independent

let p be Element of V; :: thesis: ( p in A implies ((- p) + A) \ {(0. V)} is linearly-independent )

assume A2: p in A ; :: thesis: ((- p) + A) \ {(0. V)} is linearly-independent

set pA = (- p) + A;

set pA0 = ((- p) + A) \ {(0. V)};

(- p) + p = 0. V by RLVECT_1:5;

then 0. V in (- p) + A by A2;

then A3: (((- p) + A) \ {(0. V)}) \/ {(0. V)} = (- p) + A by ZFMISC_1:116;

let L be Linear_Combination of ((- p) + A) \ {(0. V)}; :: according to RLVECT_3:def 1 :: thesis: ( not Sum L = 0. V or Carrier L = {} )

assume A4: Sum L = 0. V ; :: thesis: Carrier L = {}

reconsider sL = - (sum L) as Real ;

consider Lp being Linear_Combination of {(0. V)} such that

A5: Lp . (0. V) = sL by RLVECT_4:37;

set LLp = L + Lp;

set pLLp = p + (L + Lp);

A6: Carrier Lp c= {(0. V)} by RLVECT_2:def 6;

A7: p + ((- p) + A) = (p + (- p)) + A by Th5

.= (0. V) + A by RLVECT_1:5

.= A by Th6 ;

A8: Carrier (p + (L + Lp)) = p + (Carrier (L + Lp)) by Th16;

A9: Carrier L c= ((- p) + A) \ {(0. V)} by RLVECT_2:def 6;

then ( Carrier (L + Lp) c= (Carrier L) \/ (Carrier Lp) & (Carrier L) \/ (Carrier Lp) c= (((- p) + A) \ {(0. V)}) \/ {(0. V)} ) by A6, RLVECT_2:37, XBOOLE_1:13;

then Carrier (L + Lp) c= (- p) + A by A3;

then Carrier (p + (L + Lp)) c= A by A7, A8, RLTOPSP1:8;

then A10: p + (L + Lp) is Linear_Combination of A by RLVECT_2:def 6;

A11: sum (p + (L + Lp)) = sum (L + Lp) by Th37;

A12: sum (L + Lp) = (sum L) + (sum Lp) by Th34

.= (sum L) + sL by A5, A6, Th32

.= 0 ;

then Sum (p + (L + Lp)) = (0 * p) + (Sum (L + Lp)) by Th39

.= (0. V) + (Sum (L + Lp)) by RLVECT_1:10

.= Sum (L + Lp)

.= (Sum L) + (Sum Lp) by RLVECT_3:1

.= Sum Lp by A4

.= (Lp . (0. V)) * (0. V) by RLVECT_2:32

.= 0. V ;

then Carrier (p + (L + Lp)) = {} by A1, A10, A11, A12;

then A13: p + (L + Lp) = ZeroLC V by RLVECT_2:def 5;

A14: L + Lp = (0. V) + (L + Lp) by Th21

.= ((- p) + p) + (L + Lp) by RLVECT_1:5

.= (- p) + (ZeroLC V) by A13, Th19

.= ZeroLC V by Th20 ;

assume Carrier L <> {} ; :: thesis: contradiction

then consider v being object such that

A15: v in Carrier L by XBOOLE_0:def 1;

reconsider v = v as Element of V by A15;

not v in Carrier Lp by A6, A9, A15, XBOOLE_0:def 5;

then Lp . v = 0 ;

then (L . v) + 0 = (L + Lp) . v by RLVECT_2:def 10

.= 0 by A14, RLVECT_2:20 ;

hence contradiction by A15, RLVECT_2:19; :: thesis: verum