theorem Th24: :: NUMBER03:24

for i, k being Nat
for r being Real holds ((Partial_Sums (r GeoSeq)) . ((k + i) + 1)) - ((Partial_Sums (r GeoSeq)) . k) = (r |^ (k + 1)) * ((Partial_Sums (r GeoSeq)) . i)