let R be non empty multLoopStr ; 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; 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; 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 S1[ set , set ] means ex x, y being Element of R st
( $2 = [x,y] & y in A & L /. $1 = x * y );
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
S1[k,E /. k]
from RECDEF_1:sch 17(A1);
take
E
; E represents L
thus
len E = len L
by A3, FINSEQ_1:def 3; IDEAL_1:def 12 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 ; ( i in dom L implies ( L . i = ((E /. i) `1) * ((E /. i) `2) & (E /. i) `2 in A ) )
assume A5:
i in dom L
; ( 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; (E /. i) `2 in A
thus
(E /. i) `2 in A
by A6, A7; verum