theorem Th33: :: ZMODUL03:33

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Subset 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
for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ