theorem Th1: :: RATFUNC1:1

for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for a being Element of L
for p, q being FinSequence of L st len p = len q & ( for i being Element of NAT st i in dom p holds
q /. i = a * (p /. i) ) holds
Sum q = a * (Sum p)