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:
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:
A5: B is independent by A3, Def2;
A is independent by A2, Def2;
then reconsider A' = A, B' = B as finite linearly-independent Subset of V by A5, Th11;
set V' = Lin (A' \/ B');
A' c= the carrier of (Lin (A' \/ B'))

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in A' ; :: thesis:
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:

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:
assume a in B' ; :: thesis:
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:

end;

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

now

assume C c= the carrier of (Lin A') ; :: thesis:
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
A12: C' c= E by VECTSP_7:27, VECTSP_9:16;
A13: card A = card E by A10, A11, VECTSP_9:26;
then E is finite ;
hence contradiction by A9, A12, A13, NAT_1:44; :: thesis:

end;

then consider x being set such that
A14: x in C and
A15: x nin the carrier of (Lin A') by TARSKI:def 3;
A16: x in C \ the carrier of (Lin A') by A14, A15, XBOOLE_0:def 5;
then A17: e nin the carrier of (Lin A') by XBOOLE_0:def 5;
A18: e in C by A16, XBOOLE_0:def 5;
then e in A \/ B by A8;
then reconsider e = e as Element of (LinearlyIndependentSubsets V) ;
take e ; :: thesis:
A c= the carrier of (Lin A')

proof

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

end;

then A19: e nin A by A16, XBOOLE_0:def 5;
then A20: e in B' by A8, A18, XBOOLE_0:def 3;
hence e in B \ A by A19, XBOOLE_0:def 5; :: thesis:
reconsider a = e as Element of V by A20;
A' \/ {a} is linearly-independent by A17, Th13;
hence A \/ {e} in the_family_of (LinearlyIndependentSubsets V) by A1; :: thesis: