theorem :: IDEAL_1:36

for R, S being non empty multLoopStr
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)) ) )