let V be RealLinearSpace; :: 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
let B be Subset of V; :: thesis: ( B = I \/ A implies not B is linearly-independent )
assume A2: B = I \/ A ; :: thesis: not B is linearly-independent
assume A3: B is linearly-independent ; :: thesis: contradiction
consider v being set such that
A4: v in A by XBOOLE_0:def 1;
reconsider v = v as VECTOR of V by A4;
reconsider Bv = B \ {v} as Subset of V ;
A5: A c= B by A2, XBOOLE_1:7;
I c= B by A2, XBOOLE_1:7;
then ( I \ {v} c= B \ {v} & not v in I ) by A1, A4, XBOOLE_0:3, XBOOLE_1:33;
then I c= Bv by ZFMISC_1:65;
then ( Lin I is Subspace of Lin Bv & v in Lin I ) by Th14, RLVECT_3:23;
hence contradiction by A3, A4, A5, Th18, RLSUB_1:16; :: thesis: verum