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 :: thesis: for k being Nat st k in Seg (len L) holds
ex d being Element of [: the carrier of R, the carrier of R:] st S₁[k,d]

let k be 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 Def9;
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 Nat st k in Seg (len L) holds
S₁[k,E /. k] from RECDEF_1:sch 17(A1);
take E ; :: thesis: E represents L
thus len E = len L by A3, FINSEQ_1:def 3; :: according to IDEAL_1:def 12 :: 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 A5: 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 A5;
dom L = Seg (len L) by FINSEQ_1:def 3;
then consider x, y being Element of R such that
A6: E /. k = [x,y] and
A7: y in A and
A8: L /. k = x * y by A4, A5;
thus L . i = ((E /. i) `1) * ((E /. i) `2) by A5, A6, A8, PARTFUN1:def 6; :: thesis: (E /. i) `2 in A
thus (E /. i) `2 in A by A6, A7; :: thesis: verum