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

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 )
;

end;

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

hence A \/ {x} is linearly-dependent by ZMODUL03:16; :: thesis: verum

end;reconsider A9 = A as Basis of (Lin A) by A3, ThLin7;

reconsider B = A9 \/ X as Subset of (Lin A) ;

X misses A9

proof

then
B is linearly-dependent
by ZMODUL03:18;
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 ex y being object st

( y in X & y in A9 ) by XBOOLE_0:3;

hence contradiction by A2, TARSKI:def 1; :: thesis: verum

hence A \/ {x} is linearly-dependent by ZMODUL03:16; :: thesis: verum