theorem Th31: :: IDEAL_1:31

for R being non empty associative commutative multLoopStr
for A being non empty Subset of R
for f being LinearCombination of A holds
( f is LeftLinearCombination of A & f is RightLinearCombination of A )