set M = LinearlyIndependentSubsets V;
A1: the_family_of = { A where A is Subset of V : A is linearly-independent } by Def8;
let A, B be finite Subset of ; :: according to MATROID0:def 4 :: thesis: ( A in the_family_of & B in the_family_of & card B = (card A) + 1 implies ex e being Element of st
( e in B \ A & A \/ {e} in the_family_of ) )

assume that
A2: A in the_family_of and
A3: B in the_family_of and
A4: card B = (card A) + 1 ; :: thesis: ex e being Element of st
( e in B \ A & A \/ {e} in the_family_of )

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 ;
set V9 = Lin (A9 \/ B9);
A9 c= the carrier of (Lin (A9 \/ B9))
proof
let a be object ; :: 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)) ; :: 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 object ; :: 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)) ; :: 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 ;
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 ;
then card B <= card c by NAT_1:39;
then A9: card A < card c by ;
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 :: thesis: not C c= the carrier of (Lin A9)
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 ;
A13: card A = card E by ;
then E is finite ;
hence contradiction by A9, A12, A13, NAT_1:43; :: thesis: verum
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 ;
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 ;
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 ;
take e ; :: thesis: ( e in B \ A & A \/ {e} in the_family_of )
A c= the carrier of (Lin A9)
proof
let x be object ; :: 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) ; :: thesis: verum
end;
then A19: e nin A by ;
then A20: e in B9 by ;
hence e in B \ A by ; :: thesis:
reconsider a = e as Element of V by A20;
A9 \/ {a} is linearly-independent by ;
hence A \/ {e} in the_family_of by A1; :: thesis: verum