let GF be Field; :: thesis: for V being VectSp of GF
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 V be VectSp of GF; :: 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 A1, VECTSP_7:12;
A4: Carrier L c= A \/ B by VECTSP_6:def 7;

now

assume A5: for w being Vector of V st w in A holds
L . w = 0. GF ; :: thesis: contradiction

now

let x be set ; :: thesis: ( x in Carrier L implies not x in A )
assume A6: ( x in Carrier L & x in A ) ; :: thesis: contradiction
then ex u being Vector of V st
( x = u & L . u <> 0. GF ) by VECTSP_6:19;
hence contradiction by A5, A6; :: thesis: verum

end;

then Carrier L misses A by XBOOLE_0:3;
then Carrier L c= B by A4, XBOOLE_1:73;
then L is Linear_Combination of B by VECTSP_6:def 7;
hence contradiction by A2, A3, VECTSP_7:12; :: thesis: verum

end;

then consider w being Vector of V such that
A7: w in A and
A8: L . w <> 0. GF ;
take w ; :: thesis: ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )
set a = L . w;
consider F being FinSequence of the carrier of V such that
A9: F is one-to-one and
A10: rng F = Carrier L and
A11: Sum L = Sum (L (#) F) by VECTSP_6:def 9;
A12: w in Carrier L by A8, VECTSP_6:19;
then A13: F = ((F -| w) ^ <*w*>) ^ (F |-- w) by A10, FINSEQ_4:66;
reconsider Fw1 = F -| w as FinSequence of the carrier of V by A10, A12, FINSEQ_4:53;
reconsider Fw2 = F |-- w as FinSequence of the carrier of V by A10, A12, FINSEQ_4:65;
F = Fw1 ^ (<*w*> ^ Fw2) by A13, FINSEQ_1:45;
then L (#) F = (L (#) Fw1) ^ (L (#) (<*w*> ^ Fw2)) by VECTSP_6:37
.= (L (#) Fw1) ^ ((L (#) <*w*>) ^ (L (#) Fw2)) by VECTSP_6:37
.= ((L (#) Fw1) ^ (L (#) <*w*>)) ^ (L (#) Fw2) by FINSEQ_1:45
.= ((L (#) Fw1) ^ <*((L . w) * w)*>) ^ (L (#) Fw2) by VECTSP_6:34 ;
then A14: Sum (L (#) F) = Sum ((L (#) Fw1) ^ (<*((L . w) * w)*> ^ (L (#) Fw2))) by FINSEQ_1:45
.= (Sum (L (#) Fw1)) + (Sum (<*((L . w) * w)*> ^ (L (#) Fw2))) by RLVECT_1:58
.= (Sum (L (#) Fw1)) + ((Sum <*((L . w) * w)*>) + (Sum (L (#) Fw2))) by RLVECT_1:58
.= (Sum (L (#) Fw1)) + ((Sum (L (#) Fw2)) + ((L . w) * w)) by RLVECT_1:61
.= ((Sum (L (#) Fw1)) + (Sum (L (#) Fw2))) + ((L . w) * w) by RLVECT_1:def 6
.= (Sum ((L (#) Fw1) ^ (L (#) Fw2))) + ((L . w) * w) by RLVECT_1:58
.= (Sum (L (#) (Fw1 ^ Fw2))) + ((L . w) * w) by VECTSP_6:37 ;
set Fw = Fw1 ^ Fw2;
consider K being Linear_Combination of V such that
A15: ( Carrier K = (rng (Fw1 ^ Fw2)) /\ (Carrier L) & L (#) (Fw1 ^ Fw2) = K (#) (Fw1 ^ Fw2) ) by Th8;
F just_once_values w by A9, A10, A12, FINSEQ_4:10;
then A16: Fw1 ^ Fw2 = F - {w} by FINSEQ_4:69;
then A17: rng (Fw1 ^ Fw2) = (rng F) \ {w} by FINSEQ_3:72;
A18: rng (Fw1 ^ Fw2) = (Carrier L) \ {w} by A10, A16, FINSEQ_3:72;
A19: Carrier K = rng (Fw1 ^ Fw2) by A10, A15, A17, XBOOLE_1:28;
A20: (Carrier L) \ {w} c= (A \/ B) \ {w} by A4, XBOOLE_1:33;
then reconsider K = K as Linear_Combination of (A \/ B) \ {w} by A18, A19, VECTSP_6:def 7;
( Fw1 is one-to-one & Fw2 is one-to-one & rng Fw1 misses rng Fw2 ) by A9, A10, A12, FINSEQ_4:67, FINSEQ_4:68, FINSEQ_4:72;
then Fw1 ^ Fw2 is one-to-one by FINSEQ_3:98;
then Sum (K (#) (Fw1 ^ Fw2)) = Sum K by A19, VECTSP_6:def 9;
then ((L . w) " ) * v = (((L . w) " ) * (Sum K)) + (((L . w) " ) * ((L . w) * w)) by A3, A11, A14, A15, VECTSP_1:def 26
.= (((L . w) " ) * (Sum K)) + w by A8, VECTSP_1:67 ;
then A21: w = (((L . w) " ) * v) - (((L . w) " ) * (Sum K)) by VECTSP_2:22
.= ((L . w) " ) * (v - (Sum K)) by VECTSP_1:70
.= ((L . w) " ) * ((- (Sum K)) + v) by RLVECT_1:def 12 ;
v in {v} by TARSKI:def 1;
then v in Lin {v} by VECTSP_7:13;
then consider Lv being Linear_Combination of {v} such that
A22: v = Sum Lv by VECTSP_7:12;
A23: w = ((L . w) " ) * ((Sum (- K)) + (Sum Lv)) by A21, A22, VECTSP_6:79
.= ((L . w) " ) * (Sum ((- K) + Lv)) by VECTSP_6:77
.= Sum (((L . w) " ) * ((- K) + Lv)) by VECTSP_6:78 ;
set LC = ((L . w) " ) * ((- K) + Lv);
A24: Carrier (((L . w) " ) * ((- K) + Lv)) c= Carrier ((- K) + Lv) by VECTSP_6:58;
A25: Carrier Lv c= {v} by VECTSP_6:def 7;
Carrier ((- K) + Lv) c= (Carrier (- K)) \/ (Carrier Lv) by VECTSP_6:51;
then A26: Carrier ((- K) + Lv) c= (Carrier K) \/ (Carrier Lv) by VECTSP_6:69;
(Carrier K) \/ (Carrier Lv) c= ((A \/ B) \ {w}) \/ {v} by A18, A19, A20, A25, XBOOLE_1:13;
then Carrier ((- K) + Lv) c= ((A \/ B) \ {w}) \/ {v} by A26, XBOOLE_1:1;
then Carrier (((L . w) " ) * ((- K) + Lv)) c= ((A \/ B) \ {w}) \/ {v} by A24, XBOOLE_1:1;
then ((L . w) " ) * ((- K) + Lv) is Linear_Combination of ((A \/ B) \ {w}) \/ {v} by VECTSP_6:def 7;
hence ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) by A7, A23, VECTSP_7:12; :: thesis: verum