let V be RealLinearSpace; :: thesis: for A, B being finite Subset of V
for v being VECTOR of V st v in Lin (A \/ B) & not v in Lin B holds
ex w being VECTOR of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )

let A, B be finite Subset of V; :: thesis: for v being VECTOR of V st v in Lin (A \/ B) & not v in Lin B holds
ex w being VECTOR of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )

let v be VECTOR of V; :: thesis: ( v in Lin (A \/ B) & not v in Lin B implies ex w being VECTOR of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) )

assume that
A1: v in Lin (A \/ B) and
A2: not v in Lin B ; :: thesis: ex w being VECTOR of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )

consider L being Linear_Combination of A \/ B such that
A3: v = Sum L by ;
A4: Carrier L c= A \/ B by RLVECT_2:def 6;
now :: thesis: ex w being VECTOR of V st
( w in A & not L . w = 0 )
assume A5: for w being VECTOR of V st w in A holds
L . w = 0 ; :: thesis: contradiction
now :: thesis: for x being object st x in Carrier L holds
not x in A
let x be object ; :: thesis: ( x in Carrier L implies not x in A )
assume that
A6: x in Carrier L and
A7: x in A ; :: thesis: contradiction
ex u being VECTOR of V st
( x = u & L . u <> 0 ) by ;
hence contradiction by A5, A7; :: thesis: verum
end;
then Carrier L misses A by XBOOLE_0:3;
then Carrier L c= B by ;
then L is Linear_Combination of B by RLVECT_2:def 6;
hence contradiction by A2, A3, RLVECT_3:14; :: thesis: verum
end;
then consider w being VECTOR of V such that
A8: w in A and
A9: L . w <> 0 ;
set a = L . w;
take w ; :: thesis: ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )
consider F being FinSequence of the carrier of V such that
A10: F is one-to-one and
A11: rng F = Carrier L and
A12: Sum L = Sum (L (#) F) by RLVECT_2:def 8;
A13: w in Carrier L by ;
then reconsider Fw1 = F -| w as FinSequence of the carrier of V by ;
reconsider Fw2 = F |-- w as FinSequence of the carrier of V by ;
A14: rng Fw1 misses rng Fw2 by ;
set Fw = Fw1 ^ Fw2;
F just_once_values w by ;
then A15: Fw1 ^ Fw2 = F - {w} by FINSEQ_4:54;
then A16: rng (Fw1 ^ Fw2) = () \ {w} by ;
F = ((F -| w) ^ <*w*>) ^ (F |-- w) by ;
then F = Fw1 ^ (<*w*> ^ Fw2) by FINSEQ_1:32;
then L (#) F = (L (#) Fw1) ^ (L (#) (<*w*> ^ Fw2)) by RLVECT_3:34
.= (L (#) Fw1) ^ ((L (#) <*w*>) ^ (L (#) Fw2)) by RLVECT_3:34
.= ((L (#) Fw1) ^ (L (#) <*w*>)) ^ (L (#) Fw2) by FINSEQ_1:32
.= ((L (#) Fw1) ^ <*((L . w) * w)*>) ^ (L (#) Fw2) by RLVECT_2:26 ;
then A17: Sum (L (#) F) = Sum ((L (#) Fw1) ^ (<*((L . w) * w)*> ^ (L (#) Fw2))) by FINSEQ_1:32
.= (Sum (L (#) Fw1)) + (Sum (<*((L . w) * w)*> ^ (L (#) Fw2))) by RLVECT_1:41
.= (Sum (L (#) Fw1)) + ((Sum <*((L . w) * w)*>) + (Sum (L (#) Fw2))) by RLVECT_1:41
.= (Sum (L (#) Fw1)) + ((Sum (L (#) Fw2)) + ((L . w) * w)) by RLVECT_1:44
.= ((Sum (L (#) Fw1)) + (Sum (L (#) Fw2))) + ((L . w) * w) by RLVECT_1:def 3
.= (Sum ((L (#) Fw1) ^ (L (#) Fw2))) + ((L . w) * w) by RLVECT_1:41
.= (Sum (L (#) (Fw1 ^ Fw2))) + ((L . w) * w) by RLVECT_3:34 ;
v in {v} by TARSKI:def 1;
then v in Lin {v} by RLVECT_3:15;
then consider Lv being Linear_Combination of {v} such that
A18: v = Sum Lv by RLVECT_3:14;
consider K being Linear_Combination of V such that
A19: Carrier K = (rng (Fw1 ^ Fw2)) /\ () and
A20: L (#) (Fw1 ^ Fw2) = K (#) (Fw1 ^ Fw2) by Th7;
rng (Fw1 ^ Fw2) = (rng F) \ {w} by ;
then A21: Carrier K = rng (Fw1 ^ Fw2) by ;
A22: (Carrier L) \ {w} c= (A \/ B) \ {w} by ;
then reconsider K = K as Linear_Combination of (A \/ B) \ {w} by ;
(L . w) " <> 0 by ;
then A23: Carrier (((L . w) ") * ((- K) + Lv)) = Carrier ((- K) + Lv) by RLVECT_2:42;
set LC = ((L . w) ") * ((- K) + Lv);
Carrier ((- K) + Lv) c= (Carrier (- K)) \/ (Carrier Lv) by RLVECT_2:37;
then A24: Carrier ((- K) + Lv) c= () \/ (Carrier Lv) by RLVECT_2:51;
Carrier Lv c= {v} by RLVECT_2:def 6;
then (Carrier K) \/ (Carrier Lv) c= ((A \/ B) \ {w}) \/ {v} by ;
then Carrier ((- K) + Lv) c= ((A \/ B) \ {w}) \/ {v} by A24;
then A25: ((L . w) ") * ((- K) + Lv) is Linear_Combination of ((A \/ B) \ {w}) \/ {v} by ;
( Fw1 is one-to-one & Fw2 is one-to-one ) by ;
then Fw1 ^ Fw2 is one-to-one by ;
then Sum (K (#) (Fw1 ^ Fw2)) = Sum K by ;
then ((L . w) ") * v = (((L . w) ") * (Sum K)) + (((L . w) ") * ((L . w) * w)) by
.= (((L . w) ") * (Sum K)) + ((((L . w) ") * (L . w)) * w) by RLVECT_1:def 7
.= (((L . w) ") * (Sum K)) + (1 * w) by
.= (((L . w) ") * (Sum K)) + w by RLVECT_1:def 8 ;
then w = (((L . w) ") * v) - (((L . w) ") * (Sum K)) by RLSUB_2:61
.= ((L . w) ") * (v - (Sum K)) by RLVECT_1:34
.= ((L . w) ") * ((- (Sum K)) + v) by RLVECT_1:def 11 ;
then w = ((L . w) ") * ((Sum (- K)) + (Sum Lv)) by
.= ((L . w) ") * (Sum ((- K) + Lv)) by RLVECT_3:1
.= Sum (((L . w) ") * ((- K) + Lv)) by RLVECT_3:2 ;
hence ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) by ; :: thesis: verum