let F be Field; :: thesis: for V being VectSp of
for A being Subset of
for x being Element of st x in Lin A & not x in A holds
not A \/ {x} is linearly-independent
let V be VectSp of ; :: thesis: for A being Subset of
for x being Element of st x in Lin A & not x in A holds
not A \/ {x} is linearly-independent
let A be Subset of ; :: thesis: for x being Element of st x in Lin A & not x in A holds
not A \/ {x} is linearly-independent
let x be Element of ; :: 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 A3: A is linearly-independent ; :: thesis: not A \/ {x} is linearly-independent

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

proof

assume X meets A' ; :: thesis: contradiction
then ex y being set st
( y in X & y in A' ) by XBOOLE_0:3;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum

end;

then not B is linearly-independent by VECTSP_9:19;
hence not A \/ {x} is linearly-independent by VECTSP_9:16; :: thesis: verum

end;

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

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

end;

end;