let R, S be non empty multLoopStr ; :: thesis: for F being non empty Subset of R
for lc being LeftLinearCombination 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:] st P .: F c= G & E represents lc holds
ex LC being LeftLinearCombination 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)) ) )
let F be non empty Subset of R; :: thesis: for lc being LeftLinearCombination 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:] st P .: F c= G & E represents lc holds
ex LC being LeftLinearCombination 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)) ) )
let lc be LeftLinearCombination 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:] st P .: F c= G & E represents lc holds
ex LC being LeftLinearCombination 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)) ) )
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:] st P .: F c= G & E represents lc holds
ex LC being LeftLinearCombination 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)) ) )
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:] st P .: F c= G & E represents lc holds
ex LC being LeftLinearCombination 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)) ) )
let E be FinSequence of [: the carrier of R, the carrier of R:]; :: thesis: ( P .: F c= G & E represents lc implies ex LC being LeftLinearCombination 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)) ) ) )
assume A1: P .: F c= G ; :: thesis: ( not E represents lc or ex LC being LeftLinearCombination 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)) ) ) )
deffunc H₁( Nat) -> Element of the carrier of S = (P . ((E /. $1) `1)) * (P . ((E /. $1) `2));
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 LeftLinearCombination 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)) ) )

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

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

end;

then reconsider LC = LC as LeftLinearCombination 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)) ) )
thus len lc = len LC by A2; :: thesis: for i being set st i in dom LC holds
LC . i = (P . ((E /. i) `1)) * (P . ((E /. i) `2))
let i be set ; :: thesis: ( i in dom LC implies LC . i = (P . ((E /. i) `1)) * (P . ((E /. i) `2)) )
assume i in dom LC ; :: thesis: LC . i = (P . ((E /. i) `1)) * (P . ((E /. i) `2))
hence LC . i = (P . ((E /. i) `1)) * (P . ((E /. i) `2)) by A3; :: thesis: verum