theorem Th8: :: HURWITZ:8

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for x being Element of L
for F being FinSequence of L holds x * (Sum F) = Sum (x * F)