theorem ThEQRZMV3B: :: ZMODUL04:10

for V being Z_Module
for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V)
for lq being Linear_Combination of IQ
for m being Integer
for a being Element of F_Rat
for l being Linear_Combination of I st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds
a * (Sum lq) = (MorphsZQ V) . (Sum l)