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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) ) )
deffunc H<sub>1</sub>( Nat) -> Element of the carrier of S = ((P . ((E /. $1) `1_3)) * (P . ((E /. $1) `2_3))) * (P . ((E /. $1) `3_3));
consider LC being FinSequence of the carrier of S such that
A2: len LC = len lc and
A3: for k being Nat st k in dom LC holds
LC . k = H₁(k) from FINSEQ_2:sch 1();
assume A4: 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_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) )

now :: thesis: for i being set st i in dom LC holds
ex u, v being Element of S ex a being Element of G st LC /. i = (u * a) * v

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 A5: i in dom LC ; :: thesis: ex u, v being Element of S ex a being Element of G st LC /. i = (u * a) * v
dom lc = dom LC by A2, FINSEQ_3:29;
then ( dom P = the carrier of R & (E /. i) `2_3 in F ) by A4, A5, FUNCT_2:def 1;
then P . ((E /. i) `2_3) in P .: F by FUNCT_1:def 6;
then reconsider a = P . ((E /. i) `2_3) as Element of G by A1;
reconsider u = P . ((E /. i) `1_3), v = P . ((E /. i) `3_3) as Element of S ;
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 A5, PARTFUN1:def 6;
hence LC /. i = (u * a) * v by A3, A5; :: thesis: verum

end;

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