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

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