for R being non empty multLoopStr
for A being non empty Subset of R
for L being RightLinearCombination of A ex E being FinSequence of [: the carrier of R, the carrier of R:] st E represents L