let V be RealLinearSpace; :: thesis: for A being Subset of V st A is affinely-independent holds
for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {}
let A be Subset of V; :: thesis: ( A is affinely-independent implies for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} )
assume A1: A is affinely-independent ; :: thesis: for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {}
let L be Linear_Combination of A; :: thesis: ( Sum L = 0. V & sum L = 0 implies Carrier L = {} )
assume that
A2: Sum L = 0. V and
A3: sum L = 0 ; :: thesis: Carrier L = {}

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: Carrier L = {}

then Carrier L c= {} by RLVECT_2:def 6;
hence Carrier L = {} ; :: thesis: verum

end;

suppose not A is empty ; :: thesis: Carrier L = {}

then consider p being VECTOR of V such that
A4: p in A and
A5: ((- p) + A) \ {(0. V)} is linearly-independent by A1;
A6: A \/ {p} = A by A4, ZFMISC_1:40;
consider Lp being Linear_Combination of {p} such that
A7: Lp . p = L . p by RLVECT_4:37;
set LLp = L - Lp;
((- p) + (L - Lp)) . (0. V) = (L - Lp) . ((0. V) - (- p)) by Def1
.= (L - Lp) . (- (- p)) by RLVECT_1:14
.= (L - Lp) . p
.= (L . p) - (Lp . p) by RLVECT_2:54
.= 0 by A7 ;
then A8: not 0. V in Carrier ((- p) + (L - Lp)) by RLVECT_2:19;
A9: Carrier Lp c= {p} by RLVECT_2:def 6;
then A10: ( Carrier Lp = {p} or Carrier Lp = {} ) by ZFMISC_1:33;
Carrier L c= A by RLVECT_2:def 6;
then ( Carrier (L - Lp) c= (Carrier L) \/ (Carrier Lp) & (Carrier L) \/ (Carrier Lp) c= A \/ {p} ) by A9, RLVECT_2:55, XBOOLE_1:13;
then A11: Carrier (L - Lp) c= A by A6;
Carrier ((- p) + (L - Lp)) = (- p) + (Carrier (L - Lp)) by Th16;
then Carrier ((- p) + (L - Lp)) c= (- p) + A by A11, RLTOPSP1:8;
then Carrier ((- p) + (L - Lp)) c= ((- p) + A) \ {(0. V)} by A8, ZFMISC_1:34;
then A12: (- p) + (L - Lp) is Linear_Combination of ((- p) + A) \ {(0. V)} by RLVECT_2:def 6;
A13: (L - Lp) + Lp = L + (Lp - Lp) by RLVECT_2:40
.= L + (ZeroLC V) by RLVECT_2:57
.= L by RLVECT_2:41 ;
A14: Sum ((- p) + Lp) = ((sum Lp) * (- p)) + (Sum Lp) by Th39
.= ((sum Lp) * (- p)) + ((Lp . p) * p) by RLVECT_2:32
.= ((Lp . p) * (- p)) + ((Lp . p) * p) by A9, Th32
.= (Lp . p) * ((- p) + p) by RLVECT_1:def 5
.= (Lp . p) * (0. V) by RLVECT_1:5
.= 0. V ;
Sum ((- p) + L) = ((sum L) * (- p)) + (Sum L) by Th39
.= (0. V) + (0. V) by A2, A3, RLVECT_1:10
.= 0. V ;
then 0. V = Sum (((- p) + (L - Lp)) + ((- p) + Lp)) by A13, Th17
.= (Sum ((- p) + (L - Lp))) + (0. V) by A14, RLVECT_3:1
.= Sum ((- p) + (L - Lp)) ;
then {} = Carrier ((- p) + (L - Lp)) by A5, A12;
then A15: ZeroLC V = (- p) + (L - Lp) by RLVECT_2:def 5;
A16: L - Lp = (0. V) + (L - Lp) by Th21
.= (p + (- p)) + (L - Lp) by RLVECT_1:5
.= p + ((- p) + (L - Lp)) by Th19
.= ZeroLC V by A15, Th20 ;
then sum (L - Lp) = 0 by Th31;
then 0 = 0 + (sum Lp) by A3, A13, Th34
.= 0 + (Lp . p) by A9, Th32 ;
then not p in Carrier Lp by RLVECT_2:19;
then (Carrier (L - Lp)) \/ (Carrier Lp) = {} by A10, A16, RLVECT_2:def 5, TARSKI:def 1;
then Carrier L c= {} by A13, RLVECT_2:37;
hence Carrier L = {} ; :: thesis: verum

end;

end;