let V be free Z_Module; :: thesis: for I being Subset of V
for IQ being Subset of () st IQ = () .: I & I is Basis of V holds
IQ is Basis of ()

let I be Subset of V; :: thesis: for IQ being Subset of () st IQ = () .: I & I is Basis of V holds
IQ is Basis of ()

let IQ be Subset of (); :: thesis: ( IQ = () .: I & I is Basis of V implies IQ is Basis of () )
assume AS: ( IQ = () .: I & I is Basis of V ) ; :: thesis: IQ is Basis of ()
then I is base ;
then X0: ( I is linearly-independent & Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) by VECTSP_7:def 3;
X1: IQ is linearly-independent by ;
AS0: Z_MQ_VectSp V = ModuleStr(# (Class ()),(),(),() #) by defZMQVSp;
for vq being Element of () holds vq in Lin IQ
proof
let vq be Element of (); :: thesis: vq in Lin IQ
consider i being Element of INT.Ring, v being Element of V such that
P3: ( i <> 0 & vq = Class ((),[v,i]) ) by ;
v in Lin I by X0;
then consider l being Linear_Combination of I such that
P4: v = Sum l by ZMODUL02:64;
thus vq in Lin IQ by ; :: thesis: verum
end;
hence IQ is Basis of () by ; :: thesis: verum