:: deftheorem defines represents IDEAL_1:def 11 :
for R being non empty multLoopStr
for A being non empty Subset of R
for L being LinearCombination of A
for E being FinSequence of [: the carrier of R, 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_3) * ((E /. i) `2_3)) * ((E /. i) `3_3) & (E /. i) `2_3 in A ) ) ) );