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

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 Subspace of Lin Bv by RLVECT_3:20;

assume A7: B is linearly-independent ; :: thesis: contradiction

v in Lin I by Th13;

hence contradiction by A7, A2, A4, A6, Th17, RLSUB_1:8; :: thesis: verum

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 Subspace of Lin Bv by RLVECT_3:20;

assume A7: B is linearly-independent ; :: thesis: contradiction

v in Lin I by Th13;

hence contradiction by A7, A2, A4, A6, Th17, RLSUB_1:8; :: thesis: verum