let GF be Field; :: thesis: for V being VectSp of GF
for A being Subset of V st A is linearly-independent holds
for v being Vector of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B
let V be VectSp of GF; :: thesis: for A being Subset of V st A is linearly-independent holds
for v being Vector of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B
let A be Subset of V; :: thesis: ( A is linearly-independent implies for v being Vector of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B )
assume A1: A is linearly-independent ; :: thesis: for v being Vector of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B
let v be Vector of V; :: thesis: ( v in A implies for B being Subset of V st B = A \ {v} holds
not v in Lin B )
assume A2: v in A ; :: thesis: for B being Subset of V st B = A \ {v} holds
not v in Lin B
let B be Subset of V; :: thesis: ( B = A \ {v} implies not v in Lin B )
assume A3: B = A \ {v} ; :: thesis: not v in Lin B
assume v in Lin B ; :: thesis: contradiction
then consider L being Linear_Combination of B such that
A4: v = Sum L by VECTSP_7:12;
v in {v} by TARSKI:def 1;
then v in Lin {v} by VECTSP_7:13;
then consider K being Linear_Combination of {v} such that
A5: v = Sum K by VECTSP_7:12;
A6: 0. V = (Sum L) + (- (Sum K)) by A4, A5, RLVECT_1:def 11
.= (Sum L) + (Sum (- K)) by VECTSP_6:79
.= Sum (L + (- K)) by VECTSP_6:77
.= Sum (L - K) by VECTSP_6:def 14 ;
A7: {v} is Subset of A by A2, SUBSET_1:63;
then A8: ( {v} c= A & B c= A ) by A3, XBOOLE_1:36;
{v} is linearly-independent by A1, A7, VECTSP_7:2;
then v <> 0. V by VECTSP_7:5;
then Carrier L <> {} by A4, VECTSP_6:45;
then consider w being set such that
A9: w in Carrier L by XBOOLE_0:def 1;
A10: Carrier (L - K) c= (Carrier L) \/ (Carrier K) by VECTSP_6:74;
A11: ( Carrier L c= B & Carrier K c= {v} ) by VECTSP_6:def 7;
then A12: (Carrier L) \/ (Carrier K) c= B \/ {v} by XBOOLE_1:13;
B \/ {v} c= A \/ A by A8, XBOOLE_1:13;
then (Carrier L) \/ (Carrier K) c= A by A12, XBOOLE_1:1;
then Carrier (L - K) c= A by A10, XBOOLE_1:1;
then A13: L - K is Linear_Combination of A by VECTSP_6:def 7;
A14: for x being Vector of V st x in Carrier L holds
K . x = 0. GF

proof

let x be Vector of V; :: thesis: ( x in Carrier L implies K . x = 0. GF )
assume x in Carrier L ; :: thesis: K . x = 0. GF
then not x in Carrier K by A3, A11, XBOOLE_0:def 5;
hence K . x = 0. GF by VECTSP_6:20; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in Carrier L implies x in Carrier (L - K) )
assume that
A15: x in Carrier L and
A16: not x in Carrier (L - K) ; :: thesis: contradiction
reconsider x = x as Vector of V by A15;
A17: L . x <> 0. GF by A15, VECTSP_6:20;
(L - K) . x = (L . x) - (K . x) by VECTSP_6:73
.= (L . x) - (0. GF) by A14, A15
.= (L . x) + (- (0. GF)) by RLVECT_1:def 12
.= (L . x) + (0. GF) by RLVECT_1:25
.= L . x by RLVECT_1:10 ;
hence contradiction by A16, A17, VECTSP_6:20; :: thesis: verum

end;

then not Carrier (L - K) is empty by A9;
hence contradiction by A1, A6, A13, VECTSP_7:def 1; :: thesis: verum