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₁[ Nat] means Sum (f,$1) = b * $1;
assume that
A1: f . 0 = 0 and
A2: 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
A3: for N being Nat st S₁[N] holds
S₁[N + 1]

proof

let N be 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 5
.= ((Partial_Sums f) . N) + (f . (N + 1)) by SERIES_1:def 1
.= (b * N) + (f . (N + 1)) by A4, SERIES_1:def 5
.= (b * N) + (b * 1) by A2
.= b * (N + 1) ;
hence S₁[N + 1] ; :: thesis: verum

end;

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