let R, S be non empty multLoopStr ; :: thesis: for F being non empty Subset of R
for lc being RightLinearCombination 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 RightLinearCombination 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 RightLinearCombination 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 RightLinearCombination 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 RightLinearCombination 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 RightLinearCombination 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 RightLinearCombination 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 RightLinearCombination 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 RightLinearCombination 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 RightLinearCombination 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 H1( 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 = H1(k) from FINSEQ_2:sch 1();
 assume A4: E represents lc ; :: thesis: ex LC being RightLinearCombination 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 v being Element of S ex a being Element of G st LC /. i = a * v
let i be set ; :: thesis: ( i in dom LC implies ex v being Element of S ex a being Element of G st LC /. i = a * v )
assume A5: i in dom LC ; :: thesis: ex v being Element of S ex a being Element of G st LC /. i = a * v
dom lc = dom LC by A2, FINSEQ_3:29;
then ( dom P = the carrier of R & (E /. i) `1 in F ) by A4, A5, FUNCT_2:def 1;
then P . ((E /. i) `1) in P .: F by FUNCT_1:def 6;
then reconsider a = P . ((E /. i) `1) as Element of G by A1;
reconsider v = P . ((E /. i) `2) as Element of S ;
take v = v; :: thesis: ex a being Element of G st LC /. i = a * v
take a = a; :: thesis: LC /. i = a * v
LC . i = LC /. i by A5, PARTFUN1:def 6;
hence LC /. i = a * v by A3, A5; :: thesis: verum
end;
then reconsider LC = LC as RightLinearCombination of G by Def10;
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