let V be free Z_Module; :: thesis: for I being Basis of V
for A being non empty Subset of V st A misses I holds
for B being Subset of V st B = I \/ A holds
B is linearly-dependent
let I be Basis of V; :: thesis: for A being non empty Subset of V st A misses I holds
for B being Subset of V st B = I \/ A holds
B is linearly-dependent
let A be non empty Subset of V; :: thesis: ( A misses I implies for B being Subset of V st B = I \/ A holds
B is linearly-dependent )
assume A1: A misses I ; :: thesis: for B being Subset of V st B = I \/ A holds
B is linearly-dependent
consider v being object such that
A2: v in A by XBOOLE_0:def 1;
let B be Subset of V; :: thesis: ( B = I \/ A implies B is linearly-dependent )
assume A3: B = I \/ A ; :: thesis: B is linearly-dependent
A4: A c= B by A3, XBOOLE_1:7;
reconsider v = v as Vector of V by A2;
reconsider Bv = B \ {v} as Subset of V ;
A5: I \ {v} c= B \ {v} by A3, XBOOLE_1:7, XBOOLE_1:33;
not v in I by A1, A2, XBOOLE_0:3;
then I c= Bv by A5, ZFMISC_1:57;
then A6: Lin I is Submodule of Lin Bv by ZMODUL02:70;
assume A7: B is linearly-independent ; :: thesis: contradiction
v in Lin I by Th14;
hence contradiction by A7, A2, A4, A6, Th17, ZMODUL01:23; :: thesis: verum