theorem Th29: :: ZMODUL03:29

for p being prime Element of INT.Ring
for V being free Z_Module
for s being FinSequence of V
for t being FinSequence of (Z_MQ_VectSp (V,p)) st len s = len t & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & t . i = ZMtoMQV (V,p,si) ) ) holds
Sum t = ZMtoMQV (V,p,(Sum s))