:: deftheorem defines represents IDEAL_1:def 12 :
for R being non empty multLoopStr
for A being non empty Subset of R
for L being LeftLinearCombination of A
for E being FinSequence of [: the carrier of R, the carrier of R:] holds
( E represents L iff ( len E = len L & ( for i being set st i in dom L holds
( L . i = ((E /. i) `1) * ((E /. i) `2) & (E /. i) `2 in A ) ) ) );