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

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

B9 c= the carrier of (Lin (A9 \/ B9))

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;

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: ( e in B \ A & A \/ {e} in the_family_of (LinearlyIndependentSubsets V) )

A c= the carrier of (Lin A9)

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

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

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

proof

then reconsider A99 = A9 as finite linearly-independent Subset of (Lin (A9 \/ B9)) by VECTSP_9:12;
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;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

B9 c= the carrier of (Lin (A9 \/ B9))

proof

then reconsider B99 = B9 as finite linearly-independent Subset of (Lin (A9 \/ B9)) by VECTSP_9:12;
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;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

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;

now :: thesis: not C c= the carrier of (Lin A9)

then consider x being object such that 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 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

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: ( e in B \ A & A \/ {e} in the_family_of (LinearlyIndependentSubsets V) )

A c= the carrier of (Lin A9)

proof

then A19:
e nin A
by A16, XBOOLE_0:def 5;
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;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

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