:: deftheorem Def8 defines LinearCombination IDEAL_1:def 8 :
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 LinearCombination of A iff for i being set st i in dom b₃ holds
ex u, v being Element of R ex a being Element of A st b₃ /. i = (u * a) * v );