theorem Th5: :: POLYNOM8:5

for L being non empty right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for s being FinSequence of L
for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ) holds
Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)