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:
per cases ;
suppose A3: A is linearly-independent ; :: thesis:
reconsider X = {x} as Subset of (Lin A) by ;
reconsider A9 = A as Basis of (Lin A) by ;
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:
end;
end;