let V be RealLinearSpace; 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; 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; ( A misses I implies for B being Subset of V st B = I \/ A holds
B is linearly-dependent )
assume A1:
A misses I
; 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; ( B = I \/ A implies B is linearly-dependent )
assume A3:
B = I \/ A
; 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
; contradiction
v in Lin I
by Th13;
hence
contradiction
by A7, A2, A4, A6, Th17, RLSUB_1:8; verum