for R being non empty multLoopStr
for A being non empty Subset of R
for l being LinearCombination of A
for n being Nat holds l | (Seg n) is LinearCombination of A