let V be free finite-rank Z_Module; :: thesis: for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent
let A be Subset of V; :: thesis: for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent
let x be Element of V; :: thesis: ( x in Lin A & not x in A implies A \/ {x} is linearly-dependent )
assume that
A1: x in Lin A and
A2: not x in A ; :: thesis: A \/ {x} is linearly-dependent
per cases ( A is linearly-independent or A is linearly-dependent ) ;
suppose A3: A is linearly-independent ; :: thesis: A \/ {x} is linearly-dependent
reconsider X = {x} as Subset of (Lin A) by A1, SUBSET_1:41;
reconsider A9 = A as Basis of (Lin A) by A3, ThLin7;
reconsider B = A9 \/ X as Subset of (Lin A) ;
X misses A9
proof
assume X meets A9 ; :: thesis: contradiction
then ex y being object st
( y in X & y in A9 ) by XBOOLE_0:3;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum
end;
then B is linearly-dependent by ZMODUL03:18;
hence A \/ {x} is linearly-dependent by ZMODUL03:16; :: thesis: verum
end;
suppose A is linearly-dependent ; :: thesis: A \/ {x} is linearly-dependent
hence A \/ {x} is linearly-dependent by ZMODUL02:56, XBOOLE_1:7; :: thesis: verum
end;
end;