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₁[ Element of NAT ] means Sum f,N,$1 = b * (N - $1);
A3: for M being Element of NAT st S₁[M] holds
S₁[M + 1]

proof

let M be Element of 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 7
.= (Sum f,N) - ((Partial_Sums f) . (M + 1)) by SERIES_1:def 6
.= (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 6
.= (b * (N - M)) + (- (f . (M + 1))) by A4, SERIES_1:def 7
.= (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 6
.= 0 by A1, SERIES_1:def 1 ;
then Sum f,N,0 = (Sum f,N) - 0 by SERIES_1:def 7
.= b * (N - 0 ) by A1, A2, Lm14 ;
then A5: S₁[ 0 ] ;
for M being Element of NAT holds S₁[M] from NAT_1:sch 1(A5, A3);
hence for M being Element of NAT holds Sum f,N,M = b * (N - M) ; :: thesis: verum