let V be free Z_Module; :: thesis: for I, A being finite Subset of V st I is Basis of V & (card I) + 1 = card A holds
A is linearly-dependent
let I, A be finite Subset of V; :: thesis: ( I is Basis of V & (card I) + 1 = card A implies A is linearly-dependent )
assume AS: ( I is Basis of V & (card I) + 1 = card A ) ; :: thesis: A is linearly-dependent
reconsider IQ = (MorphsZQ V) .: I as Subset of (Z_MQ_VectSp V) ;
reconsider IQ = IQ as finite Subset of (Z_MQ_VectSp V) ;
P2: IQ is Basis of (Z_MQ_VectSp V) by AS, ThEQRZMV3D;
assume P31: not A is linearly-dependent ; :: thesis: contradiction
reconsider B = (MorphsZQ V) .: A as Subset of (Z_MQ_VectSp V) ;
reconsider B = B as finite Subset of (Z_MQ_VectSp V) ;
PP: ( IQ is linearly-independent & Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp V), the addF of (Z_MQ_VectSp V), the ZeroF of (Z_MQ_VectSp V), the lmult of (Z_MQ_VectSp V) #) ) by VECTSP_7:def 3, P2;
B is linearly-independent by P31, ThEQRZMV3C;
then P5: card B <= card IQ by VECTSP_9:19, PP;
card IQ = card I by ThEQRZMV3E;
then card A <= card I by P5, ThEQRZMV3E;
hence contradiction by AS, NAT_1:13; :: thesis: verum