theorem :: ZMODUL05:34

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