theorem :: IDEAL_1:38

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