let R, S be non empty multLoopStr ; :: thesis: for F being non empty Subset of R
for lc being LinearCombination of F
for G being non empty Subset of S
for P being Function of the carrier of R,the carrier of S
for E being FinSequence of [:the carrier of R,the carrier of R,the carrier of R:] st P .: F c= G & E represents lc holds
ex LC being LinearCombination of G st
( len lc = len LC & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) )
let F be non empty Subset of R; :: thesis: for lc being LinearCombination of F
for G being non empty Subset of S
for P being Function of the carrier of R,the carrier of S
for E being FinSequence of [:the carrier of R,the carrier of R,the carrier of R:] st P .: F c= G & E represents lc holds
ex LC being LinearCombination of G st
( len lc = len LC & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) )
let lc be LinearCombination of F; :: thesis: for G being non empty Subset of S
for P being Function of the carrier of R,the carrier of S
for E being FinSequence of [:the carrier of R,the carrier of R,the carrier of R:] st P .: F c= G & E represents lc holds
ex LC being LinearCombination of G st
( len lc = len LC & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) )
let G be non empty Subset of S; :: thesis: for P being Function of the carrier of R,the carrier of S
for E being FinSequence of [:the carrier of R,the carrier of R,the carrier of R:] st P .: F c= G & E represents lc holds
ex LC being LinearCombination of G st
( len lc = len LC & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) )
let P be Function of the carrier of R,the carrier of S; :: thesis: for E being FinSequence of [:the carrier of R,the carrier of R,the carrier of R:] st P .: F c= G & E represents lc holds
ex LC being LinearCombination of G st
( len lc = len LC & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) )
let E be FinSequence of [:the carrier of R,the carrier of R,the carrier of R:]; :: thesis: ( P .: F c= G & E represents lc implies ex LC being LinearCombination of G st
( len lc = len LC & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) ) )
assume A1: P .: F c= G ; :: thesis: ( not E represents lc or ex LC being LinearCombination of G st
( len lc = len LC & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) ) )
assume A2: E represents lc ; :: thesis: ex LC being LinearCombination of G st
( len lc = len LC & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) )
deffunc H₁( Nat) -> Element of the carrier of S = ((P . ((E /. $1) `1 )) * (P . ((E /. $1) `2 ))) * (P . ((E /. $1) `3 ));
consider LC being FinSequence of the carrier of S such that
A3: len LC = len lc and
A4: for k being Nat st k in dom LC holds
LC . k = H₁(k) from FINSEQ_2:sch 1();

now

let i be set ; :: thesis: ( i in dom LC implies ex u, v being Element of S ex a being Element of G st LC /. i = (u * a) * v )
assume A6: i in dom LC ; :: thesis: ex u, v being Element of S ex a being Element of G st LC /. i = (u * a) * v
reconsider u = P . ((E /. i) `1 ), v = P . ((E /. i) `3 ) as Element of S ;
A8: dom P = the carrier of R by FUNCT_2:def 1;
dom lc = dom LC by A3, FINSEQ_3:31;
then (E /. i) `2 in F by A2, A6, Def12;
then P . ((E /. i) `2 ) in P .: F by A8, FUNCT_1:def 12;
then reconsider a = P . ((E /. i) `2 ) as Element of G by A1;
take u = u; :: thesis: ex v being Element of S ex a being Element of G st LC /. i = (u * a) * v
take v = v; :: thesis: ex a being Element of G st LC /. i = (u * a) * v
take a = a; :: thesis: LC /. i = (u * a) * v
LC . i = LC /. i by A6, PARTFUN1:def 8;
hence LC /. i = (u * a) * v by A4, A6; :: thesis: verum

end;

then reconsider LC = LC as LinearCombination of G by Def9;
take LC ; :: thesis: ( len lc = len LC & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) )
thus len lc = len LC by A3; :: thesis: for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 ))
let i be set ; :: thesis: ( i in dom LC implies LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) )
assume A10: i in dom LC ; :: thesis: LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 ))
thus LC . i = ((P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) by A4, A10; :: thesis: verum