let V be RealUnitarySpace; :: 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 v in A ; :: thesis: for B being Subset of V st B = A \ {v} holds
not v in Lin B
then A2: {v} is Subset of A by SUBSET_1:41;
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
B c= A by A3, XBOOLE_1:36;
then A4: B \/ {v} c= A \/ A by A2, XBOOLE_1:13;
assume v in Lin B ; :: thesis: contradiction
then consider L being Linear_Combination of B such that
A5: v = Sum L by Th1;
{v} is linearly-independent by A1, A2, RLVECT_3:5;
then v <> 0. V by RLVECT_3:8;
then not Carrier L is empty by A5, RLVECT_2:34;
then A6: ex w being object st w in Carrier L ;
v in {v} by TARSKI:def 1;
then v in Lin {v} by Th2;
then consider K being Linear_Combination of {v} such that
A7: v = Sum K by Th1;
A8: ( Carrier L c= B & Carrier K c= {v} ) by RLVECT_2:def 6;
then (Carrier L) \/ (Carrier K) c= B \/ {v} by XBOOLE_1:13;
then ( Carrier (L - K) c= (Carrier L) \/ (Carrier K) & (Carrier L) \/ (Carrier K) c= A ) by A4, RLVECT_2:55;
then Carrier (L - K) c= A ;
then A9: L - K is Linear_Combination of A by RLVECT_2:def 6;
A10: for x being VECTOR of V st x in Carrier L holds
K . x = 0

proof

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

end;

now :: thesis: for x being object st x in Carrier L holds
x in Carrier (L - K)

let x be object ; :: thesis: ( x in Carrier L implies x in Carrier (L - K) )
assume that
A11: x in Carrier L and
A12: not x in Carrier (L - K) ; :: thesis: contradiction
reconsider x = x as VECTOR of V by A11;
A13: L . x <> 0 by A11, RLVECT_2:19;
(L - K) . x = (L . x) - (K . x) by RLVECT_2:54
.= (L . x) - 0 by A10, A11
.= L . x ;
hence contradiction by A12, A13; :: thesis: verum

end;

then A14: Carrier L c= Carrier (L - K) ;
0. V = (Sum L) + (- (Sum K)) by A5, A7, RLVECT_1:5
.= (Sum L) + (Sum (- K)) by RLVECT_3:3
.= Sum (L - K) by RLVECT_3:1 ;
hence contradiction by A1, A6, A9, A14; :: thesis: verum