let a, b be Real; :: thesis: for s being Real_Sequence st ( for n being Nat holds s . n = (a * n) + b ) holds
for n being Nat holds (Partial_Sums s) . n = ((n + 1) * ((s . 0) + (s . n))) / 2
let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n = (a * n) + b ) implies for n being Nat holds (Partial_Sums s) . n = ((n + 1) * ((s . 0) + (s . n))) / 2 )
assume A1: for n being Nat holds s . n = (a * n) + b ; :: thesis: for n being Nat holds (Partial_Sums s) . n = ((n + 1) * ((s . 0) + (s . n))) / 2
let n be Nat; :: thesis: (Partial_Sums s) . n = ((n + 1) * ((s . 0) + (s . n))) / 2
(Partial_Sums s) . n = ((((a * (n + 1)) * n) / 2) + (n * b)) + b by A1, Lm14
.= ((n + 1) * (((n * a) + b) + b)) / 2
.= ((n + 1) * ((s . n) + ((a * 0) + b))) / 2 by A1
.= ((n + 1) * ((s . n) + (s . 0))) / 2 by A1 ;
hence (Partial_Sums s) . n = ((n + 1) * ((s . 0) + (s . n))) / 2 ; :: thesis: verum