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)
(Sum (f,N,M)) + (f . (N + 1)) = ((Sum (f,N)) - (Sum (f,M))) + (f . (N + 1)) by SERIES_1:def 6
.= ((Sum (f,N)) + (f . (N + 1))) + (- (Sum (f,M)))
.= (((Partial_Sums f) . N) + (f . (N + 1))) + (- (Sum (f,M))) by SERIES_1:def 5
.= ((Partial_Sums f) . (N + 1)) + (- (Sum (f,M))) by SERIES_1:def 1
.= (Sum (f,(N + 1))) + (- (Sum (f,M))) by SERIES_1:def 5
.= (Sum (f,(N + 1))) - (Sum (f,M))
.= Sum (f,(N + 1),M) by SERIES_1:def 6 ;
hence (Sum (f,N,M)) + (f . (N + 1)) = Sum (f,(N + 1),M) ; :: thesis: verum