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

end;

then reconsider LC = LC as RightLinearCombination of G by Def11;
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 A3; :: 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 A10: i in dom LC ; :: thesis: LC . i = (P . ((E /. i) `1 )) * (P . ((E /. i) `2 ))
thus LC . i = (P . ((E /. i) `1 )) * (P . ((E /. i) `2 )) by A4, A10; :: thesis: verum