let n be Nat; :: thesis: for a being Real holds (Partial_Sums (seq_const a)) . n = a * (n + 1)
let a be Real; :: thesis: (Partial_Sums (seq_const a)) . n = a * (n + 1)
set f = seq_const a;
for k being Nat holds (seq_const a) . k = a by SEQ_1:57;
hence (Partial_Sums (seq_const a)) . n = a * (n + 1) by Th14; :: thesis: verum