let F be Real_Sequence; :: thesis: for n being Nat

for a being Real st ( for k being Nat holds F . k = a ) holds

(Partial_Sums F) . n = a * (n + 1)

let n be Nat; :: thesis: for a being Real st ( for k being Nat holds F . k = a ) holds

(Partial_Sums F) . n = a * (n + 1)

let a be Real; :: thesis: ( ( for k being Nat holds F . k = a ) implies (Partial_Sums F) . n = a * (n + 1) )

assume A1: for k being Nat holds F . k = a ; :: thesis: (Partial_Sums F) . n = a * (n + 1)

defpred S_{1}[ Nat] means (Partial_Sums F) . $1 = a * ($1 + 1);

(Partial_Sums F) . 0 = F . 0 by SERIES_1:def 1;

then A2: S_{1}[ 0 ]
by A1;

A3: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[i]
from NAT_1:sch 2(A2, A3);

hence (Partial_Sums F) . n = a * (n + 1) ; :: thesis: verum

for a being Real st ( for k being Nat holds F . k = a ) holds

(Partial_Sums F) . n = a * (n + 1)

let n be Nat; :: thesis: for a being Real st ( for k being Nat holds F . k = a ) holds

(Partial_Sums F) . n = a * (n + 1)

let a be Real; :: thesis: ( ( for k being Nat holds F . k = a ) implies (Partial_Sums F) . n = a * (n + 1) )

assume A1: for k being Nat holds F . k = a ; :: thesis: (Partial_Sums F) . n = a * (n + 1)

defpred S

(Partial_Sums F) . 0 = F . 0 by SERIES_1:def 1;

then A2: S

A3: for i being Nat st S

S

proof

for i being Nat holds S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A4: S_{1}[i]
; :: thesis: S_{1}[i + 1]

reconsider i1 = i + 1, One = 1 as Real ;

(Partial_Sums F) . (i + 1) = ((Partial_Sums F) . i) + (F . (i + 1)) by SERIES_1:def 1;

then (Partial_Sums F) . (i + 1) = (a * (i + 1)) + a by A1, A4;

hence S_{1}[i + 1]
; :: thesis: verum

end;assume A4: S

reconsider i1 = i + 1, One = 1 as Real ;

(Partial_Sums F) . (i + 1) = ((Partial_Sums F) . i) + (F . (i + 1)) by SERIES_1:def 1;

then (Partial_Sums F) . (i + 1) = (a * (i + 1)) + a by A1, A4;

hence S

hence (Partial_Sums F) . n = a * (n + 1) ; :: thesis: verum