theorem Th24: :: HILBASIS:24

for R, S being non empty right_complementable add-associative right_zeroed doubleLoopStr
for F being non empty Subset of R
for G being non empty Subset of S
for P being Function of R,S
for lc being LinearCombination of F
for LC being LinearCombination of G
for E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] st P is RingHomomorphism & len lc = len LC & E represents 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)) ) holds
P . (Sum lc) = Sum LC