let f be Real_Sequence; :: thesis: for b being Real st f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = b ) holds
for N being Element of NAT holds Sum f,N = b * N
let b be Real; :: thesis: ( f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = b ) implies for N being Element of NAT holds Sum f,N = b * N )
defpred S₁[ Element of NAT ] means Sum f,$1 = b * $1;
assume A1: ( f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = b ) ) ; :: thesis: for N being Element of NAT holds Sum f,N = b * N
then (Partial_Sums f) . 0 = 0 by SERIES_1:def 1;
then A2: S₁[ 0 ] by SERIES_1:def 6;
A3: for N being Element of NAT st S₁[N] holds
S₁[N + 1]

proof

let N be Element of NAT ; :: thesis: ( S₁[N] implies S₁[N + 1] )
assume A4: Sum f,N = b * N ; :: thesis: S₁[N + 1]
Sum f,(N + 1) = (Partial_Sums f) . (N + 1) by SERIES_1:def 6
.= ((Partial_Sums f) . N) + (f . (N + 1)) by SERIES_1:def 1
.= (b * N) + (f . (N + 1)) by A4, SERIES_1:def 6
.= (b * N) + (b * 1) by A1
.= b * (N + 1) ;
hence S₁[N + 1] ; :: thesis: verum

end;

for N being Element of NAT holds S₁[N] from NAT_1:sch 1(A2, A3);
hence for N being Element of NAT holds Sum f,N = b * N ; :: thesis: verum