set M = LinearlyIndependentSubsets V;
A1: the_family_of (LinearlyIndependentSubsets V) = { A where A is Subset of V : A is linearly-independent } by Def9;
let A, B be finite Subset of (LinearlyIndependentSubsets V); :: according to MATROID0:def 4 :: thesis: ( 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 ; :: thesis: 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, Def2;
A is independent by A2, Def2;
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))

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in A9 or a in the carrier of (Lin (A9 \/ B9)) )
assume a in A9 ; :: thesis: a in the carrier of (Lin (A9 \/ B9))
then a in A9 \/ B9 by XBOOLE_0:def 3;
then a in Lin (A9 \/ B9) by VECTSP_7:8;
hence a in the carrier of (Lin (A9 \/ B9)) by STRUCT_0:def 5; :: thesis: verum

end;

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))

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in B9 or a in the carrier of (Lin (A9 \/ B9)) )
assume a in B9 ; :: thesis: a in the carrier of (Lin (A9 \/ B9))
then a in A9 \/ B9 by XBOOLE_0:def 3;
then a in Lin (A9 \/ B9) by VECTSP_7:8;
hence a in the carrier of (Lin (A9 \/ B9)) by STRUCT_0:def 5; :: thesis: verum

end;

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 card B c= 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;

now

assume C c= the carrier of (Lin A9) ; :: thesis: contradiction
then reconsider C9 = C as Subset of (Lin A9) ;
the carrier of (Lin A9) c= the carrier of V by VECTSP_4:def 2;
then reconsider C99 = C9 as Subset of V by XBOOLE_1:1;
C is linearly-independent by VECTSP_7:def 3;
then C99 is linearly-independent by VECTSP_9:11;
then consider E being Basis of Lin A9 such that
A12: C9 c= E by VECTSP_7:19, VECTSP_9:12;
A13: card A = card E by A10, A11, VECTSP_9:22;
then E is finite ;
hence contradiction by A9, A12, A13, NAT_1:43; :: thesis: verum

end;

then consider x being set such that
A14: x in C and
A15: x nin the carrier of (Lin A9) by TARSKI:def 3;
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 ; :: thesis: ( e in B \ A & A \/ {e} in the_family_of (LinearlyIndependentSubsets V) )
A c= the carrier of (Lin A9)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in the carrier of (Lin A9) )
assume x in A ; :: thesis: x in the carrier of (Lin A9)
then x in Lin A9 by VECTSP_7:8;
hence x in the carrier of (Lin A9) by STRUCT_0:def 5; :: thesis: verum

end;

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; :: thesis: 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; :: thesis: verum