let p be prime Element of INT.Ring; :: thesis:
let V be free Z_Module; :: thesis:
let I be Subset of V; :: thesis:
let IQ be Subset of (Z_MQ_VectSp (V,p)); :: thesis:
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:
for vq being Element of (Z_MQ_VectSp (V,p)) holds vq in Lin IQ

let vq be Element of (Z_MQ_VectSp (V,p)); :: thesis:
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:

end;