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