let GF be Field; :: thesis: for V being VectSp of GF
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
not B is linearly-independent
let V be VectSp of GF; :: 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
not B is linearly-independent
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
not B is linearly-independent
let A be non empty Subset of V; :: thesis: ( A misses I implies for B being Subset of V st B = I \/ A holds
not B is linearly-independent )
assume A1: A misses I ; :: thesis: for B being Subset of V st B = I \/ A holds
not B is linearly-independent
consider v being set such that
A2: v in A by XBOOLE_0:def 1;
let B be Subset of V; :: thesis: ( B = I \/ A implies not B is linearly-independent )
assume A3: B = I \/ A ; :: thesis: not B is linearly-independent
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 Subspace of Lin Bv by VECTSP_7:13;
assume A7: B is linearly-independent ; :: thesis: contradiction
v in Lin I by Th14;
hence contradiction by A7, A2, A4, A6, Th18, VECTSP_4:8; :: thesis: verum