for R being Ring
for V being RightMod of R
for a being Scalar of R
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
L * a is Linear_Combination of A