let p be Prime; :: thesis: for V being free Z_Module
for I being Basis of V
for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is VECTOR of V : u in I } holds
IQ is Basis of Z_MQ_VectSp (V,p)
let V be free Z_Module; :: thesis: for I being Basis of V
for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is VECTOR of V : u in I } holds
IQ is Basis of Z_MQ_VectSp (V,p)
let I be Basis of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is VECTOR of V : u in I } holds
IQ is Basis of Z_MQ_VectSp (V,p)
let IQ be Subset of (Z_MQ_VectSp (V,p)); :: thesis: ( IQ = { (ZMtoMQV (V,p,u)) where u is VECTOR of V : u in I } implies IQ is Basis of Z_MQ_VectSp (V,p) )
assume A1: IQ = { (ZMtoMQV (V,p,u)) where u is VECTOR of V : u in I } ; :: thesis: IQ is Basis of Z_MQ_VectSp (V,p)
A2: IQ is linearly-independent by Th32, A1;
for vq being Element of (Z_MQ_VectSp (V,p)) holds vq in Lin IQ

proof

let vq be Element of (Z_MQ_VectSp (V,p)); :: thesis: vq in Lin IQ
consider v being VECTOR of V such that
A3: vq = ZMtoMQV (V,p,v) by Th22;
Lin I = Z_ModuleStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by Def2;
then consider l being Z_Linear_Combination of I such that
A4: v = Sum l by STRUCT_0:def 5, ZMODUL02:64;
thus vq in Lin IQ by A1, A4, A3, Th34; :: thesis: verum

end;

hence IQ is Basis of Z_MQ_VectSp (V,p) by A2, VECTSP_4:32, VECTSP_7:def 3; :: thesis: verum