let R, S be non empty multLoopStr ; 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; 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; 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; 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; 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:]; ( 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
; ( 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 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
; 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)) ) )
then reconsider LC = LC as LeftLinearCombination of G by Def9;
take
LC
; ( 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; for i being set st i in dom LC holds
LC . i = (P . ((E /. i) `1)) * (P . ((E /. i) `2))
let i be set ; ( i in dom LC implies LC . i = (P . ((E /. i) `1)) * (P . ((E /. i) `2)) )
assume
i in dom LC
; LC . i = (P . ((E /. i) `1)) * (P . ((E /. i) `2))
hence
LC . i = (P . ((E /. i) `1)) * (P . ((E /. i) `2))
by A3; verum