:: deftheorem Def10 defines RightLinearCombination IDEAL_1:def 10 :
for R being non empty multLoopStr
for A being non empty Subset of R
for b₃ being FinSequence of the carrier of R holds
( b₃ is RightLinearCombination of A iff for i being set st i in dom b₃ holds
ex u being Element of R ex a being Element of A st b₃ /. i = a * u );