theorem XThSum: :: ZMODUL04:6

for V being Z_Module st V is Mult-cancelable holds
for s being FinSequence of V
for t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds
Sum t = (MorphsZQ V) . (Sum s)