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:
reconsider D0 = D as finite Subset of V by AS;
A \ D0 <> {} by ;
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 ;
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 ;
consider f being Function such that
P7: ( f is one-to-one & dom f = D0 \/ {x} & rng f c= A ) by ;
set B = rng f;
P8: card (rng f) = (card D0) + 1 by ;
then reconsider B = rng f as finite set ;
reconsider B = B as finite Subset of V by ;
B is linearly-dependent by ;
hence A is linearly-dependent by ; :: thesis: verum