theorem XThSum1: :: ZMODUL04:7

for V being Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V)
for l being Linear_Combination of I
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & l = lq * (MorphsZQ V) holds
Sum lq = (MorphsZQ V) . (Sum l)