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

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in A9 ; :: thesis:
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)) ; :: thesis:

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

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in B9 ; :: thesis:
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)) ; :: thesis:

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

assume C c= the carrier of (Lin A9) ; :: thesis:
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:

end;

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 ; :: thesis:
A c= the carrier of (Lin A9)

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in A ; :: thesis:
then x in Lin A9 by VECTSP_7:8;
hence x in the carrier of (Lin A9) ; :: thesis:

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