set M = LinearlyIndependentSubsets V;
A2: the_family_of (LinearlyIndependentSubsets V) = { A where A is Subset of V : A is linearly-independent } by Def5;
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 A5: ( A in the_family_of (LinearlyIndependentSubsets V) & B in the_family_of (LinearlyIndependentSubsets V) & 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) )
( A is independent & B is independent ) by A5, Def8;
then reconsider A' = A, B' = B as finite linearly-independent Subset of V by Th21;
set V' = Lin (A' \/ B');
A' c= the carrier of (Lin (A' \/ B'))

proof

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

end;

then reconsider A'' = A' as finite linearly-independent Subset of (Lin (A' \/ B')) by VECTSP_9:16;
B' c= the carrier of (Lin (A' \/ B'))

proof

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

end;

then reconsider B'' = B' as finite linearly-independent Subset of (Lin (A' \/ B')) by VECTSP_9:16;
A0: Lin (A' \/ B') = Lin (A'' \/ B'') by VECTSP_9:21;
then consider D being Basis of Lin (A' \/ B') such that
A4: B' c= D by VECTSP_7:27;
consider C being Basis of Lin (A' \/ B') such that
A3: C c= A'' \/ B'' by A0, VECTSP_7:28;
consider e being Element of C \ the carrier of (Lin A');
reconsider c = C as finite set by A3;
A8: ( c is Basis of Lin (A' \/ B') & A' is Basis of Lin A' ) by RANKNULL:20;
then BB: ( Lin (A' \/ B') is finite-dimensional & Lin A' is finite-dimensional ) by MATRLIN:def 3;
then card c = card D by VECTSP_9:26;
then card B c= card c by A4, CARD_1:27;
then card B <= card c by NAT_1:40;
then A9: card A < card c by A5, NAT_1:13;

now

assume C c= the carrier of (Lin A') ; :: thesis: contradiction
then reconsider C' = C as Subset of (Lin A') ;
the carrier of (Lin A') c= the carrier of V by VECTSP_4:def 2;
then reconsider C'' = C' as Subset of V by XBOOLE_1:1;
C is linearly-independent by VECTSP_7:def 3;
then C'' is linearly-independent by VECTSP_9:15;
then consider E being Basis of Lin A' such that
B2: C' c= E by VECTSP_7:27, VECTSP_9:16;
B3: card A = card E by A8, BB, VECTSP_9:26;
then A,E are_equipotent by CARD_1:21;
then E is finite by CARD_1:68;
hence contradiction by A9, B2, B3, NAT_1:44; :: thesis: verum

end;

then consider x being set such that
AA: ( x in C & x nin the carrier of (Lin A') ) by TARSKI:def 3;
x in C \ the carrier of (Lin A') by AA, XBOOLE_0:def 5;
then A6: ( e in C & e nin the carrier of (Lin A') ) by XBOOLE_0:def 5;
then A7: e in A \/ B by A3;
then reconsider e = e 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 A')

proof

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

end;

then B7: e nin A by A6;
then B8: e in B' by A7, XBOOLE_0:def 3;
hence e in B \ A by B7, XBOOLE_0:def 5; :: thesis: A \/ {e} in the_family_of (LinearlyIndependentSubsets V)
reconsider a = e as Element of V by B8;
A' \/ {a} is linearly-independent by A6, ThI1;
hence A \/ {e} in the_family_of (LinearlyIndependentSubsets V) by A2; :: thesis: verum