let R be non empty multLoopStr ; :: thesis: 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; :: thesis: 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; :: thesis: 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 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,the carrier of R:] st S1[k,d] )assume
k in Seg (len L)
;
:: thesis: 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 Def9;
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;
:: thesis: S1[k,d]thus
S1[
k,
d]
by A2;
:: thesis: 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 Element of NAT st k in Seg (len L) holds
S1[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 12 :: thesis: for i being set st i in dom L holds
( L . i = (((E /. i) `1 ) * ((E /. i) `2 )) * ((E /. i) `3 ) & (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) `3 ) & (E /. i) `2 in A ) )
assume A6:
i in dom L
; :: thesis: ( L . i = (((E /. i) `1 ) * ((E /. i) `2 )) * ((E /. i) `3 ) & (E /. i) `2 in A )
reconsider k = i as Element of NAT by A6;
consider x, y, z being Element of R such that
A7:
( E /. k = [x,y,z] & y in A & L /. k = (x * y) * z )
by A4, A5, A6;
( [x,y,z] `1 = x & [x,y,z] `2 = y & [x,y,z] `3 = z )
by MCART_1:def 5, MCART_1:def 6, MCART_1:def 7;
hence
L . i = (((E /. i) `1 ) * ((E /. i) `2 )) * ((E /. i) `3 )
by A6, A7, PARTFUN1:def 8; :: thesis: (E /. i) `2 in A
thus
(E /. i) `2 in A
by A7, MCART_1:def 6; :: thesis: verum