let p be prime Element of INT.Ring; :: thesis: for V being free Z_Module

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp (V,p)) st Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #)

let V be free Z_Module; :: thesis: for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp (V,p)) st Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #)

let I be Subset of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp (V,p)) st Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #)

let IQ be Subset of (Z_MQ_VectSp (V,p)); :: thesis: ( Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } implies Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #) )

assume that

P0: Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) and

AS: IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } ; :: thesis: Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #)

for vq being Element of (Z_MQ_VectSp (V,p)) holds vq in Lin IQ

for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp (V,p)) st Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #)

let V be free Z_Module; :: thesis: for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp (V,p)) st Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #)

let I be Subset of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp (V,p)) st Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #)

let IQ be Subset of (Z_MQ_VectSp (V,p)); :: thesis: ( Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } implies Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #) )

assume that

P0: Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) and

AS: IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } ; :: thesis: Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #)

for vq being Element of (Z_MQ_VectSp (V,p)) holds vq in Lin IQ

proof

hence
Lin IQ = ModuleStr(# the carrier of (Z_MQ_VectSp (V,p)), the addF of (Z_MQ_VectSp (V,p)), the ZeroF of (Z_MQ_VectSp (V,p)), the lmult of (Z_MQ_VectSp (V,p)) #)
by VECTSP_4:32; :: thesis: verum
let vq be Element of (Z_MQ_VectSp (V,p)); :: thesis: vq in Lin IQ

consider v being Vector of V such that

P3: vq = ZMtoMQV (V,p,v) by ZMODUL03:22;

consider l being Linear_Combination of I such that

P4: v = Sum l by P0, STRUCT_0:def 5, ZMODUL02:64;

thus vq in Lin IQ by AS, P4, P3, ThQuotBasis5A; :: thesis: verum

end;consider v being Vector of V such that

P3: vq = ZMtoMQV (V,p,v) by ZMODUL03:22;

consider l being Linear_Combination of I such that

P4: v = Sum l by P0, STRUCT_0:def 5, ZMODUL02:64;

thus vq in Lin IQ by AS, P4, P3, ThQuotBasis5A; :: thesis: verum