let V be free Z_Module; :: thesis: for D, A being Subset of V st D is Basis of V & D is finite & card D c< card A holds

A is linearly-dependent

let D, A be Subset of V; :: thesis: ( D is Basis of V & D is finite & card D c< card A implies A is linearly-dependent )

assume AS: ( D is Basis of V & D is finite & card D c< card A ) ; :: thesis: A is linearly-dependent

reconsider D0 = D as finite Subset of V by AS;

A \ D0 <> {} by AS, CARD_1:68, ORDINAL1:11;

then consider x being object such that

P3: x in A \ D0 by XBOOLE_0:def 1;

( x in A & not x in D0 ) by P3, XBOOLE_0:def 5;

then P5: card (D0 \/ {x}) = (card D0) + 1 by CARD_2:41;

succ (card D0) = (card D0) +^ 1 by ORDINAL2:31

.= (card D0) + 1 by CARD_2:36 ;

then P6: (card D0) + 1 c= card A by AS, ORDINAL1:11, ORDINAL1:21;

consider f being Function such that

P7: ( f is one-to-one & dom f = D0 \/ {x} & rng f c= A ) by CARD_1:10, P5, P6;

set B = rng f;

P8: card (rng f) = (card D0) + 1 by P5, P7, CARD_1:5, WELLORD2:def 4;

then reconsider B = rng f as finite set ;

reconsider B = B as finite Subset of V by P7, XBOOLE_1:1;

B is linearly-dependent by XXTh1, P8, AS;

hence A is linearly-dependent by XXTh2, P7; :: thesis: verum

A is linearly-dependent

let D, A be Subset of V; :: thesis: ( D is Basis of V & D is finite & card D c< card A implies A is linearly-dependent )

assume AS: ( D is Basis of V & D is finite & card D c< card A ) ; :: thesis: A is linearly-dependent

reconsider D0 = D as finite Subset of V by AS;

A \ D0 <> {} by AS, CARD_1:68, ORDINAL1:11;

then consider x being object such that

P3: x in A \ D0 by XBOOLE_0:def 1;

( x in A & not x in D0 ) by P3, XBOOLE_0:def 5;

then P5: card (D0 \/ {x}) = (card D0) + 1 by CARD_2:41;

succ (card D0) = (card D0) +^ 1 by ORDINAL2:31

.= (card D0) + 1 by CARD_2:36 ;

then P6: (card D0) + 1 c= card A by AS, ORDINAL1:11, ORDINAL1:21;

consider f being Function such that

P7: ( f is one-to-one & dom f = D0 \/ {x} & rng f c= A ) by CARD_1:10, P5, P6;

set B = rng f;

P8: card (rng f) = (card D0) + 1 by P5, P7, CARD_1:5, WELLORD2:def 4;

then reconsider B = rng f as finite set ;

reconsider B = B as finite Subset of V by P7, XBOOLE_1:1;

B is linearly-dependent by XXTh1, P8, AS;

hence A is linearly-dependent by XXTh2, P7; :: thesis: verum