let R be non empty multLoopStr ; :: thesis: for A being non empty Subset of R
for L being LeftLinearCombination of A ex E being FinSequence of [:the carrier of R,the carrier of R:] st E represents L
let A be non empty Subset of R; :: thesis: for L being LeftLinearCombination of A ex E being FinSequence of [:the carrier of R,the carrier of R:] st E represents L
let L be LeftLinearCombination of A; :: thesis: ex E being FinSequence of [:the carrier of R,the carrier of R:] st E represents L
set D = [:the carrier of R,the carrier of R:];
defpred S₁[ set , set ] means ex x, y being Element of R st
( $2 = [x,y] & y in A & L /. $1 = x * y );

A1: now

let k be Element of NAT ; :: thesis: ( k in Seg (len L) implies ex d being Element of [:the carrier of R,the carrier of R:] st S₁[k,d] )
assume k in Seg (len L) ; :: thesis: ex d being Element of [:the carrier of R,the carrier of R:] st S₁[k,d]
then k in dom L by FINSEQ_1:def 3;
then consider u being Element of R, a being Element of A such that
A2: L /. k = u * a by Def10;
reconsider b = a as Element of R ;
reconsider d = [u,b] as Element of [:the carrier of R,the carrier of R:] ;
take d = d; :: thesis: S₁[k,d]
thus S₁[k,d] by A2; :: thesis: verum

end;

consider E being FinSequence of [:the carrier of R,the carrier of R:] such that
A3: dom E = Seg (len L) and
A4: for k being Element of NAT st k in Seg (len L) holds
S₁[k,E /. k] from POLYNOM2:sch 1(A1);
take E ; :: thesis: E represents L
A5: dom L = Seg (len L) by FINSEQ_1:def 3;
thus len E = len L by A3, FINSEQ_1:def 3; :: according to IDEAL_1:def 13 :: thesis: for i being set st i in dom L holds
( L . i = ((E /. i) `1 ) * ((E /. i) `2 ) & (E /. i) `2 in A )
let i be set ; :: thesis: ( i in dom L implies ( L . i = ((E /. i) `1 ) * ((E /. i) `2 ) & (E /. i) `2 in A ) )
assume A6: i in dom L ; :: thesis: ( L . i = ((E /. i) `1 ) * ((E /. i) `2 ) & (E /. i) `2 in A )
reconsider k = i as Element of NAT by A6;
consider x, y being Element of R such that
A7: ( E /. k = [x,y] & y in A & L /. k = x * y ) by A4, A5, A6;
( [x,y] `1 = x & [x,y] `2 = y ) by MCART_1:def 1, MCART_1:def 2;
hence L . i = ((E /. i) `1 ) * ((E /. i) `2 ) by A6, A7, PARTFUN1:def 8; :: thesis: (E /. i) `2 in A
thus (E /. i) `2 in A by A7, MCART_1:def 2; :: thesis: verum