set M = LinearlyIndependentSubsets V;
A1:
the_family_of (LinearlyIndependentSubsets V) = { A where A is Subset of V : A is linearly-independent }
by Def8;
let A, B be finite Subset of (LinearlyIndependentSubsets V); MATROID0:def 4 ( A in the_family_of (LinearlyIndependentSubsets V) & B in the_family_of (LinearlyIndependentSubsets V) & card B = (card A) + 1 implies ex e being Element of (LinearlyIndependentSubsets V) st
( e in B \ A & A \/ {e} in the_family_of (LinearlyIndependentSubsets V) ) )
assume that
A2:
A in the_family_of (LinearlyIndependentSubsets V)
and
A3:
B in the_family_of (LinearlyIndependentSubsets V)
and
A4:
card B = (card A) + 1
; ex e being Element of (LinearlyIndependentSubsets V) st
( e in B \ A & A \/ {e} in the_family_of (LinearlyIndependentSubsets V) )
A5:
B is independent
by A3;
A is independent
by A2;
then reconsider A9 = A, B9 = B as finite linearly-independent Subset of V by A5, Th11;
set V9 = Lin (A9 \/ B9);
A9 c= the carrier of (Lin (A9 \/ B9))
then reconsider A99 = A9 as finite linearly-independent Subset of (Lin (A9 \/ B9)) by VECTSP_9:12;
B9 c= the carrier of (Lin (A9 \/ B9))
then reconsider B99 = B9 as finite linearly-independent Subset of (Lin (A9 \/ B9)) by VECTSP_9:12;
A6:
Lin (A9 \/ B9) = Lin (A99 \/ B99)
by VECTSP_9:17;
then consider D being Basis of (Lin (A9 \/ B9)) such that
A7:
B9 c= D
by VECTSP_7:19;
consider C being Basis of (Lin (A9 \/ B9)) such that
A8:
C c= A99 \/ B99
by A6, VECTSP_7:20;
reconsider c = C as finite set by A8;
c is Basis of (Lin (A9 \/ B9))
;
then
Lin (A9 \/ B9) is finite-dimensional
by MATRLIN:def 1;
then
card c = card D
by VECTSP_9:22;
then
Segm (card B) c= Segm (card c)
by A7, CARD_1:11;
then
card B <= card c
by NAT_1:39;
then A9:
card A < card c
by A4, NAT_1:13;
set e = the Element of C \ the carrier of (Lin A9);
A10:
A9 is Basis of (Lin A9)
by RANKNULL:20;
then A11:
Lin A9 is finite-dimensional
by MATRLIN:def 1;
then consider x being object such that
A14:
x in C
and
A15:
x nin the carrier of (Lin A9)
;
A16:
x in C \ the carrier of (Lin A9)
by A14, A15, XBOOLE_0:def 5;
then A17:
the Element of C \ the carrier of (Lin A9) nin the carrier of (Lin A9)
by XBOOLE_0:def 5;
A18:
the Element of C \ the carrier of (Lin A9) in C
by A16, XBOOLE_0:def 5;
then
the Element of C \ the carrier of (Lin A9) in A \/ B
by A8;
then reconsider e = the Element of C \ the carrier of (Lin A9) as Element of (LinearlyIndependentSubsets V) ;
take
e
; ( e in B \ A & A \/ {e} in the_family_of (LinearlyIndependentSubsets V) )
A c= the carrier of (Lin A9)
then A19:
e nin A
by A16, XBOOLE_0:def 5;
then A20:
e in B9
by A8, A18, XBOOLE_0:def 3;
hence
e in B \ A
by A19, XBOOLE_0:def 5; A \/ {e} in the_family_of (LinearlyIndependentSubsets V)
reconsider a = e as Element of V by A20;
A9 \/ {a} is linearly-independent
by A17, Th13;
hence
A \/ {e} in the_family_of (LinearlyIndependentSubsets V)
by A1; verum