theorem :: MEASURE9:56

for F being ExtREAL_sequence
for n being Nat
for a being R_eal st ( for k being Nat holds F . k = a ) holds
(Partial_Sums F) . n = a * (n + 1)