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