for R being non empty associative multLoopStr
for A being non empty Subset of R
for a being Element of R
for F being LinearCombination of A holds a * F is LinearCombination of A