let f be Real_Sequence; :: thesis: for N, M being Nat holds (Sum f,N,M) + (f . (N + 1)) = Sum f,(N + 1),M
let N, M be Nat; :: thesis: (Sum f,N,M) + (f . (N + 1)) = Sum f,(N + 1),M
A1: N in NAT by ORDINAL1:def 13;
(Sum f,N,M) + (f . (N + 1)) = ((Sum f,N) - (Sum f,M)) + (f . (N + 1)) by SERIES_1:def 7
.= ((Sum f,N) + (f . (N + 1))) + (- (Sum f,M))
.= (((Partial_Sums f) . N) + (f . (N + 1))) + (- (Sum f,M)) by SERIES_1:def 6
.= ((Partial_Sums f) . (N + 1)) + (- (Sum f,M)) by A1, SERIES_1:def 1
.= (Sum f,(N + 1)) + (- (Sum f,M)) by SERIES_1:def 6
.= (Sum f,(N + 1)) - (Sum f,M)
.= Sum f,(N + 1),M by SERIES_1:def 7 ;
hence (Sum f,N,M) + (f . (N + 1)) = Sum f,(N + 1),M ; :: thesis: verum