theorem :: ZMODUL05:34

for V being Z_Module
for A being Subset of V
for l being Linear_Combination of A
for x being Element of V
for a being Element of INT.Ring holds l +* (x,a) is Linear_Combination of A \/ {x}