let f be Real_Sequence; :: thesis: for b being Real
for N being Element of NAT st f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = b ) holds
for M being Element of NAT holds Sum (f,N,M) = b * (N - M)
let b be Real; :: thesis: for N being Element of NAT st f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = b ) holds
for M being Element of NAT holds Sum (f,N,M) = b * (N - M)
let N be Element of NAT ; :: thesis: ( f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = b ) implies for M being Element of NAT holds Sum (f,N,M) = b * (N - M) )
assume that
A1: f . 0 = 0 and
A2: for n being Element of NAT st n > 0 holds
f . n = b ; :: thesis: for M being Element of NAT holds Sum (f,N,M) = b * (N - M)
defpred S₁[ Nat] means Sum (f,N,$1) = b * (N - $1);
A3: for M being Nat st S₁[M] holds
S₁[M + 1]

proof

let M be Nat; :: thesis: ( S₁[M] implies S₁[M + 1] )
assume A4: Sum (f,N,M) = b * (N - M) ; :: thesis: S₁[M + 1]
Sum (f,N,(M + 1)) = (Sum (f,N)) - (Sum (f,(M + 1))) by SERIES_1:def 6
.= (Sum (f,N)) - ((Partial_Sums f) . (M + 1)) by SERIES_1:def 5
.= (Sum (f,N)) - (((Partial_Sums f) . M) + (f . (M + 1))) by SERIES_1:def 1
.= ((Sum (f,N)) - ((Partial_Sums f) . M)) + (- (f . (M + 1)))
.= ((Sum (f,N)) - (Sum (f,M))) + (- (f . (M + 1))) by SERIES_1:def 5
.= (b * (N - M)) + (- (f . (M + 1))) by A4, SERIES_1:def 6
.= (b * (N - M)) + (- b) by A2
.= b * (N - (M + 1)) ;
hence S₁[M + 1] ; :: thesis: verum

end;

Sum (f,0) = (Partial_Sums f) . 0 by SERIES_1:def 5
.= 0 by A1, SERIES_1:def 1 ;
then Sum (f,N,0) = (Sum (f,N)) - 0 by SERIES_1:def 6
.= b * (N - 0) by A1, A2, Lm14 ;
then A5: S₁[ 0 ] ;
for M being Nat holds S₁[M] from NAT_1:sch 2(A5, A3);
hence for M being Element of NAT holds Sum (f,N,M) = b * (N - M) ; :: thesis: verum