let R be non empty multLoopStr ; for A being non empty Subset of R
for L being LinearCombination of A ex E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] st E represents L
let A be non empty Subset of R; for L being LinearCombination of A ex E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] st E represents L
let L be LinearCombination of A; ex E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] st E represents L
set D = [: the carrier of R, the carrier of R, the carrier of R:];
defpred S1[ set , set ] means ex x, y, z being Element of R st
( $2 = [x,y,z] & y in A & L /. $1 = (x * y) * z );
A1:
now for k being Nat st k in Seg (len L) holds
ex d being Element of [: the carrier of R, the carrier of R, the carrier of R:] st S1[k,d]let k be
Nat;
( k in Seg (len L) implies ex d being Element of [: the carrier of R, the carrier of R, the carrier of R:] st S1[k,d] )assume
k in Seg (len L)
;
ex d being Element of [: the carrier of R, the carrier of R, the carrier of R:] st S1[k,d]then
k in dom L
by FINSEQ_1:def 3;
then consider u,
v being
Element of
R,
a being
Element of
A such that A2:
L /. k = (u * a) * v
by Def8;
reconsider b =
a as
Element of
R ;
reconsider d =
[u,b,v] as
Element of
[: the carrier of R, the carrier of R, the carrier of R:] ;
take d =
d;
S1[k,d]thus
S1[
k,
d]
by A2;
verum end;
consider E being FinSequence of [: the carrier of R, 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 11 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 )
let i be set ; ( i in dom L implies ( L . i = (((E /. i) `1_3) * ((E /. i) `2_3)) * ((E /. i) `3_3) & (E /. i) `2_3 in A ) )
assume A5:
i in dom L
; ( L . i = (((E /. i) `1_3) * ((E /. i) `2_3)) * ((E /. i) `3_3) & (E /. i) `2_3 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, z being Element of R such that
A6:
E /. k = [x,y,z]
and
A7:
y in A
and
A8:
L /. k = (x * y) * z
by A4, A5;
thus
L . i = (((E /. i) `1_3) * ((E /. i) `2_3)) * ((E /. i) `3_3)
by A5, A6, A8, PARTFUN1:def 6; (E /. i) `2_3 in A
thus
(E /. i) `2_3 in A
by A6, A7; verum