let F be Field; :: thesis: for V being VectSp of F
for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
not A \/ {x} is linearly-independent
let V be VectSp of F; :: thesis: for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
not A \/ {x} is linearly-independent
let A be Subset of V; :: thesis: for x being Element of V st x in Lin A & not x in A holds
not A \/ {x} is linearly-independent
let x be Element of V; :: thesis: ( x in Lin A & not x in A implies not A \/ {x} is linearly-independent )
assume that
A1: x in Lin A and
A2: not x in A ; :: thesis: not A \/ {x} is linearly-independent

per cases ( A is linearly-independent or not A is linearly-independent ) ;

suppose A is linearly-independent ; :: thesis: not A \/ {x} is linearly-independent

then reconsider A' = A as Basis of Lin A by Th20;
x in [#] (Lin A) by A1, STRUCT_0:def 5;
then reconsider X = {x} as Subset of (Lin A) by SUBSET_1:63;
A3: X misses A'

proof

assume X meets A' ; :: thesis: contradiction
then consider y being set such that
A4: y in X and
A5: y in A' by XBOOLE_0:3;
thus contradiction by A2, A4, A5, TARSKI:def 1; :: thesis: verum

end;

reconsider B = A' \/ X as Subset of (Lin A) ;
A6: not B is linearly-independent by A3, VECTSP_9:19;
thus not A \/ {x} is linearly-independent by A6, VECTSP_9:16; :: thesis: verum

end;

suppose A7: not A is linearly-independent ; :: thesis: not A \/ {x} is linearly-independent

thus not A \/ {x} is linearly-independent by A7, VECTSP_7:2, XBOOLE_1:7; :: thesis: verum

end;

end;